[build] Bump minimal dune version to 3.6.1 #18359
Merged
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
coqbot-app
bot
added
the
needs: full CI
ejgallego
added
part: build
|
Unfortunately due to ocaml/dune#6545 , we either rework quite a few opens in the codebase, or bump to 3.6.1. |
|
Here's an example of pitfalls of testing vs versioning of the build language, as Coq didn't bump the Dune version, the bug wasn't detected at 3.5.0 release time. |
ejgallego
changed the title
|
The patch says 3.6.1 here and 3.6.0 there. Which is the right one? |
|
@coqbot run full CI |
coqbot-app
bot
removed
the
needs: full CI
ejgallego
changed the title
Indeed 3.5.0 and 3.6.0 are buggy and cannot build Coq if We'll have to tweak this in the |
ejgallego
added
needs: fixing
coqbot-app
bot
added
the
needs: full CI
|
Dep for |
|
@coqbot run full CI |
coqbot-app
bot
removed
the
needs: full CI
|
@coqbot run full CI |
|
This seems ready too, anyone willing to assign? |
SkySkimmer
added
the
needs: rebase
|
Dune 3.6.1 is from 2022-11-24, debian testing has 3.11.1, should be fine to require 3.6.1. |
SkySkimmer
approved these changes
Dec 8, 2023
coqbot-app
bot
added
needs: full CI
github-actions
bot
added
the
needs: rebase
This brings mainly improvements into the directory target feature, so we can go ahead with packaging the docs properly. Note some fixes in documentation, plus now Dune enables some more warnings by default that we address in the following way: - warning 67 [unused functor parameter]: we make the arguments anonymous as OCaml seems to recommend - warning 69 [unused-field]: we disable this warning, but should be maybe enabled and handled again. It seems that most of the triggers for this warning are legit, however the situation is delicate due to some parts of the code involved using `Obj.magic` or `Marshall`. Also quite a few of these warnings are in code that is scheduled for removal at some point. Note that we couldn't bump to 3.5 directly due to ocaml/dune#6545
ejgallego
added
the
request: full CI
coqbot-app
bot
removed
needs: rebase
|
@coqbot merge now |
SkySkimmer
added a commit
to SkySkimmer/coq
that referenced
this pull request
Dec 14, 2023
coqbot-app bot
added a commit
that referenced
this pull request
Dec 15, 2023
Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
JasonGross
added a commit
to JasonGross/coq-packaging
that referenced
this pull request
Dec 21, 2023
JasonGross
added a commit
to JasonGross/coq-packaging
that referenced
this pull request
Dec 21, 2023
JasonGross
reviewed
Dec 22, 2023
| @@ -27,7 +27,7 @@ homepage: "https://coq.inria.fr/" | |||
| doc: "https://coq.github.io/doc/" | |||
| bug-reports: "https://github.com/coq/coq/issues" | |||
| depends: [ | |||
| "dune" {>= "2.9"} | |||
| "dune" {>= "3.6" & >= "3.6.1"} | |||
There was a problem hiding this comment.
Why is it written like this instead of just >= "3.6.1"?
There was a problem hiding this comment.
As we declare (lang dune 3.6) dune adds automatically the dune >= 3.6 lower bound when auto-generating the opam file, then our bound is added, as 3.6.0 contains a bug fatal to Coq.
louiseddp
pushed a commit
to louiseddp/coq
that referenced
this pull request
Feb 27, 2024
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.
This brings mainly improvements into the directory target feature, so we can go ahead with packaging the docs properly.
Note some fixes in documentation, plus now Dune enables some more warnings by default that we address in the following way:
warning 67 [unused functor parameter]: we make the arguments anonymous as OCaml seems to recommend
warning 69 [unused-field]: we disable this warning, but should be maybe enabled and handled again. It seems that most of the triggers for this warning are legit, however the situation is delicate due to some parts of the code involved using
Obj.magicorMarshall. Also quite a few of these warnings are in code that is scheduled for removal at some point.Note that we couldn't bump to 3.5 due to
ocaml/dune#6545