ci(rocq): pre-cppo plugin sources to bypass dune multiple-rules error#42
Open
alpaylan wants to merge 4 commits into
Open
ci(rocq): pre-cppo plugin sources to bypass dune multiple-rules error#42alpaylan wants to merge 4 commits into
alpaylan wants to merge 4 commits into
Conversation
QuickChick's plugin/dune declares (rule (targets X.ml) (deps X.ml.cppo)) for several modules. With (modules :standard) in the same stanza, dune considers both the .ml.cppo source AND the rule output as candidates for X.ml — fails with "Multiple rules generated for ..._build/.../X.ml: file present in source tree, plugin/dune:31". Pre-running cppo and rewriting plugin/dune from scratch (drop cppo rules, keep the four coqpp rules) eliminates the conflict. Bump cache key v3→v4 to invalidate poisoned ~/.opam from prior failed runs. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Surfaced after the cppo fix unblocked the QuickChick build — coq-simple-io.1.11.0 fails on coq.8.18 + dune 3.x with: Error: Can't find file coqsimpleio_plugin.cmxs on loadpath. The plugin built by simple-io's own dune isn't visible on coqc's loadpath when SimpleIO_Plugin.v compiles. 1.10.0 (older layout) installs cleanly. quickchick depends on simple-io so we pre-install 1.10.0 before pulling quickchick. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Surfaced after the simple-io pin unblocked installation — opam's coq-quickchick build runs `make compat` (a Makefile target in the property-language tree) which lists plugin/depDriver.ml etc. as deps via a pattern rule `%: %.cppo`. Deleting the .cppo source breaks make's dep resolution: make: *** No rule to make target 'plugin/depDriver.ml', needed by 'compat'. Stop. Keep both forms — the .ml is what dune compiles (no cppo rule in our rewritten plugin/dune), and the .cppo placates make. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1.10.0 succeeds in isolation locally (coq.8.18 + cppo only) but fails on CI under the full opam stack (coq-elpi + mathcomp + etc.): Error: Can't find file coqsimpleio_plugin.cmxs on loadpath. Try 1.9.0 — known to predate the dune-layout regression.
alpaylan
force-pushed
the
rocq-precompile-cppo
branch
from
4d9b4c9 to
389f882
Compare
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.
Summary
QuickChick's
plugin/dunedeclares(rule (targets X.ml) (deps X.ml.cppo))for several modules. With(modules :standard)in the same stanza, dune (2.x and 3.x both) considers both the.ml.cpposource AND the rule output as candidates forX.ml, then bails withMultiple rules generated for ..._build/.../X.ml: file present in source tree, plugin/dune:31. Earlier attempts (build-dir purge, cache invalidation, dune 2.9.3 pin) all failed.This PR pre-runs cppo on all
.cppofiles inplugin/and rewritesplugin/dunefrom scratch — drops the cppo rules, keeps only the four coqpp.mlg → .mlrules and thevoid_for_linkingwrite-file rule. Cache key bumped v3 → v4 to invalidate any poisoned~/.opamfrom prior failed runs.Test plan
etna-rocq-bstcoq-quickchickinstalls without "Multiple rules" error