Skip to content

Adapt to rocq-prover/rocq#21063 (fixed apply auto-projecting from record with letin projection)#837

Merged
andrew-appel merged 1 commit intoPrincetonUniversity:masterfrom
SkySkimmer:fix-apply-nreal
Sep 22, 2025
Merged

Adapt to rocq-prover/rocq#21063 (fixed apply auto-projecting from record with letin projection)#837
andrew-appel merged 1 commit intoPrincetonUniversity:masterfrom
SkySkimmer:fix-apply-nreal

Conversation

@SkySkimmer
Copy link
Contributor

Should be backwards compatible

@ppedrot
Copy link
Contributor

ppedrot commented Sep 12, 2025

CI is green so this is indeed backwards compatible. Please merge already.

@SkySkimmer
Copy link
Contributor Author

ping @andrew-appel

@ppedrot
Copy link
Contributor

ppedrot commented Sep 22, 2025

Ping @andrew-appel

@andrew-appel andrew-appel merged commit 12921c5 into PrincetonUniversity:master Sep 22, 2025
23 checks passed
@andrew-appel
Copy link
Collaborator

Now that this has been merged, VST's own CI fails in the dev branch:
https://github.com/PrincetonUniversity/VST/actions/runs/17916506780/job/50940016368

<><> Updating package repositories ><><><><><><><><><><><><><><><><><><><><><><>
  [prerelease] no changes from file:///github/workspace/opam-prerelease
  Error:  Could not update repository "rocq-extra-dev": OpamDownload.Download_fail(_, "curl failed: \"/usr/bin/curl --write-out %{http_code}\\\\n --retry 3 --retry-delay 2 --user-agent opam/2.3.0 -L -o /tmp/opam-12-871e96/index.tar.gz.part -- [https://rocq-prover.org/opam/extra-dev/index.tar.gz\](https://rocq-prover.org/opam/extra-dev/index.tar.gz/)" exited with code 35")

Do either of you have any advice about how to fix this?

@SkySkimmer SkySkimmer deleted the fix-apply-nreal branch September 22, 2025 14:08
@SkySkimmer
Copy link
Contributor Author

Seems like a network error, retry the job?

@andrew-appel
Copy link
Collaborator

Yes, that was it. Thank you.

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.

3 participants