Library coq.kernel replaced by coq-core.kernel in Coq >= 8.14 #4713
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
|
@ejgallego you are probably the most knowledgable on that matter. |
ejgallego
reviewed
Jun 8, 2021
There was a problem hiding this comment.
Great catch @proux01 ! Just in time for 2.9, I hadn't realized about this problem.
The PR looks good, but you need to:
- add a changes entry [place under 2.9]
- update the documentation to state compat guidelines
- add a signed-off-by git header to meet dune's DCO
Additionally, I'd suggest:
- swap the order of resolution, so coq-core is preferred
- move the code to an aux function resolve_first which would take a list and just fold over the result monad, so we can do
resolve_first [ "coq-core.kernel"; "coq.kernel" ]
proux01
force-pushed
the
coq-core-kernel
branch
4 times, most recently
from
8919005 to
3556ae8
Compare
|
Thanks @ejgallego here it is. |
ejgallego
reviewed
Jun 9, 2021
| @@ -96,6 +96,13 @@ let select_native_mode ~sctx ~(buildable : Buildable.t) = | |||
| else | |||
| snd buildable.mode | |||
|
|
|||
| let rec resolve_first lib_db = function | |||
| | [] -> assert false | |||
There was a problem hiding this comment.
You could also use Error (User_error.E (User_error.make ...)) to avoid the assert false here, as this function already returns a Result.t.
There was a problem hiding this comment.
Sorry, what (user) error would you report? This case only happens when calling the function with an empty list, this just doesn't make any sense to me.
Signed-off-by: Pierre Roux <[email protected]>
ejgallego
pushed a commit
to ejgallego/dune
that referenced
this pull request
Jun 19, 2021
…caml#4713) Signed-off-by: Pierre Roux <[email protected]>
ejgallego
added a commit
that referenced
this pull request
Jun 19, 2021
…4713) (#4757) Signed-off-by: Pierre Roux <[email protected]> Co-authored-by: Pierre Roux <[email protected]>
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this pull request
Jun 21, 2021
…ator, dune-private-libs, dune and dune-build-info (2.9-rc1) CHANGES: - Add `(enabled_if ...)` to `(mdx ...)` (ocaml/dune#4434, @emillon) - Add support for instrumentation dependencies (ocaml/dune#4210, fixes ocaml/dune#3983, @nojb) - Add the possibility to use `locks` with the cram tests stanza (ocaml/dune#4480, @voodoos) - Allow to set up merlin in a variant of the default context (ocaml/dune#4145, @TheLortex, @voodoos) - Add `(package ...)` to `(mdx ...)` (ocaml/dune#4691, fixes ocaml/dune#3756, @emillon) - Handle renaming of `coq.kernel` library to `coq-core.kernel` in Coq 8.14 (ocaml/dune#4713, @proux01) - Fix generation of merlin configuration when using `(include_subdirs unqualified)` on Windows (ocaml/dune#4745, @nojb) - Fix bug for the install of Coq native files when using `(include_subdirs qualified)` (ocaml/dune#4753, @ejgallego) - Allow users to specify install target directories for `doc` and `etc` sections. We add new options `--docdir` and `--etcdir` to both Dune's configure and `dune install` command. (ocaml/dune#4744, fixes ocaml/dune#4723, @ejgallego, thanks to @JasonGross for reporting this issue) - Handle renaming of `coq.kernel` library to `coq-core.kernel` in Coq 8.14 (ocaml/dune#4713, @proux01) - Fix issue where Dune would ignore `(env ... (coq (flags ...)))` declarations appearing in `dune` files (ocaml/dune#4749, fixes ocaml/dune#4566, @ejgallego @rgrinberg) - Disable some warnings on Coq 8.14 and `(lang coq (>= 0.3))` due to the rework of the Coq "native" compilation system (ocaml/dune#4760, @ejgallego)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this pull request
Jun 29, 2021
…ator, dune-private-libs, dune and dune-build-info (2.9.0) CHANGES: - Add `(enabled_if ...)` to `(mdx ...)` (ocaml/dune#4434, @emillon) - Add support for instrumentation dependencies (ocaml/dune#4210, fixes ocaml/dune#3983, @nojb) - Add the possibility to use `locks` with the cram tests stanza (ocaml/dune#4480, @voodoos) - Allow to set up merlin in a variant of the default context (ocaml/dune#4145, @TheLortex, @voodoos) - Add `(package ...)` to `(mdx ...)` (ocaml/dune#4691, fixes ocaml/dune#3756, @emillon) - Handle renaming of `coq.kernel` library to `coq-core.kernel` in Coq 8.14 (ocaml/dune#4713, @proux01) - Fix generation of merlin configuration when using `(include_subdirs unqualified)` on Windows (ocaml/dune#4745, @nojb) - Fix bug for the install of Coq native files when using `(include_subdirs qualified)` (ocaml/dune#4753, @ejgallego) - Allow users to specify install target directories for `doc` and `etc` sections. We add new options `--docdir` and `--etcdir` to both Dune's configure and `dune install` command. (ocaml/dune#4744, fixes ocaml/dune#4723, @ejgallego, thanks to @JasonGross for reporting this issue) - Fix issue where Dune would ignore `(env ... (coq (flags ...)))` declarations appearing in `dune` files (ocaml/dune#4749, fixes ocaml/dune#4566, @ejgallego @rgrinberg) - Disable some warnings on Coq 8.14 and `(lang coq (>= 0.3))` due to the rework of the Coq "native" compilation system (ocaml/dune#4760, @ejgallego) - Fix a bug where instrumentation flags would be added even if the instrumentatation was disabled (@nojb, ocaml/dune#4770) - Fix ocaml/dune#4682: option `-p` takes now precedence on environement variable `DUNE_PROFILE` (ocaml/dune#4730, ocaml/dune#4774, @bobot, reported by @dra27 ocaml/dune#4632) - Fix installation with opam of package with dune sites. The `.install` file is now produced by a local `dune install` during the build phase (ocaml/dune#4730, ocaml/dune#4645, @bobot, reported by @kit-ty-kate ocaml/dune#4198) - Fix multiple issues in the sites feature (ocaml/dune#4730, ocaml/dune#4645 @bobot, reported by @Lelio-Brun ocaml/dune#4219, by @Kakadu ocaml/dune#4325, by @toots ocaml/dune#4415)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this pull request
Jul 1, 2021
…ator, dune-private-libs, dune and dune-build-info (2.9.0) CHANGES: - Add `(enabled_if ...)` to `(mdx ...)` (ocaml/dune#4434, @emillon) - Add support for instrumentation dependencies (ocaml/dune#4210, fixes ocaml/dune#3983, @nojb) - Add the possibility to use `locks` with the cram tests stanza (ocaml/dune#4480, @voodoos) - Allow to set up merlin in a variant of the default context (ocaml/dune#4145, @TheLortex, @voodoos) - Add `(package ...)` to `(mdx ...)` (ocaml/dune#4691, fixes ocaml/dune#3756, @emillon) - Handle renaming of `coq.kernel` library to `coq-core.kernel` in Coq 8.14 (ocaml/dune#4713, @proux01) - Fix generation of merlin configuration when using `(include_subdirs unqualified)` on Windows (ocaml/dune#4745, @nojb) - Fix bug for the install of Coq native files when using `(include_subdirs qualified)` (ocaml/dune#4753, @ejgallego) - Allow users to specify install target directories for `doc` and `etc` sections. We add new options `--docdir` and `--etcdir` to both Dune's configure and `dune install` command. (ocaml/dune#4744, fixes ocaml/dune#4723, @ejgallego, thanks to @JasonGross for reporting this issue) - Fix issue where Dune would ignore `(env ... (coq (flags ...)))` declarations appearing in `dune` files (ocaml/dune#4749, fixes ocaml/dune#4566, @ejgallego @rgrinberg) - Disable some warnings on Coq 8.14 and `(lang coq (>= 0.3))` due to the rework of the Coq "native" compilation system (ocaml/dune#4760, @ejgallego) - Fix a bug where instrumentation flags would be added even if the instrumentatation was disabled (@nojb, ocaml/dune#4770) - Fix ocaml/dune#4682: option `-p` takes now precedence on environement variable `DUNE_PROFILE` (ocaml/dune#4730, ocaml/dune#4774, @bobot, reported by @dra27 ocaml/dune#4632) - Fix installation with opam of package with dune sites. The `.install` file is now produced by a local `dune install` during the build phase (ocaml/dune#4730, ocaml/dune#4645, @bobot, reported by @kit-ty-kate ocaml/dune#4198) - Fix multiple issues in the sites feature (ocaml/dune#4730, ocaml/dune#4645 @bobot, reported by @Lelio-Brun ocaml/dune#4219, by @Kakadu ocaml/dune#4325, by @toots ocaml/dune#4415)
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.
mode nativeseems broken with Coq master as it looks forcoq.kernelwhereas onlycoq-core.kernelis listed by ocamlfind.