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

fix(coq): delay boot type detection #9845

Merged
merged 1 commit into from
Feb 9, 2024
Merged

fix(coq): delay boot type detection #9845

merged 1 commit into from
Feb 9, 2024

Conversation

rgrinberg
Copy link
Member

@rgrinberg rgrinberg commented Jan 26, 2024 •
edited by ejgallego
Loading

Signed-off-by: Rudi Grinberg me@rgrinberg.com

Fixes #9818

@rgrinberg rgrinberg force-pushed the ps/rr/fix_coq___delay_boot_type_detection branch from 60eca42 to d3134d9 Compare January 26, 2024 23:40
@rgrinberg rgrinberg mentioned this pull request Jan 26, 2024
Closed
rgrinberg
rgrinberg commented Jan 26, 2024
View reviewed changes
src/dune_rules/coq/coq_rules.ml
>>= Coq_lib.DB.resolve_boot ~coq_lang_version
|> Resolve.Memo.read_memo
Copy link
Member Author

@rgrinberg rgrinberg Jan 26, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

This is a no-no because it prevents the rules in the entire directory from loading if the library isn't found.

rgrinberg
rgrinberg commented Jan 26, 2024
View reviewed changes
src/dune_rules/coq/coq_rules.ml
"Couldn't find Coq standard library, and theory is not using (stdlib no)"
]
else Implicit
Resolve.Memo.fail
Copy link
Member Author

Choose a reason for hiding this comment

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

Instead of raising, we save the error.

rgrinberg
rgrinberg commented Jan 26, 2024
View reviewed changes
src/dune_rules/coq/coq_rules.ml
@@ -289,7 +293,8 @@ let coqc_file_flags ~dir ~theories_deps ~wrapper_name ~boot_type ~ml_flags
; A wrapper_name
]
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 ]
Copy link
Member Author

Choose a reason for hiding this comment

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

And here we resurface the error, but this time only when we try to execute the relevant rule that needs this.

@rgrinberg rgrinberg added the coq label Jan 26, 2024
@emillon
Copy link
Collaborator

emillon commented Jan 29, 2024

FTR, this does fix #9818.

ejgallego
ejgallego approved these changes Jan 29, 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 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.

@ejgallego ejgallego force-pushed the ps/rr/fix_coq___delay_boot_type_detection branch from d3134d9 to adb6e1c Compare January 29, 2024 10:48
@emillon
Copy link
Collaborator

emillon commented Jan 29, 2024

@ejgallego you can make a path directory with just dune and ocamlc copied from the PATH, and set PATH to just that directory. See https://github.com/ocaml/dune/blob/3.13.0/test/blackbox-tests/test-cases/melange/missing-melc.t for example.

@ejgallego
Copy link
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.

@rgrinberg
Copy link
Member Author

Sure, feel free to update the output if it looks good to you. I don't have coq installed at the moment.

@ejgallego ejgallego force-pushed the ps/rr/fix_coq___delay_boot_type_detection branch 3 times, most recently from ea83270 to 783efb3 Compare February 9, 2024 17:29
@rgrinberg @ejgallego
fix(coq): delay boot type detection
f70fa83 
Fixes #9818

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

<!-- ps-id: d2fe6b57-4512-4907-8577-43fdabcdcf8b -->
@ejgallego ejgallego force-pushed the ps/rr/fix_coq___delay_boot_type_detection branch from 783efb3 to f70fa83 Compare February 9, 2024 20:53
@ejgallego ejgallego merged commit 189a517 into main Feb 9, 2024
1 of 2 checks passed
@ejgallego ejgallego deleted the ps/rr/fix_coq___delay_boot_type_detection branch February 9, 2024 20:53
rlepigre pushed a commit to rlepigre/dune that referenced this pull request Feb 29, 2024
@ejgallego @rlepigre
Merge pull request ocaml#9845 from ocaml/ps/rr/fix_coq___delay_boot_t…
8643b04 
…ype_detection

fix(coq): delay boot type detection
rlepigre pushed a commit to rlepigre/dune that referenced this pull request Feb 29, 2024
@ejgallego @rlepigre
Merge pull request ocaml#9845 from ocaml/ps/rr/fix_coq___delay_boot_t…
5308f7b 
…ype_detection

fix(coq): delay boot type detection
rlepigre pushed a commit to rlepigre/dune that referenced this pull request Feb 29, 2024
@ejgallego @rlepigre
Merge pull request ocaml#9845 from ocaml/ps/rr/fix_coq___delay_boot_t…
b175a99 
…ype_detection

fix(coq): delay boot type detection
@Leonidas-from-XIV Leonidas-from-XIV mentioned this pull request Mar 26, 2024
Closed
Leonidas-from-XIV added a commit to Leonidas-from-XIV/opam-repository that referenced this pull request Mar 26, 2024
@Leonidas-from-XIV
[new release] dune (15 packages) (3.15.0~alpha1)
68b4763 
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
@Leonidas-from-XIV
[new release] dune (15 packages) (3.15.0)
950c529 
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 Leonidas-from-XIV mentioned this pull request Apr 3, 2024
Merged
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
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

regression on missing Coq
3 participants
@rgrinberg @emillon @ejgallego