ArghDA M8 follow-on: dependency-ordered Coq compilation (M8 → 97%)#50
Merged
Merged
Conversation
Multi-file Coq projects are now checkable. Before this, a bare `coqc B.v` where B `Require`s an in-tree sibling A errored "Cannot find a physical path bound to logical path A" (ground-truthed) — so any Coq file with a local dependency verdicted Error. check_file now stages the target and its in-tree transitive `Require` deps into a temp build tree, compiles the deps in topological order (deps before dependents; `coq_transitive_deps` is a cycle-safe post-order DFS) so each `.vo` exists, then checks the target against `-R <build> ""`. It all happens under temp, so the source tree stays clean. External stdlib/MML requires resolve on coqc's own load path (they're skipped as non-in-tree). Honesty preserved — a transitive admit is NOT whitewashed. Dogfooded: a dependent whose dep contains `Admitted` gets a per-file `check` verdict of `proven` (the dependent's own content is sound), but the reasoning graph demotes its EFFECTIVE verdict to `admitted` via the And-edge to the admitted dep. So dep-ordering makes projects checkable without letting a transitive admit ride through green — the self/effective split does its job. Verification (actually run): cargo fmt --check, clippy -D warnings, cargo test (174 pass, +1 topo-order unit), check-spdx.sh — all green. Dogfooded vs real coqc 8.18.0: a 3-module A←B←C chain of real Qed proofs → `check C.v` = proven; `reason --check` → A/B/C all proven; the admit-taint case demotes as above. Residual (the 3%): `_CoqProject`-driven custom `-Q`/`-R` prefix remapping. The empty-prefix convention (`Foo.Bar` ↔ `Foo/Bar.v` under the root) is fully working; only non-default logical prefixes remain a follow-on. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7
hyperpolymath
marked this pull request as ready for review
July 17, 2026 04:22
hyperpolymath
added a commit
that referenced
this pull request
Jul 17, 2026
## What A theory that imports from another session — `imports "HOL-Library.FuncSet"` — is now checkable. This is the **last** of the heavy-tail completion cuts. Ground-truthed first (the important step): **flat sibling imports already worked** — the adapter stages every sibling `.thy` into the session, so `imports Main Foo` on a sibling `Foo` already resolved. So the real gap was narrower than the milestone text suggested: only *session-qualified* imports. ## How The gap: the generated ROOT said `= HOL +` with no route to `HOL-Library`, so the build errored "Cannot load theory". Fix: `session_prefixes` scans all staged theories' `imports` clauses for qualified `"Session.Theory"` forms (session = the segment before the first `.`; Isabelle session names are dot-free) and emits a `sessions "<S>" …` clause in the generated ROOT, so `isabelle build` pulls those sessions' heaps. The distribution session heaps ship prebuilt, so the build stays fast (~15 s). ## Verification (actually run) - `cargo fmt --check` / `clippy -D warnings` — clean - `cargo test` — **176 pass** (+1 `session_prefixes` unit) - `check-spdx.sh` — OK **Dogfooded vs real Isabelle2025:** | case | result | |---|---| | `Q.thy` importing `"HOL-Library.FuncSet"`, using its Pi-notation | `proven` (was `error` before) | | flat-sibling regression (`Bar` imports sibling `Foo`) | still `proven` | ## Scope M9 → 98%. Residual: a project with its OWN multi-session ROOT (a locally-defined session importing another local session's theories) — niche; single-theory, flat-sibling and distribution-session-qualified imports all work. **This completes the heavy-tail completion cuts** (Coq dependency-ordering #50, Mizar cross-refs #51, Isabelle session-qualified imports). 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7 --- _Generated by [Claude Code](https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7)_ Co-authored-by: Claude <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Multi-file Coq projects are now checkable. Before this, a bare
coqc B.vwhereBRequires an in-tree siblingAerroredCannot find a physical path bound to logical path A(ground-truthed) — so any Coq file with a local dependency verdictedError.How
check_filenow stages the target and its in-tree transitiveRequiredeps into a temp build tree, compiles the deps in topological order (deps before dependents;coq_transitive_depsis a cycle-safe post-order DFS) so each.voexists, then checks the target against-R <build> "". It all happens under temp, so the source tree stays clean. External stdlib/MML requires resolve on coqc's own load path (skipped as non-in-tree).Honesty preserved — a transitive admit is NOT whitewashed
This is the load-bearing verification. Dogfooded: a dependent whose dep contains
Admittedgets a per-filecheckverdict ofproven(the dependent's own content is sound), but the reasoning graph demotes its EFFECTIVE verdict toadmittedvia the And-edge to the admitted dep:So dep-ordering makes projects checkable without letting a transitive admit ride through green — the self/effective split does its job.
Verification (actually run)
cargo fmt --check/clippy -D warnings— cleancargo test— 174 pass (+1 topo-order unit)check-spdx.sh— OKDogfooded vs real coqc 8.18.0:
check C.vin a 3-moduleA ← B ← Cchain of realQedproofsproven(waserrorbefore)reason --checkover the chainprovenAdmittedmoduleproven, effectiveadmittedScope
M8 → 97%. Residual:
_CoqProject-driven custom-Q/-Rprefix remapping (the empty-prefixFoo.Bar↔Foo/Bar.vconvention is fully working; only non-default logical prefixes remain a follow-on).Part of the heavy-tail completion cuts — next: Mizar prel export (M10), then Isabelle multi-session (M9).
🤖 Generated with Claude Code
https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7
Generated by Claude Code