Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Library coq.kernel replaced by coq-core.kernel in Coq >= 8.14 #4713

Merged
merged 1 commit into from
Jun 9, 2021
Merged

Library coq.kernel replaced by coq-core.kernel in Coq >= 8.14 #4713

merged 1 commit into from
Jun 9, 2021

Conversation

proux01
Copy link
Contributor

@proux01 proux01 commented Jun 8, 2021

mode native seems broken with Coq master as it looks for coq.kernel whereas only coq-core.kernel is listed by ocamlfind.

@proux01
Copy link
Contributor Author

proux01 commented Jun 8, 2021

@ejgallego you are probably the most knowledgable on that matter.

ejgallego
ejgallego reviewed Jun 8, 2021
View reviewed changes
Copy link
Collaborator

@ejgallego ejgallego left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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" ]

@ejgallego ejgallego added this to the 2.9 milestone Jun 8, 2021
@ejgallego ejgallego added the coq label Jun 8, 2021
@ejgallego ejgallego self-assigned this Jun 8, 2021
@proux01 proux01 force-pushed the coq-core-kernel branch 4 times, most recently from 8919005 to 3556ae8 Compare June 9, 2021 15:29
@proux01
Copy link
Contributor Author

proux01 commented Jun 9, 2021

Thanks @ejgallego here it is.

ejgallego
ejgallego reviewed Jun 9, 2021
View reviewed changes
src/dune_rules/coq_rules.ml
@@ -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
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

ejgallego
ejgallego approved these changes Jun 9, 2021
View reviewed changes
Copy link
Collaborator

@ejgallego ejgallego left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks a lot @proux01 , modulo the optional tweak I suggested this looks great; I will backport this change to 2.9 myself.

@proux01
Library coq.kernel replaced by coq-core.kernel in Coq >= 8.14
75ffdc9 
Signed-off-by: Pierre Roux <pierre.roux@onera.fr>
@ejgallego ejgallego merged commit 269f50a into ocaml:main Jun 9, 2021
@proux01 proux01 deleted the coq-core-kernel branch June 10, 2021 07:45
ejgallego pushed a commit to ejgallego/dune that referenced this pull request Jun 19, 2021
@proux01 @ejgallego
[coq] Library coq.kernel replaced by coq-core.kernel in Coq >= 8.14 (o…
f31b56f 
…caml#4713)

Signed-off-by: Pierre Roux <pierre.roux@onera.fr>
@ejgallego ejgallego mentioned this pull request Jun 19, 2021
Merged
ejgallego added a commit that referenced this pull request Jun 19, 2021
@ejgallego @proux01
[coq] Library coq.kernel replaced by coq-core.kernel in Coq >= 8.14 (#…
bb3a234 
…4713) (#4757)

Signed-off-by: Pierre Roux <pierre.roux@onera.fr>

Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
@ejgallego ejgallego mentioned this pull request Jun 21, 2021
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Jun 21, 2021
@ejgallego
[new release] dune-action-plugin, dune-glob, dune-site, dune-configur…
da0714f 
…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
@ejgallego
[new release] dune-action-plugin, dune-glob, dune-site, dune-configur…
a13f842 
…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
@ejgallego
[new release] dune-action-plugin, dune-glob, dune-site, dune-configur…
96c14a5 
…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
Reviewers

@ejgallego ejgallego ejgallego approved these changes

Assignees

@ejgallego ejgallego

Labels
coq
Projects
Coq + Dune
Archived in project
Milestone
2.9
Development

Successfully merging this pull request may close these issues.
2 participants
@proux01 @ejgallego