Skip to content

extra-dev: coq-prosa compatibility shim for rocq-prosa - #3822

Merged
JasonGross merged 1 commit into
rocq-prover:masterfrom
JasonGross:coq-prosa-dev-shim
Aug 10, 2026
Merged

extra-dev: coq-prosa compatibility shim for rocq-prosa#3822
JasonGross merged 1 commit into
rocq-prover:masterfrom
JasonGross:coq-prosa-dev-shim

Conversation

@JasonGross

Copy link
Copy Markdown
Member

Split out of #3821, which adds the same shim for four other packages. Opened as a
draft because this row is expected to be red, and not because of the shim.

coq-prosa has no .dev row while its twin rocq-prosa does, and both install to
logpath:prosa. So on a dev switch there is nothing at the coq-prosa name that
resolves without overwriting the twin's files. This adds a coq-prosa.dev that
installs no files of its own and only depends on rocq-prosa {= version} — the same
shape as the 14 coq-*/rocq-* pairs already in extra-dev that are wrapped this
way (coq-mathcomp-*, coq-equations, coq-elpi, coq-hierarchy-builder, ...).

Why it is red

The pre-existing rocq-prosa.dev does not build against the dev prover. CI builds a
changed package's dependencies, so adding a dependency on it is enough to surface the
failure. Both legs of #3821 (4.14.2 and 5.3.0) resolved rocq-prosa at dev and died
inside its own sources:

[ERROR] The compilation of rocq-prosa.dev failed at "make -j2".
File "./util/tactics.v", line 125, characters 21-35:
Error: The reference ssreflect.done was not found in the current environment.
Did you mean ssreflect.hide, ssreflect.phant, ssreflect.hideT or ssreflect.Phant?
make[2]: *** [Makefile.coq:868: util/tactics.vo] Error 1

Nothing in this PR touches rocq-prosa.dev; the diff is one new file. The shim will
go green as soon as rocq-prosa builds at dev, at which point this can be undrafted
and merged as-is.

🤖 Generated with Claude Code

https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b

Split out of rocq-prover#3821 so that the four shims whose dependency builds at dev
can merge on a green CI.

This row is expected to be RED for now, and not because of the shim: the
pre-existing rocq-prosa.dev does not build against the dev prover.  Both
CI legs of rocq-prover#3821 (4.14.2 and 5.3.0) resolved rocq-prosa at dev and failed
inside its own sources:

  File "./util/tactics.v", line 125, characters 21-35:
  Error: The reference ssreflect.done was not found in the current environment.

The shim itself installs no files and only adds a dependency, so it will
go green as soon as rocq-prosa builds at dev.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
@JasonGross
JasonGross marked this pull request as ready for review August 10, 2026 16:03
@JasonGross
JasonGross merged commit 3e40179 into rocq-prover:master Aug 10, 2026
2 of 5 checks passed
@JasonGross
JasonGross deleted the coq-prosa-dev-shim branch August 10, 2026 16:03
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