Reproducing the boundary-context checks

Use the official Lean 4.30.0 release. This package needs Lean’s bundled core and standard libraries, not Mathlib or any separately fetched package.

From this directory:

LEAN_BIN=/absolute/path/to/lean-4.30.0-linux/bin/lean ./check.sh

If lean is already on PATH, ./check.sh suffices. The script prints the actual version, requires all six modules (Fragments, Contexts, Adaptive, Summaries, Examples, Audit), rejects source-level sorry, admit, and axiom tokens outside comments and strings, and checks each module from source. It places generated .olean files in a fresh temporary directory and removes that directory at exit. Warnings are errors. The modules’ own #print axioms commands report dependencies of the audited declarations.

The lexical guard is a supplemental check, not a theorem prover. The Lean kernel checks the elaborated proof terms. Ordinary foundational axioms reported by #print axioms must be distinguished from custom unproved mathematical assumptions; the verification report records the actual list. No finite testing is substituted for a universal proof.

Runtime used for the recorded check

• Release: leanprover/lean4 tag v4.30.0.
• Lean reports commit d024af099ca4bf2c86f649261ebf59565dc8c622.
• Archive: lean-4.30.0-linux.tar.zst, 529208534 bytes.
• SHA-256: 4dad74141c2c119ca1aa626656be83b8e14238afba97271fd7bf1eb3f081b319.
• The downloaded archive’s SHA-256 matched the digest in the official GitHub release API response.

Official sources:

• Release
• Linux archive
• Release metadata

Extract with tar --no-same-owner --zstd -xf lean-4.30.0-linux.tar.zst when running in a container that cannot restore the archive owner’s numeric ID.

Optional container path compatibility

The checking container’s numeric process IDs did not correspond to its mounted /proc/<pid> directories. /proc/self/exe worked, but Lean 4.30.0 uses getpid() followed by readlink("/proc/<pid>/exe") when locating its own libraries. This made the official executable fail before checking a file. LEAN_SYSROOT does not repair that startup path: Lean’s internal search-path initialization calls getBuildDir, which calls IO.appDir.

The supplied proc-self-compat.c is an optional, narrowly scoped workaround for that container behavior. It intercepts readlink only when the requested path is exactly /proc/ plus the calling process’s getpid() plus /exe; it redirects that lookup to /proc/self/exe. Every other lookup goes directly to the system readlink. It does not alter Lean’s kernel, elaborator, proof terms, axioms, or imported library files.

To reproduce that environment-specific check:

cc -shared -fPIC -O2 proc-self-compat.c -ldl -o /tmp/fprd-proc-self-compat.so
FPRD_LEAN_PRELOAD=/tmp/fprd-proc-self-compat.so \
  LEAN_BIN=/absolute/path/to/lean-4.30.0-linux/bin/lean ./check.sh

Normal installations should omit this option. The C source is included so that the workaround can be inspected and rebuilt rather than relying on an opaque binary. The source SHA-256 used for the recorded check was 6ee11fe1995a880c299af53a18b97ac88b6e0138f219a4d3e63e24c05da987ca.