Skip to content

Fix install phases for migrated and legacy dev packages - #3793

Merged
JasonGross merged 5 commits into
rocq-prover:masterfrom
theorem-labs:codex/dev-install-phase
Jul 31, 2026
Merged

Fix install phases for migrated and legacy dev packages#3793
JasonGross merged 5 commits into
rocq-prover:masterfrom
theorem-labs:codex/dev-install-phase

Conversation

@JasonGross

@JasonGross JasonGross commented Jul 28, 2026 •
edited
Loading

Copy link
Copy Markdown
Member

Summary

Move make install from build: to opam’s dedicated install: phase for these migrated/legacy dev packages:

  • coq-additions.dev
  • coq-dictionaries.dev
  • coq-ieee754.dev
  • coq-euler-formula.dev
  • coq-qarith.dev
  • coq-hardware.dev
  • coq-int-map.dev
  • coq-mod-red.dev
  • coq-zsearch-trees.dev
  • coq-zchinese.dev
  • coq-float.dev
  • coq-bdds.dev
  • coq-smc.dev

Also remove the obsolete ./configure.sh invocation from coq-mathcomp-grobner.dev and use its current source recipe (make, then make install in the install phase).

Why

With opam 2.5 sandboxing, the switch prefix is read-only during build:. These packages compile successfully but then fail when build-phase make install attempts to write under %{lib}%/coq/user-contrib. Grobner fails earlier because its current source tree no longer contains configure.sh; its Makefile generates Makefile.coq directly.

Validation

  • opam lint passes on every edited file under the opam 2.1.2 that .gitlab-ci.yml
    pins (2.5.1 does not reproduce that stage's error 67)
  • git diff --check
  • coq-mathcomp-grobner.dev now resolves under both opam 2.1.2 and 2.5.1 against
    CI's repo set (core-dev + extra-dev + default)

Correction to an earlier version of this description

An earlier revision of this body claimed that all 14 packages install successfully
against Rocq dev, and that coq-mathcomp-grobner builds grobner.vo against Rocq
dev. Neither claim holds, and CI disagrees with both:

  • Every legacy package CI reached fails to build. coq-int-map requires the
    removed Ndigits stdlib library; coq-hardware and coq-additions have Make
    files using -extra, which modern coq_makefile rejects; coq-bdds fails only
    because coq-int-map does.
  • The grobner claim was verified against upstream master, while the recipe at the
    time still pinned the 2016 v1.0.1 tarball, which has no Makefile at all. Upstream
    master builds fine on Rocq 9.2 with multinomials 2.4.0 but fails on 9.4+alpha in
    ideal_mem at grobner.v:113 with No assumption in (p = ...).

Known-broken sources, not fixed here

The install-phase move is necessary but not sufficient. These packages track
coq-contribs masters frozen in the Coq 8.x era and their sources do not compile
against Rocq dev at all. Because scripts/opam-coq-list-pr-files restricts the build
stage to the files a PR changed, that pre-existing breakage surfaces as this PR's red
pipeline. The metadata fix is still correct and worth having on its own.

coq-mathcomp-grobner.dev additionally depends on rocq-elpi.dev, which is currently
unbuildable for an unrelated reason (dune 3.24 deleted the coq extension); that is
fixed by #3806.

ci-skip: coq-additions coq-bdds coq-dictionaries coq-euler-formula coq-float coq-hardware coq-ieee754 coq-int-map coq-mathcomp-grobner coq-mod-red coq-qarith coq-smc coq-zchinese coq-zsearch-trees

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.

@JasonGross JasonGross changed the title Run migrated contrib installs in opam install phase Fix install phases for migrated and legacy dev packages Jul 28, 2026
JasonGross and others added 5 commits July 31, 2026 19:22
@JasonGross
Run migrated contrib installs in opam install phase
a4ab9ee
@JasonGross
Run dev package installation in opam install phase
3d02691
@JasonGross
Run BDDs and SMC installation in opam install phase
d60380d
@JasonGross @claude
Fix coq-mathcomp-grobner.dev lint error and restore Makefile generation
698e692 
Two problems in coq-mathcomp-grobner.dev, both surfaced by this branch:

* opam lint fails with `error 67: Checksum specified with a non archive
  url` under the opam version CI uses (2.1.2, pinned in .gitlab-ci.yml),
  which does not classify a `.zip` as an archive.  The defect is
  pre-existing on master; it only became visible here because
  scripts/opam-coq-list-pr-files lints just the files a PR touches.
  Switch to the `.tar.gz` of the same tag and record its sha256.  The
  recorded md5 of the zip was correct, so this is a format change only.

* Dropping the `./configure.sh` build step left the package with no
  Makefile.  The v1.0.1 tarball ships only `Make`, `configure.sh` and
  `grobner.v`, and `configure.sh` is exactly
  `coq_makefile -f Make -o Makefile`, so `make` had nothing to run.
  Generate the Makefile directly, as the other packages on this branch
  already do.

Verified with the pinned opam 2.1.2 and CI's exact invocation
(`opam lint --warn=-21 --check-upstream`, which re-downloads and checks
the new checksum): all 14 files touched by this branch now lint clean,
leaving only warnings.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
@JasonGross @claude
Track upstream master in coq-mathcomp-grobner.dev
d96f355 
The recipe pinned the 2016 v1.0.1 tarball, which is wrong for a .dev
package and was unsatisfiable besides: it required
coq-mathcomp-multinomials = "1.6.dev", a version that no longer exists
in the archive (only 1.5.1 and dev do), so CI reported the package under
"Packages that can never be installed".  That constraint is pre-existing
on master; it only became visible now because CI lints and builds just
the files a PR touches.

Point the url at thery/grobner#master and adopt the dependency
constraints from upstream's own coq-grobner.opam (coq >= 9.0,
mathcomp ssreflect/algebra >= 2.5.0, multinomials >= 2.4.0).  Upstream
master carries a Makefile that generates Makefile.coq from _CoqProject,
so the plain "make" build plus install-phase "make install" from this
branch is the correct recipe there and the coq_makefile invocation
needed by the v1.0.1 tarball can go away.  The url is now a git source,
which also removes the checksum-on-non-archive-url lint error.

Verified: opam lint passes under the opam 2.1.2 that CI pins, and the
dependency set is solvable under both opam 2.1.2 and 2.5.1 against
core-dev + extra-dev + default (the repo set CI uses).

Not fixed by this commit: grobner's source does not compile against
Rocq dev.  Upstream master builds fine on Rocq 9.2 with multinomials
2.4.0, but on 9.4+alpha it fails in ideal_mem at grobner.v:113 with
"No assumption in (p = ...)" from ssreflect's decompose_assum.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
@JasonGross
JasonGross force-pushed the codex/dev-install-phase branch from d7e9625 to d96f355 Compare July 31, 2026 19:22
@JasonGross
JasonGross marked this pull request as ready for review July 31, 2026 20:59
@JasonGross
JasonGross merged commit b3b1ff6 into rocq-prover:master Jul 31, 2026
3 checks passed
@JasonGross JasonGross mentioned this pull request Aug 11, 2026
Merged
JasonGross added a commit that referenced this pull request Aug 11, 2026
@JasonGross @claude
Run the remaining dev package installs in opam's install phase (#3825)
67e0386 
Nine extra-dev recipes still call `make install` from `build:` and carry
no `install:` field, so the install runs under opam's build sandbox
rather than its install sandbox.  Under a sandboxed opam the build phase
has no write access to the switch prefix, so these rows cannot install:
`make install` fails, or worse, silently installs nothing while the
build reports success.

This is the same defect and the same mechanical fix as #3793, which
cleared 14 of the 23 extra-dev rows that had it.  These nine are the
residue; after this commit the class is empty under extra-dev/.  The
edit is identical in every file: drop `[make "install"]` from the tail
of `build:` and add `install: [make "install"]` immediately after.
Nothing else changes -- no dependency, bound, url or remove: field is
touched.

  coq-algebra.dev
  coq-distributed-reference-counting.dev
  coq-fermat4.dev
  coq-hoare-tut.dev
  coq-jordan-curve-theorem.dev
  coq-maths.dev
  coq-orb-stab.dev
  coq-tree-automata.dev
  coq-universe-comparator.1.0.1

Tested: coq-tree-automata.dev installs on a Rocq dev switch with exactly
this split and does not without it.  The other eight are not
individually build-tested against a dev prover -- several have other,
unrelated reasons not to build there -- so this commit is a fix to the
recipes' install phase, not a claim that the nine packages build.


Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@JasonGross