Coq 8.19 #702
Merged
Coq 8.19 #702
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Adapt to coq/coq#17928 (Search uses search_restriction instead of bool)
…arch-pass-sigma Adapt to Coq PR #17987 which adds sigma to the API of search functions
…ecursive definitions as extra arguments.
…ecursive definitions as extra arguments.
…tra-checks-proof-using
gares
commented
Dec 24, 2023
gares
commented
Dec 24, 2023
gares
commented
Dec 24, 2023
|
The source code is ported, the same code (modulo a few ifdefs) works on 8.18 and 8.19. |
|
See also coq/coq#18440 |
gares
commented
Dec 29, 2023
|
I think the nix problem is related to dune. I did have a weird problem using the coq:version variable, see my initial message. |
|
@gares I think we're good ! Would you care to check and merge ? |
|
Although it just dawned on me, why do we need coqc to build @gares ? |
|
I've updated the TODO list up there. |
Make devShells for coq 8.18, coq 8.19 and coq master. Run them all in the CI.
Fixing Coq pin in flake and adding correction to make coq master branch compile.
gares
commented
Feb 6, 2024
Co-authored-by: Enrico Tassi <[email protected]>
gares
commented
Feb 6, 2024
|
Seems we're good on this side ! What's the next step to make coq/coq#18440 happen @gares ? |
|
@gares should I just merge ? I really want to get that next release going to support Coq 8.19 ! |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Since 8.19+rc1 is tagged, I tried to merge coq-master into main, and have a single branch as we discussed.
The only file I ported is language/hover.ml where you can see ppx_optcomp in action.
I have a weird problem with dune 3.5, not the version of the software, which seems required in order to have the
coq:versionvariables, but with(lang dune 3.5)in dune-project. Mysterious sanboxing error.Also nix/flake is broken, I did commit the merge error, since I have no clue.
TODO for CI: