Require (safe): Import/Export + dependency propagation (combined) - #29
Draft
JasonGross wants to merge 6 commits into
Draft
Require (safe): Import/Export + dependency propagation (combined)#29JasonGross wants to merge 6 commits into
JasonGross wants to merge 6 commits into
Conversation
…rt support The kernel-structure walk that pushes fully-qualified names for a Require(safe) library used to live in library.ml. Move it into declaremods.ml so that Import/Export of a safe-loaded library can reuse it. The walk is parameterized by a visibility function computed from the module-nesting depth: at load time it pushes at Until (fully-qualified names only, as a plain Require(safe) should), at import time at Exactly (k-1), matching the depth open_object uses for the same object during a normal Import so that a top-level constant becomes visible under its bare name. The top library module name is not re-pushed on import, mirroring normal library import. A safe-loaded library has no ModObjs entry, so the usual object-collection import machinery cannot import it. Record safe-loaded libraries per stage (SafeLibs, storing the module body since it cannot be recovered from the kernel at the Synterp stage) and branch in collect_module: when the module path is an MPfile registered safe, push its short (Exactly) names directly instead of collecting/opening libobjects. This makes standalone Import/Export vernacs work on safe-loaded libraries and takes precedence over the missing ModObjs entry. Filters/categories are ignored since there are no libobjects to filter. library.ml now drives declaremods via register_safe_library and keeps only its own bookkeeping (libraries_table / native / loaded-list). Co-Authored-By: Claude Fable 5 <[email protected]> Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw
Extend the Require(safe) grammar with an optional Import/Export token (including the From ... form). No import_categories or import filters are accepted for the safe form: they filter libobjects, which safe-require does not create; only bare qualids plus an optional Import/Export. VernacSafeRequire / EVernacSafeRequire now carry an export_flag option. Export is routed through the same import_module path a normal Require Export uses (recording the standard ExportObject), so the Declaremods safe-import branch is reached both immediately and on later re-export. Co-Authored-By: Claude Fable 5 <[email protected]> Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw
output/SafeRequireImport.v covers, in a single session: - plain Require(safe) exposes only qualified names (bare flip fails to resolve, CRelationClasses.flip does); - a standalone Import on an already safe-loaded library exposes the bare names (exercises the safe branch of Declaremods' import machinery, which has no ModObjs entry to collect); - Require(safe) Import exposes bare names immediately; - Require(safe) Export behaves like Import for the current session (the same-session ExportObject path); - the From ... Require(safe) Import form parses and imports; - a plain Require of a safe-imported library still errors. Co-Authored-By: Claude Fable 5 <[email protected]> Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw
A library compiled with [Require (safe) M] now keeps M (and, through M, its safe dependencies) safe for its downstream users: a plain [Require] of such a library loads it fully but only safe-loads the dependencies it had itself safe-required. The set of safe-required direct dependencies is recorded in each vo summary ([md_safe_deps], threaded into [library_t.library_safe_deps] and mirrored in the checker's summary type + [v_libsum]). At require time the whole dependency closure is interned first, then a per-library effective mode is computed as a monotone fixpoint: roots get the command mode, a library is full iff it is reachable from a full root through normal (i.e. non-safe) edges, otherwise it is safe-loaded. The topologically-ordered closure is registered through a single require object carrying each library's mode, so full/safe registrations interleave in dependency order and the all-full case replays objects exactly as before. In-session conflicts are unchanged: a full demand reaching a previously-safe-required library still errors, reported (as before) on the first such library a plain require would reach. Co-Authored-By: Claude Fable 5 <[email protected]> Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw
Add test-suite/misc/safe-require-propagation: A safe-requires CMorphisms (which depends on CRelationClasses); requiring A fully must keep CRelationClasses safe (no implicit arguments, and a plain require of it is still rejected), while fully requiring CRelationClasses before A keeps it fully loaded. Co-Authored-By: Claude Fable 5 <[email protected]> Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw
Add test-suite/misc/safe-require-export-import, an integration test that only passes when both Require (safe) Import/Export support and safe-dependency propagation are present. A does [Require (safe) Export CRelationClasses], so its .vo both records CRelationClasses as a safe dependency (propagation) and carries the standard ExportObject that re-exports it (import/export support). B requires A fully: propagation keeps CRelationClasses safe in B, so before [Import A] only its fully-qualified names resolve. [Import A] replays the ExportObject, whose import of the safe-loaded CRelationClasses reaches the safe branch of Declaremods' import machinery (no ModObjs entry to collect) and pushes the short names. B then checks the short name resolves, that CRelationClasses is still only safe-loaded (About shows no implicit arguments), and that a plain require of it is still rejected. Without propagation a plain [Require A] would fully load CRelationClasses (About would show implicit arguments and the final [Fail Require] would not fail); without import/export support [Import A] would find no safe short-name walk. The test is thus meaningful only on the combined branch. Co-Authored-By: Claude Fable 5 <[email protected]> Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw
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
1 participant
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.
Combined follow-up for rocq-prover#22291 against your
safrequirebranch: the Import/Export offer and the dep-propagation offer reconciled on one branch (they conflict — both restructure the safe-registration path).Reconciliation: propagation's unified mode-dispatching require objects are the single mechanism; the ModeSafe path calls the relocated
Declaremods.{Synterp,Interp}.register_safe_library(which also feeds theSafeLibsregistry that Import/Export needs — including for safe libs pulled in transitively by a plainRequire).VernacSafeRequirecarries both the export flag and mode-annotated interning results.The combination unlocks an integration test impossible on either branch alone (misc/safe-require-export-import): A.v does
Require (safe) Export CRelationClasses; B.v doesRequire AthenImport A— the ExportObject replay hits the safe path downstream because propagation kept the lib safe in B's session, and short names appear while the lib stays safe (verified to fail on the import-export branch alone, whereRequire Afully loads the dep).All green:
make world, base SafeRequire + SafeRequireImport + propagation tests + the new integration test, full modules/coqchk/misc/output groups.Supersedes the two individual PRs if you want both features.
Written by Claude (Anthropic AI) at the request of and under the supervision of @JasonGross.
🤖 Generated with Claude Code
https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw