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

[coq] make expand "coq.version" and co not depend on coq-stdlib #10631

Merged
merged 6 commits into from
Jun 30, 2024
Merged

[coq] make expand "coq.version" and co not depend on coq-stdlib #10631

merged 6 commits into from
Jun 30, 2024

Conversation

gares
Copy link
Contributor

@gares gares commented Jun 9, 2024

fix #10629

@gares gares mentioned this pull request Jun 9, 2024
Merged
@ejgallego ejgallego requested a review from Alizter June 10, 2024 13:07
@ejgallego ejgallego added the coq label Jun 10, 2024
ejgallego
ejgallego reviewed Jun 10, 2024
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 for the patch, indeed it seems very useful!

I'll let @Alizter review first, as he is the expert on this code.

Can you add changelog meanwhile (add a new file in doc/changes)

@gares
Copy link
Contributor Author

gares commented Jun 11, 2024

@Alizter please take a look at
https://github.com/ocaml/dune/pull/10631/files#diff-3d90c4b942eed2beaba48d8cbbd71cbe1ce22b6b7a61ea76999e92cf0a9a13e8
you are already testing this for coq 8.16

@Alizter
Copy link
Collaborator

Alizter commented Jun 11, 2024

@gares Thanks, I forgot all the details there. I will take a closer look at this PR soon.

@gares
Copy link
Contributor Author

gares commented Jun 27, 2024

ping

@ejgallego
Copy link
Collaborator

@Alizter you want to review this?

Alizter
Alizter reviewed Jun 27, 2024
View reviewed changes
doc/changes/10631.md Outdated Show resolved Hide resolved
src/dune_rules/coq/coq_config.mli Show resolved Hide resolved
test/blackbox-tests/test-cases/coq/failed-config.t/run.t Outdated Show resolved Hide resolved
test/blackbox-tests/test-cases/coq/failed-config.t/run.t Show resolved Hide resolved
@ejgallego ejgallego self-assigned this Jun 27, 2024
@gares
Copy link
Contributor Author

gares commented Jun 27, 2024

Thanks for the review, I think I did implement the requested changes

Alizter
Alizter approved these changes Jun 27, 2024
View reviewed changes
Copy link
Collaborator

@Alizter Alizter left a comment

Choose a reason for hiding this comment

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

@ejgallego I am happy with these changes. Would you like to take another look now.

@ejgallego
Copy link
Collaborator

@ejgallego I am happy with these changes. Would you like to take another look now.

Thanks @Alizter , I will process this likely early next week, thanks for the help.

I think tho the PR needs a minor tweak to about the redundant Coq_config.Config, other than that, seems good to me.

@gares
Copy link
Contributor Author

gares commented Jun 28, 2024

done

ejgallego
ejgallego approved these changes Jun 28, 2024
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!

@ejgallego
Copy link
Collaborator

@gares format CI job failed (you can also rebase on the way as github is complaining about it)

gares added 5 commits June 28, 2024 14:31
@gares
[coq] refactor coq_config
22e8f2a 
Signed-off-by: Enrico Tassi <Enrico.Tassi@Inria.fr>
@gares
--print-version needs no init
0df9a12 
Signed-off-by: Enrico Tassi <Enrico.Tassi@Inria.fr>
@gares
[coq] promote tests
d8f12e5 
Signed-off-by: Enrico Tassi <Enrico.Tassi@Inria.fr>
@gares
changelog
2b6f519 
Signed-off-by: Enrico Tassi <Enrico.Tassi@Inria.fr>
@gares
[coq] remove Config module
7a37df2 
Signed-off-by: Enrico Tassi <Enrico.Tassi@Inria.fr>
@gares
Copy link
Contributor Author

gares commented Jun 28, 2024

hoefully done

@ejgallego ejgallego enabled auto-merge (squash) June 30, 2024 08:21
@ejgallego ejgallego merged commit 24dab51 into ocaml:main Jun 30, 2024
1 check passed
@gares gares deleted the fix-coq-config branch July 11, 2024 11:33
@ejgallego ejgallego mentioned this pull request Oct 15, 2024
Closed
anmonteiro pushed a commit to anmonteiro/dune that referenced this pull request Nov 17, 2024
@gares @anmonteiro
[coq] make expand "coq.version" and co not depend on coq-stdlib (ocam…
4ad2f96 
…l#10631)

* [coq] fix `%{coq.version} expansion to work without coq-stdlib

Signed-off-by: Enrico Tassi <Enrico.Tassi@Inria.fr>
maiste added a commit to maiste/opam-repository that referenced this pull request Nov 25, 2024
@maiste
[new release] dune (15 packages) (3.17.0~alpha0)
f1d49be 
CHANGES:

### Fixed

- Show the context name for errors happening in non-default contexts.
  (ocaml/dune#10414, fixes ocaml/dune#10378, @jchavarri)

- Correctly declare dependencies of indexes so that they are rebuilt when
  needed. (ocaml/dune#10623, @voodoos)

- Don't depend on coq-stdlib being installed when expanding variables
  of the `coq.version` family (ocaml/dune#10631, fixes ocaml/dune#10629, @gares)

- Error out if no files are found when using `copy_files`. (ocaml/dune#10649, @jchavarri)

- Re_export dune-section private library in the dune-site library stanza,
  in order to avoid failure when generating and building sites modules
  with implicit_transitive_deps = false. (ocaml/dune#10650, fixes ocaml/dune#9661, @MA0100)

- Expect test fixes: support multiple modes and fix dependencies when there is
  a custom runner (ocaml/dune#10671, @vouillon)

- In a `(library)` stanza with `(extra_objects)` and `(foreign_stubs)`, avoid
  double linking the extra object files in the final executable.
  (ocaml/dune#10783, fixes ocaml/dune#10785, @nojb)

- Map `(re_export)` library dependencies to the `exports` field in `META` files,
  and vice-versa. This field was proposed in to
  https://discuss.ocaml.org/t/proposal-a-new-exports-field-in-findlib-meta-files/13947.
  The field is included in Dune-generated `META` files only when the Dune lang
  version is >= 3.17.
  (ocaml/dune#10831, fixes ocaml/dune#10830, @nojb)

- Fix staged pps preprocessors on Windows (which were not working at all
  previously) (ocaml/dune#10869, fixes ocaml/dune#10867, @nojb)

- Fix `dune describe` when an executable is disabled with `enabled_if`.
  (ocaml/dune#10881, fixes ocaml/dune#10779, @moyodiallo)

- Fix an issue where C stubs would be rebuilt whenever the stderr of Dune was
  redirected. (ocaml/dune#10883, fixes ocaml/dune#10882, @nojb)

- Format long lists in s-expressions to fill the line instead of formatting
  them in a vertical way (ocaml/dune#10892, fixes ocaml/dune#10860, @nojb)

- Fix the URL opened by the command `dune ocaml doc`. (ocaml/dune#10897, @gridbugs)

- Fix the file referred to in the error/warning message displayed due to the
  dune configuration version not supporting a particular configuration
  stanza in use. (ocaml/dune#10923, @H-ANSEN)

- Fix `enabled_if` when it uses `env` variable. (ocaml/dune#10936, fixes ocaml/dune#10905, @moyodiallo)

- Fix exec -w for relative paths with --root argument (ocaml/dune#10982, @gridbugs)

- Do not ignore the `(locks ..)` field in the `test` and `tests` stanza
  (ocaml/dune#11081, @rgrinberg)

- Tolerate files without extension when generating merlin rules.
  (ocaml/dune#11128, @anmonteiro)

### Added

- Make Merlin/OCaml-LSP aware of "hidden" dependencies used by
  `(implicit_transitive_deps false)` via the `-H` compiler flag. (ocaml/dune#10535, @voodoos)

- Add support for the -H flag (introduced in OCaml compiler 5.2) in dune
  (requires lang versions 3.17). This adaptation gives
  the correct semantics for `(implicit_transitive_deps false)`.
  (ocaml/dune#10644, fixes ocaml/dune#9333, ocsigen/tyxml#274, ocaml/dune#2733, ocaml/dune#4963, @MA0100)

- Add support for specifying Gitlab organization repositories in `source`
  stanzas (ocaml/dune#10766, fixes ocaml/dune#6723, @H-ANSEN)

- New option to control jsoo sourcemap generation in env and executable stanza
  (ocaml/dune#10777, fixes ocaml/dune#10673, @hhugo)

- One can now control jsoo compilation_mode inside an executable stanza
  (ocaml/dune#10777, fixes ocaml/dune#10673, @hhugo)

- Add support for specifying default values of the `authors`, `maintainers`, and
  `license` stanzas of the `dune-project` file via the dune config file. Default
  values are set using the `(project_defaults)` stanza (ocaml/dune#10835, @H-ANSEN)

- Add names to source tree events in performance traces (ocaml/dune#10884, @jchavarri)

- Add `codeberg` as an option for defining project sources in dune-project
  files. For example, `(source (codeberg user/repo))`. (ocaml/dune#10904, @nlordell)

- `dune runtest` can now run individual tests with `dune runtest mytest.t`
  (ocaml/dune#11041, @Alizter).

- Wasm_of_ocaml support (ocaml/dune#11093, @vouillon)

- Add a `coqdep_flags` field to the `coq` field of the `env` stanza, and to the `coq.theory` stanza, allowing to configure `coqdep` flags.
  (ocaml/dune#11094, @rlepigre)

### Changed

- Remove all remnants of the experimental `patch-back-source-tree`. (ocaml/dune#10771,
  @rgrinberg)

- Change the preset value for author and maintainer fields in the
  `dune-project` file to encourage including emails. (ocaml/dune#10848, @punchagan)

- Tweak the preset value for tags in the `dune-project` file to hint at topics
  not having a special meaning. (ocaml/dune#10849, @punchagan)

- Change some colors to improve readability in light-mode terminals
  (ocaml/dune#10890, @gridbugs)

- Forward the linkall flag to jsoo in whole program compilation as well (ocaml/dune#10935, @hhugo)

- Configurator uses `pkgconf` as pkg-config implementation when available
  and forwards it the `target` of `ocamlc -config`. (ocaml/dune#10937, @pirbo)

- Enable Dune cache by default. Add a new Dune cache setting
  `enabled-except-user-rules`, which enables the Dune cache, but excludes
  user-written rules from it. This is a conservative choice that can avoid
  breaking rules whose dependencies are not correctly specified. This is the
  current default. (ocaml/dune#10944, ocaml/dune#10710, @nojb, @ElectreAAS)

- Do not add `dune` dependency in `dune-project` when creating projects with
  `dune init proj`. The Dune dependency is implicitely added when generating
  opam files (ocaml/dune#11129, @Leonidas-from-XIV)
@maiste maiste mentioned this pull request Nov 25, 2024
Closed
maiste added a commit to maiste/opam-repository that referenced this pull request Nov 27, 2024
@maiste
[new release] dune (15 packages) (3.17.0)
ca0426d 
CHANGES:

### Fixed

- Show the context name for errors happening in non-default contexts.
  (ocaml/dune#10414, fixes ocaml/dune#10378, @jchavarri)

- Correctly declare dependencies of indexes so that they are rebuilt when
  needed. (ocaml/dune#10623, @voodoos)

- Don't depend on coq-stdlib being installed when expanding variables
  of the `coq.version` family (ocaml/dune#10631, fixes ocaml/dune#10629, @gares)

- Error out if no files are found when using `copy_files`. (ocaml/dune#10649, @jchavarri)

- Re_export dune-section private library in the dune-site library stanza,
  in order to avoid failure when generating and building sites modules
  with implicit_transitive_deps = false. (ocaml/dune#10650, fixes ocaml/dune#9661, @MA0100)

- Expect test fixes: support multiple modes and fix dependencies when there is
  a custom runner (ocaml/dune#10671, @vouillon)

- In a `(library)` stanza with `(extra_objects)` and `(foreign_stubs)`, avoid
  double linking the extra object files in the final executable.
  (ocaml/dune#10783, fixes ocaml/dune#10785, @nojb)

- Map `(re_export)` library dependencies to the `exports` field in `META` files,
  and vice-versa. This field was proposed in to
  https://discuss.ocaml.org/t/proposal-a-new-exports-field-in-findlib-meta-files/13947.
  The field is included in Dune-generated `META` files only when the Dune lang
  version is >= 3.17.
  (ocaml/dune#10831, fixes ocaml/dune#10830, @nojb)

- Fix staged pps preprocessors on Windows (which were not working at all
  previously) (ocaml/dune#10869, fixes ocaml/dune#10867, @nojb)

- Fix `dune describe` when an executable is disabled with `enabled_if`.
  (ocaml/dune#10881, fixes ocaml/dune#10779, @moyodiallo)

- Fix an issue where C stubs would be rebuilt whenever the stderr of Dune was
  redirected. (ocaml/dune#10883, fixes ocaml/dune#10882, @nojb)

- Fix the URL opened by the command `dune ocaml doc`. (ocaml/dune#10897, @gridbugs)

- Fix the file referred to in the error/warning message displayed due to the
  dune configuration version not supporting a particular configuration
  stanza in use. (ocaml/dune#10923, @H-ANSEN)

- Fix `enabled_if` when it uses `env` variable. (ocaml/dune#10936, fixes ocaml/dune#10905, @moyodiallo)

- Fix exec -w for relative paths with --root argument (ocaml/dune#10982, @gridbugs)

- Do not ignore the `(locks ..)` field in the `test` and `tests` stanza
  (ocaml/dune#11081, @rgrinberg)

- Tolerate files without extension when generating merlin rules.
  (ocaml/dune#11128, @anmonteiro)

### Added

- Make Merlin/OCaml-LSP aware of "hidden" dependencies used by
  `(implicit_transitive_deps false)` via the `-H` compiler flag. (ocaml/dune#10535, @voodoos)

- Add support for the -H flag (introduced in OCaml compiler 5.2) in dune
  (requires lang versions 3.17). This adaptation gives
  the correct semantics for `(implicit_transitive_deps false)`.
  (ocaml/dune#10644, fixes ocaml/dune#9333, ocsigen/tyxml#274, ocaml/dune#2733, ocaml/dune#4963, @MA0100)

- Add support for specifying Gitlab organization repositories in `source`
  stanzas (ocaml/dune#10766, fixes ocaml/dune#6723, @H-ANSEN)

- New option to control jsoo sourcemap generation in env and executable stanza
  (ocaml/dune#10777, fixes ocaml/dune#10673, @hhugo)

- One can now control jsoo compilation_mode inside an executable stanza
  (ocaml/dune#10777, fixes ocaml/dune#10673, @hhugo)

- Add support for specifying default values of the `authors`, `maintainers`, and
  `license` stanzas of the `dune-project` file via the dune config file. Default
  values are set using the `(project_defaults)` stanza (ocaml/dune#10835, @H-ANSEN)

- Add names to source tree events in performance traces (ocaml/dune#10884, @jchavarri)

- Add `codeberg` as an option for defining project sources in dune-project
  files. For example, `(source (codeberg user/repo))`. (ocaml/dune#10904, @nlordell)

- `dune runtest` can now run individual tests with `dune runtest mytest.t`
  (ocaml/dune#11041, @Alizter).

- Wasm_of_ocaml support (ocaml/dune#11093, @vouillon)

- Add a `coqdep_flags` field to the `coq` field of the `env` stanza, and to the `coq.theory` stanza, allowing to configure `coqdep` flags.
  (ocaml/dune#11094, @rlepigre)

### Changed

- Remove all remnants of the experimental `patch-back-source-tree`. (ocaml/dune#10771,
  @rgrinberg)

- Change the preset value for author and maintainer fields in the
  `dune-project` file to encourage including emails. (ocaml/dune#10848, @punchagan)

- Tweak the preset value for tags in the `dune-project` file to hint at topics
  not having a special meaning. (ocaml/dune#10849, @punchagan)

- Change some colors to improve readability in light-mode terminals
  (ocaml/dune#10890, @gridbugs)

- Forward the linkall flag to jsoo in whole program compilation as well (ocaml/dune#10935, @hhugo)

- Configurator uses `pkgconf` as pkg-config implementation when available
  and forwards it the `target` of `ocamlc -config`. (ocaml/dune#10937, @pirbo)

- Enable Dune cache by default. Add a new Dune cache setting
  `enabled-except-user-rules`, which enables the Dune cache, but excludes
  user-written rules from it. This is a conservative choice that can avoid
  breaking rules whose dependencies are not correctly specified. This is the
  current default. (ocaml/dune#10944, ocaml/dune#10710, @nojb, @ElectreAAS)

- Do not add `dune` dependency in `dune-project` when creating projects with
  `dune init proj`. The Dune dependency is implicitely added when generating
  opam files (ocaml/dune#11129, @Leonidas-from-XIV)
@maiste maiste mentioned this pull request Nov 27, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Alizter Alizter Alizter approved these changes

@ejgallego ejgallego ejgallego approved these changes

Assignees

@ejgallego ejgallego

Labels
coq
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

[coq] expand coq.version & co without using coq-lib
3 participants
@gares @Alizter @ejgallego