Repository navigation
fix(rocq): restrict Corelib dependencies to its theories directory - #16545
Open
pgiarrusso-sl wants to merge 2 commits into
Open
pgiarrusso-sl wants to merge 2 commits into
pgiarrusso-sl wants to merge 2 commits into
Conversation
Extend the merged broken-symlink fixture with Corelib-disabled controls, selected parent and child namespaces, and objects directly in Corelib's root. Exercise absolute-PATH and Dune-managed compilers, ROCQPATH, and a child project reading its parent's build installation. The fake compiler reports no imports so missing objects expose Dune's installed-theory dependencies independently of Rocq compilation. Preserve upstream's observed failures in this test-only commit, with caching enabled. Validation: make dev, @check, @fmt, and the expanded Cram fixture pass. Full @runtest is not green in the prepared local environment: dune-site's run_2_9.t has byte-for-byte identical failure diagnostics with the Rocq module restored to upstream main. Commit with the approved exception to the full-suite gate; no tests disabled or failure outputs promoted.
Collect implicit Corelib objects from COQLIB/theories instead of all of COQLIB, which incorrectly included unrelated user-contrib objects. Include objects directly in theories as well as its subdirectories when narrowing the scan. Leave selected legacy theories and ROCQPATH discovery unchanged. Flip the merged broken-symlink regression and the parent-install/child-root control to success. The preceding characterization commit retains controls for missing Corelib objects, selected legacy subtrees, and compiler lookup. Validation: make dev, dune fmt, @check and @fmt pass. The expanded regression and compose-installed-rebuild.t / compose-installed-sub.t pass, with caching enabled in the broken-symlink fixture. Full @runtest remains blocked locally by dune-site run_2_9.t; restoring the Rocq module to upstream main and rebuilding reproduces byte-for-byte identical failure diagnostics.
This branch has not been deployed
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
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.
Description
In the Rocq support, scanning for Corelib's
.vofiles includesuser-contrib, not justtheories, and can add dependencies to broken symlinks. Restrict the scan totheories.Suggested by Codex, endorsed by @rlepigre-skylabs-ai for submission.
Related Issue and Motivation
See #16544 and #16326.
Checklist
From Codex GPT-6.1 Sol (high)
An implicit Corelib dependency currently collects
.vofiles from all of COQLIB, including unrelated user-contrib theories. A dangling object in an unrelated theory can therefore prevent a build that requests only a healthy installed theory.Scan
COQLIB/theoriesfor Corelib, retaining both direct and nested objects. The correction preserves root-level objects that the first narrow-scan implementation accidentally omitted. Selected legacy theories and ROCQPATH keep their existing dependency behavior.This draft is stacked on the characterization branch. It changes the merged regression and the parent-install/child-project control from failure to success; the other controls retain their observed outcomes. A broken unimported descendant of a selected legacy parent still fails, so this change does not claim to solve installation-readiness races generally.
Validation:
make dev,dune fmt,@check,@fmt, the expanded fixture, and the realcompose-installed-rebuild.t/compose-installed-sub.tneighbors pass. Full@runtestremains blocked locally bydune-site/run_2_9.t; restoring the Rocq module to upstream main and rebuilding reproduces byte-for-byte identical diagnostics.Draft for review within this fork. Changelog and upstream submission are deferred until this review is complete.