Skip to content

Accept dev versions of coq, coq-compcert and coq-flocq in coq-vst.opam#861

Open
JasonGross wants to merge 1 commit into
PrincetonUniversity:masterfrom
JasonGross:opam-allow-rocq-dev
Open

Accept dev versions of coq, coq-compcert and coq-flocq in coq-vst.opam#861
JasonGross wants to merge 1 commit into
PrincetonUniversity:masterfrom
JasonGross:opam-allow-rocq-dev

Conversation

@JasonGross

Copy link
Copy Markdown
Contributor

Allows installing a pin to this branch on a switch tracking Rocq master

Allows installing on a switch tracking Rocq master (e.g. pinned
rocq-core dev builds); release constraints are unchanged.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw
@JasonGross

JasonGross commented Jul 16, 2026

Copy link
Copy Markdown
Contributor Author

@JasonGross can you explain further? How is this branch going to track the master branch? Will you have to fastforward from time to time? And why need a P.R. instead of just a fork branch?

Originally posted by @andrew-appel in #860 (comment)

This is not strictly needed on master, as one can use the version in the opam repo. However, if we want to, e.g., opam pin add git+https://github.com/PrincetonUniversity/VST.git#some-branch and have that work on rocq dev, that branch would need to adjust the opam file.

The particular workflow this is useful to me for is:

  1. fork VST, create a branch with a fix
  2. open a PR to PrincetonUniversity/VST with the fix
  3. point my opam setup at my branch in the meantime, so as to not block development of things depending on VST
  4. if/when the PR is merged, repoint opam back at upstream VST

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