Skip to content

Add missing analysis dependency to experimental reals dev package - #3789

Merged
JasonGross merged 1 commit into
rocq-prover:masterfrom
theorem-labs:codex/experimental-reals-analysis-dep
Aug 6, 2026
Merged

Add missing analysis dependency to experimental reals dev package#3789
JasonGross merged 1 commit into
rocq-prover:masterfrom
theorem-labs:codex/experimental-reals-analysis-dep

Conversation

@JasonGross

@JasonGross JasonGross commented Jul 28, 2026

Copy link
Copy Markdown
Member

The development version of coq-mathcomp-experimental-reals now imports mathcomp.esum, mathcomp.ereal, and mathcomp.numfun. Those modules live in the coq-mathcomp-analysis package, but the opam metadata did not declare that dependency, allowing the experimental-reals build to start before analysis was available.

Add the matching-version analysis dependency so opam orders these builds correctly.

Validation: opam lint passes for the updated package. The observed build failure was Unable to locate library esum with prefix mathcomp; the analysis development package was concurrently still building, confirming the missing dependency edge. Full source validation will follow once that long-running dependency build completes.

Authorship note: this was researched and written by an AI coding agent
(OpenAI Codex), working on Jason Gross's behalf; Jason reviews what is
posted from this account.


CI note. Rebased onto master. The opam-build:4.09.0 failure this PR was showing was rocq-runtime.9.3.dev dying at ./configure with "You need OCaml 4.14.0 or later"; that is fixed in master by #3803, so the rebase clears it. An earlier revision of this branch also carried a dune < 3.24 bound for rocq-elpi.dev and rocq-micromega-plugin.dev; that has been split out into #3806 so this PR is the one-line dependency fix only.

Update (rebased again). #3806 has merged, so the elpi/micromega dune < 3.24 bound is now in master. This branch is rebased on top of it; the opam-build:4.14.2 and 5.3.0 failures were mathcomp-analysis pulling in rocq-elpi.dev, so they should clear too.

@JasonGross
JasonGross force-pushed the codex/experimental-reals-analysis-dep branch from 18f881f to 885f2e6 Compare July 31, 2026 19:45
@JasonGross
JasonGross marked this pull request as ready for review August 6, 2026 04:08
@JasonGross
JasonGross merged commit 71fa852 into rocq-prover:master Aug 6, 2026
3 checks passed
@JasonGross
JasonGross deleted the codex/experimental-reals-analysis-dep branch August 6, 2026 04:08
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant