Portable Lean replay instructions
Machine Native Reasoning
RUNTIME_REPRODUCTION.md
1 # Reproduce the pinned offline proof environment
2
3 Use the saved `Lean_Compact_01.zip` through `Lean_Compact_05.zip`, not a newer
4 online compiler. These are separately stored user runtime parts and are not copied
5 into this source delivery. Place the five ZIPs in one directory and run:
6
7 ```sh
8 python3 tools/restore_runtime.py --parts /path/to/parts \
9 --out /path/to/Lean_Portable_Compact.tar.xz \
10 --extract-to /path/to/runtime-parent
11 ```
12
13 The tool verifies every chunk and the complete archive before extracting. It
14 refuses an existing output file or a nonempty extraction directory and requires
15 Python's `tarfile.data_filter`. The actual combined archive is 2,220,147,424 bytes,
16 with SHA-256
17 `f7548038f94ea30789ce28fc2ff769c40e9c37d8879ea133e9bea821056342c7`.
18 In this continuation the helper assembled and extracted all 166,035 members.
19 The actual restoration receipts are under `evidence/runtime19/`. The helper code
20 is byte-identical to the predecessor and its earlier 28-fixture validation remains in historical evidence. The current gates rerun 20 verifier tests and 10 snapshot/comparison tests. This does not prove arbitrary Python executions correct.
21
22 The runtime root is
23 `runtime-parent/Komorebi_Portable_Lean_4.34.0-rc2`. Its compiler is Lean 4.34.0-rc2,
24 commit `6a10ac8c22beadecabdbb0919c2b50214762f91d`. Mathlib is pinned to
25 `aeb72f1e9981b6d35b426b16dca7759be3e7ba06`, alongside eight other pinned
26 repositories. The cumulative gate verifies all nine revisions, the compiler
27 identity and the actual imported proof-cache artifacts against the retained
28 runtime inventory. It does not rebuild those dependencies or independently attest
29 their origin. The runtime is Linux x86-64; native Windows execution is not claimed.
30
31 ## Verify the delivered source before building
32
33 ```sh
34 python3 tools/verify_package.py
35 python3 scripts/supervise.py \
36 --runtime /path/to/runtime-parent/Komorebi_Portable_Lean_4.34.0-rc2 \
37 --out evidence/my_replay --whole-timeout 1800
38 ```
39
40 Choose a new output directory. A run adds files to the working tree, so the immutable
41 package integrity command is intended before generating those new outputs. An
42 independent extracted-source replay must use a separate source directory with no
43 preexisting project objects. Run the primary and extracted gates sequentially.
44 `evidence/CORE32_FROZEN_SOURCE.zip` contains the exact proof-gate source inputs
45 without compiled project objects. It is a source snapshot, not a full distribution.
46
47 Each compiler invocation has one worker, warnings as errors, a 4096 MiB internal
48 limit and a 45-second wall limit. Every other gate command retains the 45-second
49 wall bound. The supervisor has a 1800-second total bound. These limits may be
50 unsuitable for slower hosts. A timeout must remain a failed execution rather than
51 being relabeled as a logical rejection or a successful proof run.
52
53 ## Compare completed fresh runs
54
55 After both runs terminate successfully, use the supplied comparison script:
56
57 ```sh
58 python3 scripts/compare_rebuild.py \
59 --final /path/to/primary/evidence/my_replay \
60 --fresh /path/to/extracted/evidence/my_fresh_replay \
61 --snapshot /path/to/CORE32_FROZEN_SOURCE.zip \
62 --out /path/to/comparison.json
63 ```
64
65 The comparison also checks the source tree containing that script against the
66 receipts. Every production object must be byte-identical; a generated nonproduction
67 audit helper may differ only under the explicitly recorded helper boundary. Its
68 source and complete axiom records must still agree. This release includes the current final19/fresh19 proof objects. Earlier compact predecessor objects remain omitted and inventoried as historical omissions.
69
70 ## Adapter on this host
71
72 The direct compiler startup failed with `failed to locate application`. Both accepted gates used the distribution’s preserved `compat/app_path.so` through `LD_PRELOAD`. This adapter supplies executable-path discovery for the host; no proof-kernel modification was made. Example:
73
74 ```sh
75 LD_PRELOAD="$KOMOREBI_LEAN_RUNTIME/compat/app_path.so" python3 scripts/supervise.py --runtime "$KOMOREBI_LEAN_RUNTIME" --out evidence/my_new_replay --whole-timeout 1800
76 ```