Merged
Conversation
60eca42 to
d3134d9
Compare
rgrinberg
commented
Jan 26, 2024
| Scope.coq_libs scope | ||
| |> Resolve.Memo.lift_memo | ||
| >>= Coq_lib.DB.resolve_boot ~coq_lang_version | ||
| |> Resolve.Memo.read_memo |
Member
Author
There was a problem hiding this comment.
This is a no-no because it prevents the rules in the entire directory from loading if the library isn't found.
rgrinberg
commented
Jan 26, 2024
| "Couldn't find Coq standard library, and theory is not using (stdlib no)" | ||
| ] | ||
| else Implicit | ||
| Resolve.Memo.fail |
Member
Author
There was a problem hiding this comment.
Instead of raising, we save the error.
rgrinberg
commented
Jan 26, 2024
| in | ||
| [ Bootstrap.flags boot_type; S file_flags ] | ||
| let boot_flags = Resolve.Memo.read boot_type |> Action_builder.map ~f:Bootstrap.flags in | ||
| [ Dyn boot_flags; S file_flags ] |
Member
Author
There was a problem hiding this comment.
And here we resurface the error, but this time only when we try to execute the relevant rule that needs this.
Collaborator
|
FTR, this does fix #9818. |
ejgallego
approved these changes
Jan 29, 2024
Collaborator
ejgallego
left a comment
There was a problem hiding this comment.
Thanks a lot @rgrinberg !
It would be good if we try to push the test case, however I'm unsure how can we make a test such that we ensure coqc is not available, maybe we could mock coqc to fail, but that's not exactly the same.
d3134d9 to
adb6e1c
Compare
Collaborator
|
@ejgallego you can make a |
Collaborator
|
Thanks @emillon ! Will add this test, as this seems like an easy to get wrong case. @rgrinberg , PR looks ready for merging to me, however a tweak on Coq's test-suite is needed due to the output being more verbose now on error. |
Member
Author
|
Sure, feel free to update the output if it looks good to you. I don't have coq installed at the moment. |
ea83270 to
783efb3
Compare
Fixes #9818 Signed-off-by: Rudi Grinberg <me@rgrinberg.com> <!-- ps-id: d2fe6b57-4512-4907-8577-43fdabcdcf8b -->
783efb3 to
f70fa83
Compare
rlepigre
pushed a commit
to rlepigre/dune
that referenced
this pull request
Feb 29, 2024
…ype_detection fix(coq): delay boot type detection
rlepigre
pushed a commit
to rlepigre/dune
that referenced
this pull request
Feb 29, 2024
…ype_detection fix(coq): delay boot type detection
rlepigre
pushed a commit
to rlepigre/dune
that referenced
this pull request
Feb 29, 2024
…ype_detection fix(coq): delay boot type detection
Leonidas-from-XIV
added a commit
to Leonidas-from-XIV/opam-repository
that referenced
this pull request
Mar 26, 2024
CHANGES: ### Added - Add link flags to to `ocamlmklib` for ctypes stubs (ocaml/dune#8784, @frejsoya) - Remove some unnecessary limitations in the expansions of percent forms in install stanza. For example, the `%{env:..}` form can be used to select files to be installed. (ocaml/dune#10160, @rgrinberg) - Allow artifact expansion percent forms (`%{cma:..}`, `%{cmo:..}`, etc.) in more contexts. Previously, they would be randomly forbidden in some fields. (ocaml/dune#10169, @rgrinberg) - Allow `%{inline_tests}` in more contexts (ocaml/dune#10191, @rgrinberg) - Remove limitations on percent forms in the `(enabled_if ..)` field of libraries (ocaml/dune#10250, @rgrinberg) - Support dialects in `dune describe pp` (ocaml/dune#10283, @emillon) - Allow defining executables or melange emit stanzas with the same name in the same folder under different contexts. (ocaml/dune#10220, @rgrinberg, @jchavarri) ### Fixed - coq: Delay Coq rule setup checks so OCaml-only packages can build in hybrid Coq/OCaml projects when `coqc` is not present. Thanks to @vzaliva for the test case and report (ocaml/dune#9845, fixes ocaml/dune#9818, @rgrinberg, @ejgallego) - Fix conditional source selection with `select` on `bigarray` in OCaml 5 (ocaml/dune#10011, @moyodiallo) - melange: fix inconsistency in virtual library implementation. Concrete modules within a virtual library can now refer to its virtual modules too (ocaml/dune#10051, fixes ocaml/dune#7104, @anmonteiro) - melange: fix a bug that would cause stale `import` paths to be emitted when moving source files within `(include_subdirs ..)` (ocaml/dune#10286, fixes ocaml/dune#9190, @anmonteiro) - Dune file formatting: output utf8 if input is correctly encoded (ocaml/dune#10113, fixes ocaml/dune#9728, @moyodiallo) - Fix expanding dependencies and locks specified in the cram stanza. Previously, they would be installed in the context of the cram test, rather than the cram stanza itself (ocaml/dune#10165, @rgrinberg) - Fix bug with `dune exec --watch` where the working directory would always be set to the project root rather than the directory where the command was run (ocaml/dune#10262, @gridbugs) - Regression fix: sign executables that are promoted into the source tree (ocaml/dune#10263, fixes ocaml/dune#9272, @emillon) - Fix crash when decoding dune-package for libraries with `(include_subdirs qualified)` (ocaml/dune#10269, fixes ocaml/dune#10264, @emillon) ### Changed - Remove the `--react-to-insignificant-changes` option. (ocaml/dune#10083, @rgrinberg)
Leonidas-from-XIV
added a commit
to Leonidas-from-XIV/opam-repository
that referenced
this pull request
Apr 3, 2024
CHANGES: ### Added - Add link flags to to `ocamlmklib` for ctypes stubs (ocaml/dune#8784, @frejsoya) - Remove some unnecessary limitations in the expansions of percent forms in install stanza. For example, the `%{env:..}` form can be used to select files to be installed. (ocaml/dune#10160, @rgrinberg) - Allow artifact expansion percent forms (`%{cma:..}`, `%{cmo:..}`, etc.) in more contexts. Previously, they would be randomly forbidden in some fields. (ocaml/dune#10169, @rgrinberg) - Allow `%{inline_tests}` in more contexts (ocaml/dune#10191, @rgrinberg) - Remove limitations on percent forms in the `(enabled_if ..)` field of libraries (ocaml/dune#10250, @rgrinberg) - Support dialects in `dune describe pp` (ocaml/dune#10283, @emillon) - Allow defining executables or melange emit stanzas with the same name in the same folder under different contexts. (ocaml/dune#10220, @rgrinberg, @jchavarri) ### Fixed - coq: Delay Coq rule setup checks so OCaml-only packages can build in hybrid Coq/OCaml projects when `coqc` is not present. Thanks to @vzaliva for the test case and report (ocaml/dune#9845, fixes ocaml/dune#9818, @rgrinberg, @ejgallego) - Fix conditional source selection with `select` on `bigarray` in OCaml 5 (ocaml/dune#10011, @moyodiallo) - melange: fix inconsistency in virtual library implementation. Concrete modules within a virtual library can now refer to its virtual modules too (ocaml/dune#10051, fixes ocaml/dune#7104, @anmonteiro) - melange: fix a bug that would cause stale `import` paths to be emitted when moving source files within `(include_subdirs ..)` (ocaml/dune#10286, fixes ocaml/dune#9190, @anmonteiro) - Dune file formatting: output utf8 if input is correctly encoded (ocaml/dune#10113, fixes ocaml/dune#9728, @moyodiallo) - Fix expanding dependencies and locks specified in the cram stanza. Previously, they would be installed in the context of the cram test, rather than the cram stanza itself (ocaml/dune#10165, @rgrinberg) - Fix bug with `dune exec --watch` where the working directory would always be set to the project root rather than the directory where the command was run (ocaml/dune#10262, @gridbugs) - Regression fix: sign executables that are promoted into the source tree (ocaml/dune#10263, fixes ocaml/dune#9272, @emillon) - Fix crash when decoding dune-package for libraries with `(include_subdirs qualified)` (ocaml/dune#10269, fixes ocaml/dune#10264, @emillon) ### Changed - Remove the `--react-to-insignificant-changes` option. (ocaml/dune#10083, @rgrinberg)
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
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.
Signed-off-by: Rudi Grinberg me@rgrinberg.com
Fixes #9818