/reports/phase0_compile.md · raw

Phase 0: compile findings (2026-10-09)

Toolchain: opam 2.5.0, switch bb6, OCaml 4.14.2, Coq 8.20.1 with coq-native (COQ_NATIVE_COMPILER_DEFAULT=yes). Activate with eval $(opam env --switch=bb6).

Framework build

make -j 30 in vendor/busycoq/verify: 79 files, 51 s wall, 0.85 GB peak RSS, exit 0. No tracked files changed.
The Makefile's commented line (#BB52.v ... Skelet* ... Finned* ...) continues with backslashes, so BB5/Skelet/Finned files are not built. Files importing Individual52, Finned, Skelet26, or CounterClass1/* need extra compilation first.

Single-proof compiles (from a temp dir, `-Q verify BusyCoq -Q verify/BigInt BigInt -native-compiler yes`)

File	Result	Wall time	Notes
`Example.v`	OK	2 s	`nonhalt` lemmas live inside modules
`Bouncer_v3.v` (`1LB1RA_0RA0RC_---1RD_1RE1RB_1LF0LE_0RD0LE`)	OK	244 s	needs `ulimit -s unlimited` (stack overflow at default 8 MB); one `Qed` takes 158 s
`Bouncer_v2.v` (`1RB0LB_1RC0LC_1LD1RF_---1LE_0RC1LA_0RB1RA`)	OK	188 s	`Print Assumptions TM1.nonhalt`: Closed under the global context (no axioms)
`1RB1LD_1RC1RE_0LA1LB_0LD1LC_1RF0RA_---0RC.v`	OK	11 s	cryptid-style rule reduction: no `nonhalt` lemma
`1RB0LD_1RC1RF_1LA0RA_0LA0LE_1LD1LA_0RB---.v`	OK	6 s	cryptid-style rule reduction: no `nonhalt` lemma

Gotchas for check_kill.sh

Many accepted proofs wrap everything in Module TM1. ... End TM1., so the theorem is TM1.nonhalt. The checker must locate the lemma (top level or one module deep) and run Print Assumptions on the qualified name.
Small machine-named top-level files are often not kills (cryptid rule reductions with MayHalt-style lemmas). Don't assume a machine-named file proves nonhalt.
-native-compiler yes prints a deprecation warning (harmless). native_compute / native_check_eq are trusted kernel features and do not show up in Print Assumptions.
Always compile with ulimit -s unlimited.

Assumptions baseline

Print Assumptions TM1.nonhalt. for Bouncer_v3.v:

Axioms:
FunctionalExtensionality.functional_extensionality_dep :
  forall (A : Type) (B : A -> Type) (f g : forall x : A, B x),
  (forall x : A, f x = g x) -> f = g

Bouncer_v2.v: Closed under the global context.