| Rust (rustc/cargo ≥ 1.85, edition 2024; developed with 1.92) | The implementation language and its build system. | Chosen by the specification (presk-specs/report/chapters/08-implementation.tex): pattern matching and traits for deep IRs, memory safety, the e-graph ecosystem (egg) for the later optimizer, serde for the serialized IR, LLVM/Cranelift bindings for code generation. Cargo builds and tests every crate; nothing else drives it. |
| make | GNU make, driving the Makefile. | A thin orchestrator over cargo for the recipes that are not a single cargo command (check-examples, sync-examples, doc). Preferred to just because it is installed everywhere the project is developed. The specification’s rule: cargo for the compiler, a thin orchestrator on top, never a foreign build system driving cargo. |
rustdoc (cargo doc) | Rust’s documentation generator. | Renders this manual (crate presk-manual, Markdown chapters included with #[doc = include_str!]) and the API documentation of the crates, in one tool, with search and navigation, no extra dependency. |
| cargo-insta (optional CLI) | Reviewer for insta snapshots. | cargo insta review shows the diff of every changed snapshot and accepts or rejects it; without it, INSTA_UPDATE=always cargo test rewrites snapshots blindly. |
| cranelift-codegen, -frontend, -module, -jit, -native 0.131 | The Cranelift code generator (from the Wasmtime project): IR, a builder for it, linking, an in-process JIT, host ISA detection. | The native backend compiles each kernel to machine code at run time. Pure Rust, fast compilation, no LLVM installation; version 0.131 is the newest that builds with rustc 1.92 (Cranelift’s minimum Rust version follows stable closely). |
| libm 0.2 | Pure-Rust port of the C math library: musl’s, as it was before musl 1.1.23. | The functions the kernel interpreter and the Cranelift backend compute exp, log, tanh, sin, cos and erf with, in f64 and f32, so that the two give the same bits (the interpreter took Rust’s standard library’s for all but erf until 0.16.0, D159; the standard library has no erf). Since 0.9.0 step 2, presk-export-c‘s tests compare the C export’s copy of musl’s functions with it, bit for bit (D78). Since step 6 the kernel backends’ sample calls its exp, so that their draws do not depend on the platform’s C library and the C export’s presk_exp gives the same (D83). |
A C compiler (cc; GCC 13.3 on falicon) | The system’s C compiler, or the one CC names. | Already needed to build GMP and MPFR for rug. Since 0.9.0 step 1, presk-export-c’s tests compile the printed kernels with it, with the export’s flags (-std=c11 -O2 -ffp-contract=off) and -Wall -Wextra -Werror, so make test runs it (D77). Since step 3, presk-cli’s and presk-export-c’s tests also build exported programs with their own Makefile (make) and run their conformance/check.sh (sh, cmp), as subprocesses (D79). Since step 5 with OpenMP too (-fopenmp, GCC’s libgomp), a launch divided among threads being an OpenMP region; every program is built with it and without it (D81). |
GCC 16.2.0 (optional), built from its release into .gcc (experiments/gcc/setup.sh) | GNU’s C compiler at its latest release, C only, with the libgomp it ships; the script checks the tarball’s SHA-256, lets the release’s contrib/download_prerequisites fetch GMP, MPFR, MPC and isl, and builds without bootstrap and without root (three minutes on twenty cores, 1.4 GB installed). .gcc/wrap holds gcc and cc calling it with an rpath to its libgomp. Optional: only D184’s timing puts it on PATH; the compiler of record stays the system’s cc. | Ubuntu 24.04’s GCC 13.3 knows neither of falicon’s cores (Cortex-X925, A725), so its -mcpu=native passes no target (D183), and the distribution’s newest, GCC 14.2, needs root and knows neither. GCC 16 knows NVIDIA’s GB10, the chip falicon is: its -mcpu=native and -march=native pass -mcpu=gb10+crc+nossbs, Armv9.2-A with SVE2, which makes the C program’s “-O3 -march=native” mean what it says (D184). |
zig 0.16.0 (its zig cc: Clang 21.1.0), from PyPI (ziglang) | A C compiler driver over Clang that cross-compiles to any target out of the box, with the C libraries’ headers and sources (musl, glibc) it needs; one package (382 MB installed), installed by pip into .venv-zig (make zig). Optional: only make c-conformance uses it. | Statement C3 of plan 0.9.0 asks the exported C to compile without a warning on Clang and for x86-64 as well as on GCC. Falicon has neither Clang nor an x86-64 cross-compiler, and the distribution’s packages need root; zig gives both from one pinned version in a virtual environment, the same on every machine. On aarch64 the Clang build is linked and run, and gives the native bits; the x86-64 build (musl, static) is linked, not run. zig has no OpenMP runtime, so the OpenMP build is compiled on both, not linked, against GCC’s omp.h (0.9.0 step 5, D81). |
LLVM 23.1.2, its release for Linux on aarch64 (clang and its headers, with Polly linked in), from GitHub | The LLVM project’s own binary release, whose clang links Polly, LLVM’s polyhedral optimizer (-mllvm -polly), and with it isl; downloaded by make llvm (1.8 GB, its SHA-256 pinned), of which bin/clang and lib/clang/23/include are kept in .llvm (413 MB), without root. Optional: make c-conformance uses it, and since 0.17.0 step 3 the LLVM backend (--backend llvm), which compiles each kernel with this clang and links it with the system’s linker. | The SCoP mode of the C export (0.9.0 step 8) writes each nest as a static-control part for a polyhedral tool, and a polyhedral front end checks that each static-control nest is one SCoP. Falicon has none of the plan’s (pet, Clang with Polly): Ubuntu packages neither pet nor PLUTO, and its clang-18 and libpolly-18-dev need root. The release links Polly into clang (loading LLVMPolly.so as well registers its options twice and aborts), so -mllvm -polly suffices. Chosen over GCC’s Graphite, installed but whose verdict follows GCC’s own passes (it rejects nests of one loop, cuts a softmax, and takes most gathers), and over pet, which would be built from source against Clang’s libraries (D85). The LLVM backend (0.17.0 step 3, D176) needs no more of the release: no libLLVM and no LLVM headers, since it prints C and drives clang as a program (route (a) of plan 0.17.0’s question 1). |
Gappa 1.6.0 (optional; Debian’s package gappa, apt install gappa) | A prover of bounds on straight-line expressions over the reals with rounding operators (float<ieee_32,ne>(…)), from interval hypotheses, by interval arithmetic and its own rewriting rules, with a proof a checker can replay (Inria, de Dinechin, Lauter, Melquiond). | make gappa (D108) sets one nest’s bound proved beside the compiler’s and the measured gap: experiments/gappa_layernorm.py writes the layer norm’s kernels, operation by operation in their order, as a Gappa file whose hypotheses are the envelope presk calibrate --precision measured, and Gappa proves the distance to the exact value. The compiler neither calls nor links it; the .g files and Gappa’s answers are kept under docs/gappa/. Packaged by Debian and Ubuntu; on a machine without it, its source builds with GMP, MPFR and Boost (.gappa/ is git-ignored for that). make gappa-dot (D131) ran it so on falicon: Gappa 1.6.0’s source release configured with Boost 1.83’s headers and the GMP and MPFR that gmp-mpfr-sys builds for presk (CPPFLAGS=-I… LDFLAGS=-L…, ./remake, GAPPA=.gappa/gappa-1.6.0/src/gappa), the largest bound of each of D108’s layer-norm files D108’s to the bit. |
pandoc 3.1.3 (optional; Debian’s package, /usr/bin/pandoc on falicon) | A converter between document formats; here Markdown to PDF through LaTeX. | make explain-pdf makes the PDF of a presk explain document from its Markdown, which the tool writes and which stays the document of record (0.11.0 step 6, D116). The compiler does not depend on it: the PDF is a make target. pandoc’s pipe tables take their columns’ widths from the dashes the renderer writes. |
LuaLaTeX from TeX Live 2026 (optional; /usr/local/texlive/2026/bin/aarch64-linux on falicon, TEXLIVE= another), with the packages fvextra, etoolbox and xurl | The TeX engine pandoc drives (--pdf-engine=lualatex), which reads OpenType fonts by name; fvextra’s verbatim breaks a long listing’s lines, etoolbox sets the tables’ size, xurl breaks a long path. | A presk explain document is mostly Unicode (ℝ, θ, ‖∂L/∂v‖₁, subscripts) in listings, which pdfLaTeX’s 8-bit fonts cannot set. crates/presk-explain/pandoc/header.tex holds the settings. |
DejaVu fonts (Serif, Sans, Sans Mono; Debian’s fonts-dejavu) | Free fonts with a wide Unicode coverage. | Their monospace face has every character a document’s listings print (ℝ, θ, ∂, ‖, ⁻, ᵢ), so the PDF has no missing glyph. |
| uv (optional) | Python package and environment manager. | make venv creates .venv for the conformance tests in seconds; any way of installing PyTorch into .venv works. |
PyTorch 2.14, NumPy, pytest (optional, in .venv) | The framework the export targets; its array dependency; the test runner. | Needed only to run the generated test_conformance.py and train.py (make conformance); the compiler never imports them. PyTorch’s exact F.gelu (erf-based) and torch.func (functional_call, grad) are what the export relies on. |
tokenizers 0.23.3 (optional, in .venv) | Hugging Face’s tokenizer library, which reads a checkpoint’s tokenizer.json. | The tokenizer of Llama 3.2 stays outside the compiler, which takes and prints token ids: experiments/llama/tokens.py turns text into ids and back (0.17.0 step 7, D180). The converter experiments/llama/hf_to_pskd.py needs none: it reads safetensors by hand (an 8-byte length, a JSON header, the raw bytes) with the standard library and NumPy. |
transformers 5.21.0, safetensors 0.8.0, PyTorch 2.14 (optional, in .venv-hf, make venv-hf) | Hugging Face’s model library, with its Llama, and the format it saves in, in a virtual environment of their own. | Statement RW2 of plan 0.17.0 (D180) compares presk run in f64 on Llama 3.2 1B’s converted weights with LlamaForCausalLM in float64 on the same ids (experiments/llama/rw2.py). Its Llama computes in float32 in three places whatever the model’s type (the rotary angles, LlamaRMSNorm, the eager softmax), so the comparison recomputes the angles by its own function in float64, removes the norm’s cast and takes the SDPA attention. The compiler never imports it; it is kept apart from .venv, whose PyTorch the export’s tests run. Since 0.17.1 (D185) `rw2.py –dtype float32 |
pyarrow 26.0.1 (optional, in .venv-hf) | Apache Arrow’s Python library, which reads Parquet files. | WikiText-2 raw, plan 0.17.1’s text (D185), is distributed as Parquet (Salesforce/wikitext, the user’s download); experiments/llama/texts.py reads its text column. The compiler never imports it. |
llama.cpp b12132 (optional; experiments/llama/setup_llamacpp.sh builds it from its release into .llamacpp, MIT) | ggml-org’s inference engine for quantized models in its GGUF format: its converter from a Hugging Face checkpoint (convert_hf_to_gguf.py, with its own gguf-py, run in .venv-hf), llama-quantize, llama-perplexity and libllama. Built by cmake and the system’s GCC at its defaults (-mcpu=native, OpenMP), without its network library; experiments/llama/llamacpp_logits.c reads the logits of given ids through libllama. | Plan 0.17.1 measures the field’s quantizations (llama.cpp’s BF16, Q8_0, Q4_K_M and Q4_0) against Llama 3.2 1B’s exact logits on the same tokens (D185). The converter imports sentencepiece before it checks for a tokenizer.model Llama 3 does not have; a stand-in module that only lets the import succeed (experiments/llama/stub/) sends it down its Llama 3 path. The compiler neither calls nor links it. |
onnx, onnxscript, onnxruntime (optional, in .venv) | The ONNX graph format and its Python API; the library torch.onnx.export(dynamo=True) uses to build ONNX graphs; the reference runtime for ONNX models. | --mode graph writes model.onnx through PyTorch’s exporter (which needs onnxscript), and the generated test_onnx runs it under ONNX Runtime against the interpreter; none of the three is imported by the compiler. |