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.

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

fix: resolve installed binaries to local paths #9496

Merged

Conversation

rgrinberg
Copy link
Member

@rgrinberg rgrinberg commented Dec 13, 2023

Previously, we'd always binaries from the install context
(_build/install/$context/bin). This would unnecessarily load the install
rules.

Now, we add an argument that allows us to resolve to the original paths.
Reducing the amount of rules that need to be loaded.

We use this argument in a few cases where we don't need to build the
path in _build/install

Ideally, we'd use this everywhere as it's basically strictly superior. The only issue is that it doesn't preserve backward compat in cases like:

(rule
 (dep %{bin:foo})
 (action (run which foo)))

Resolving it in _build/install/default will make the which above succeed because we add the bin path in the install directory to the PATH when executing actions. There's a way to get around that of course, but it's not trivial.

@rgrinberg rgrinberg force-pushed the ps/rr/refactor__resolve_installed_binaries_to_local_paths branch from f6dcec0 to b2f8a20 Compare December 13, 2023 18:44
@rgrinberg rgrinberg force-pushed the ps/rr/refactor__resolve_installed_binaries_to_local_paths branch 2 times, most recently from e8a5a71 to 6d4ab70 Compare December 22, 2023 16:47
@rgrinberg rgrinberg added the coq label Dec 22, 2023
~dir
~where:Original_path
~hint:"opam install melange"
"melc"
Copy link
Member Author

Choose a reason for hiding this comment

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

@anmonteiro I tweaked the resolution of melange here as well. It shouldn't affect anything, but could in theory help with some odd cycles

@rgrinberg rgrinberg force-pushed the ps/rr/refactor__resolve_installed_binaries_to_local_paths branch 3 times, most recently from 94964b6 to c500f06 Compare December 22, 2023 18:31
@rgrinberg
Copy link
Member Author

I just realized that we also resolve (enabled_if ..) a little too early for public binaries. I'll fix that in a subsequent PR.

@rgrinberg rgrinberg force-pushed the ps/rr/refactor__resolve_installed_binaries_to_local_paths branch from c500f06 to 604883b Compare December 22, 2023 19:03
@rgrinberg
Copy link
Member Author

ping @ejgallego

@rgrinberg rgrinberg force-pushed the ps/rr/refactor__resolve_installed_binaries_to_local_paths branch from 604883b to d8a9e8b Compare January 2, 2024 20:23
@ejgallego
Copy link
Collaborator

ping @ejgallego

Thanks, I'm still on holidays but I'll try to test this ASAP.

@rgrinberg rgrinberg force-pushed the ps/rr/refactor__resolve_installed_binaries_to_local_paths branch from d8a9e8b to 8f000f4 Compare January 10, 2024 19:20
@rgrinberg
Copy link
Member Author

Sure no problem. Although the window for getting this in for 3.13 is closing.

@ejgallego
Copy link
Collaborator

ejgallego commented Jan 10, 2024

Sure no problem. Although the window for getting this in for 3.13 is closing.

I just came back to Paris today, I'll keep that in mind thanks!

I have a first question tho, is this really a refactoring? Seems to me like an observable behavior change?

@rgrinberg
Copy link
Member Author

I did a CHANGES entry to the observable bit. I'll change the title since it's indeed not a refactoring.

@rgrinberg rgrinberg changed the title refactor: resolve installed binaries to local paths fix: resolve installed binaries to local paths Jan 10, 2024
@ejgallego
Copy link
Collaborator

ejgallego commented Jan 11, 2024

@rgrinberg I can confirm that this PR fixes the base and extended cases I have for #7908 .

H̶o̶w̶e̶v̶e̶r̶ ̶w̶e̶ ̶s̶t̶i̶l̶l̶ ̶h̶a̶v̶e̶ ̶a̶ ̶p̶r̶o̶b̶l̶e̶m̶ ̶i̶n̶ ̶t̶h̶e̶ ̶c̶a̶s̶e̶ ̶a̶ ̶C̶o̶q̶ ̶t̶h̶e̶o̶r̶y̶ ̶u̶s̶i̶n̶g̶ ̶p̶l̶u̶g̶i̶n̶s̶ ̶i̶s̶ ̶i̶n̶ ̶t̶h̶e̶ ̶w̶o̶r̶k̶s̶p̶a̶c̶e̶.̶ ̶I̶n̶ ̶t̶h̶i̶s̶ ̶c̶a̶s̶e̶,̶ ̶D̶u̶n̶e̶ ̶h̶a̶n̶g̶s̶ ̶h̶a̶r̶d̶.̶

Outdated info

I guess this is due to Coq_rules.ml_pack_and_meta_rule , however I don't see how the install rules are forced.

What the code does is as follows, assume a setup such as:

(library
 (name bar)
 (public_name foo.bar)
 (libraries coq-core.vernac))

(coq.theory
 (name bar)
 (package foo)
 (modules moo)
 (plugins foo.bar))

Then, the rule to generate bar.v.d using coqdep needs to be as follows:

(rule
  (targets moo.v.d)
  (deps %{install}/lib/foo/META moo.v)
  (action (run coqdep -Q bar . moo.v)))

As coqdep needs META for foo in place to resolve the .cmxs file that will appear as a dependency on the .vo rule.

But indeed I'm puzzled as why this makes Dune hang, I don't see any forcing in computing the META path.

@rgrinberg
Copy link
Member Author

Those META issues need to be addressed separately from this PR.

But indeed I'm puzzled as why this makes Dune hang, I don't see any forcing in computing the META path.

Probably there's a cycle that makes it hang. AFAIK @snowleopard is working on upstreaming some improvements to the cycle detection

@ejgallego

This comment was marked as outdated.

@ejgallego
Copy link
Collaborator

Actually never mind, I messed up my testing and I was not using the right dune binary!

Things seem to work fine even with my extended test cases, as they should be.

@@ -0,0 +1,2 @@
- Resolve various public binaries to their build location, rather than to where
they're copied in the `_build/install` directory (@9496, @rgrinberg).
Copy link
Collaborator

Choose a reason for hiding this comment

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

Fixes #7908

@ejgallego
Copy link
Collaborator

Another comment @rgrinberg : should this change be guarded by dune lang version?

@rgrinberg
Copy link
Member Author

Don't think so. I've only changed the behavior of internals rules that never guaranteed where the binary they resolve to would come from.

@ejgallego
Copy link
Collaborator

LGTM

Previously, we'd always binaries from the install context
(_build/install/$context/bin). This would unnecessarily load the install
rules.

Now, we add an argument that allows us to resolve to the original paths.
Reducing the amount of rules that need to be loaded.

We use this argument in a few cases where we don't need to build the
path in _build/install

<!-- ps-id: cb6fc8f6-5f50-439b-b542-6b933c656af0 -->

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>
@rgrinberg rgrinberg force-pushed the ps/rr/refactor__resolve_installed_binaries_to_local_paths branch from 8f000f4 to 71804bb Compare January 11, 2024 17:36
@rgrinberg rgrinberg added this to the 3.13.0 milestone Jan 11, 2024
@rgrinberg rgrinberg merged commit b4242f8 into main Jan 11, 2024
24 of 27 checks passed
@rgrinberg rgrinberg deleted the ps/rr/refactor__resolve_installed_binaries_to_local_paths branch January 11, 2024 17:36
emillon added a commit to emillon/opam-repository that referenced this pull request Jan 12, 2024
CHANGES:

- Do not ignore `(formatting ..)` settings in context or workspace files
  (ocaml/dune#8447, @rgrinberg)

- Add command `dune cache clear` to completely delete all traces of the Dune
  cache. (ocaml/dune#8975, @nojb)

- Fixed a bug where Dune was incorrectly parsing the output of coqdep when it
  was escaped, as is the case on Windows. (ocaml/dune#9231, fixes ocaml/dune#9218, @Alizter)

- Copying mode for sandboxes will now follow symbolic links (ocaml/dune#9282, @rgrinberg)

- Forbid the empty `(binaries ..)` field in the `env` stanza in the workspace
  file unless language version is at least 3.2.

- [coq] Fix bug in computation of flags when composed with boot theories.
  (ocaml/dune#9347, fixes ocaml/dune#7909, @ejgallego)

- Fixed a bug where the `(select)` field of the `(libraries)` field of the
  `(test)` stanza wasn't working properly. (ocaml/dune#9387, fixes ocaml/dune#9365, @Alizter)

- Allow to disable Coq 0.8 deprecation warning (ocaml/dune#9439, @ejgallego)

- Fix handling of the `PATH` argument to `dune init proj NAME PATH`. An
  intermediate directory called `NAME` is no longer created if `PATH` is
  supplied, so `dune init proj my_project .` will now initialize a project in
  the current working directory. (ocaml/dune#9447, fixes ocaml/dune#9209, @shonfeder)

- Allow `OCAMLFIND_TOOLCHAIN` to be set per context in the workspace file
  through the `env` stanza. (ocaml/dune#9449, @rgrinberg)

- Experimental doc rules: Correctly handle the case when a package depends upon
  its own sublibraries (ocaml/dune#9461, fixes ocaml/dune#9456, @jonludlam)

- Resolve various public binaries to their build location, rather than to where
  they're copied in the `_build/install` directory (ocaml/dune#9496, fixes ocaml/dune#7908,
  @rgrinberg).

- Menhir: generate `.conflicts` file by default. Add new field to the
  `(menhir)` stanza to control the generation of this file: `(explain <blang
  expression>)`. Introduce `(menhir (flags ...) (explain ...))` field in the
  `(env)` stanza, delete `(menhir_flags)` field. All changes are guarded under
  a new version of the Menhir extension, 3.0. (ocaml/dune#9512, @nojb)

- Correctly ignore warning flags in vendored projects (ocaml/dune#9515, @rgrinberg)

- Directory targets can now be caches. (ocaml/dune#9535, @rleshchinskiy)

- Remove warning 30 from default set for projects where dune lang is at least
  3.13 (ocaml/dune#9568, @gasche)

- It is now possible to use special forms such as `(:include)` and variables
  `%{read-lines:}` in `(modules)` and similar fields. Note that the
  dependencies introduced in this way (ie the files being read) must live in a
  different directory than the stanza making use of them. (ocaml/dune#9578, @nojb)

- Use watch exclusions in watch mode on MacOS (ocaml/dune#9643, fixes ocaml/dune#9517,
  @PoorlyDefinedBehaviour)

- Fix merlin configuration for `(include_subdirs qualified)` modules (ocaml/dune#9659,
  fixes ocaml/dune#8297, @rgrinberg)

- Fix handling of `enabled_if` in binary install stanzas. Previously, we'd
  ignore the result of `enabled_if` when evaluating `%{bin:..}` (ocaml/dune#9707,
  @rgrinberg)

- Add `coqdoc_flags` field to `coq` field of `env` stanza allowing the setting
  of workspace-wide defaults for `coqdoc_flags`. (ocaml/dune#9280, fixes ocaml/dune#9139, @Alizter)

- ctypes: fix an error where `(ctypes)` with no `(function_description)` would
  cause an error trying refer to a nonexistent `_stubs.a` dependency (ocaml/dune#9302,
  fix ocaml/dune#9300, @emillon)
emillon added a commit to emillon/opam-repository that referenced this pull request Jan 16, 2024
CHANGES:

### Added

- Add command `dune cache clear` to completely delete all traces of the Dune
  cache. (ocaml/dune#8975, @nojb)

- Allow to disable Coq 0.8 deprecation warning (ocaml/dune#9439, @ejgallego)

- Allow `OCAMLFIND_TOOLCHAIN` to be set per context in the workspace file
  through the `env` stanza. (ocaml/dune#9449, @rgrinberg)

- Menhir: generate `.conflicts` file by default. Add new field to the
  `(menhir)` stanza to control the generation of this file: `(explain <blang
  expression>)`. Introduce `(menhir (flags ...) (explain ...))` field in the
  `(env)` stanza, delete `(menhir_flags)` field. All changes are guarded under
  a new version of the Menhir extension, 3.0. (ocaml/dune#9512, @nojb)

- Directory targets can now be cached. (ocaml/dune#9535, @rleshchinskiy)

- It is now possible to use special forms such as `(:include)` and variables
  `%{read-lines:}` in `(modules)` and similar fields. Note that the
  dependencies introduced in this way (ie the files being read) must live in a
  different directory than the stanza making use of them. (ocaml/dune#9578, @nojb)

- Remove warning 30 from default set for projects where dune lang is at least
  3.13 (ocaml/dune#9568, @gasche)

- Add `coqdoc_flags` field to `coq` field of `env` stanza allowing the setting
  of workspace-wide defaults for `coqdoc_flags`. (ocaml/dune#9280, fixes ocaml/dune#9139, @Alizter)

- ctypes: fix an error where `(ctypes)` with no `(function_description)` would
  cause an error trying refer to a nonexistent `_stubs.a` dependency (ocaml/dune#9302,
  fix ocaml/dune#9300, @emillon)

### Changed

- Check that package names in `(depends)` and related fields in `dune-project`
  are well-formed. (ocaml/dune#9472, fixes ocaml/dune#9270, @ElectreAAS)

### Fixed

- Do not ignore `(formatting ..)` settings in context or workspace files
  (ocaml/dune#8447, @rgrinberg)

- Fixed a bug where Dune was incorrectly parsing the output of coqdep when it
  was escaped, as is the case on Windows. (ocaml/dune#9231, fixes ocaml/dune#9218, @Alizter)

- Copying mode for sandboxes will now follow symbolic links (ocaml/dune#9282, @rgrinberg)

- Forbid the empty `(binaries ..)` field in the `env` stanza in the workspace
  file unless language version is at least 3.2.

- [coq] Fix bug in computation of flags when composed with boot theories.
  (ocaml/dune#9347, fixes ocaml/dune#7909, @ejgallego)

- Fixed a bug where the `(select)` field of the `(libraries)` field of the
  `(test)` stanza wasn't working properly. (ocaml/dune#9387, fixes ocaml/dune#9365, @Alizter)

- Fix handling of the `PATH` argument to `dune init proj NAME PATH`. An
  intermediate directory called `NAME` is no longer created if `PATH` is
  supplied, so `dune init proj my_project .` will now initialize a project in
  the current working directory. (ocaml/dune#9447, fixes ocaml/dune#9209, @shonfeder)

- Experimental doc rules: Correctly handle the case when a package depends upon
  its own sublibraries (ocaml/dune#9461, fixes ocaml/dune#9456, @jonludlam)

- Resolve various public binaries to their build location, rather than to where
  they're copied in the `_build/install` directory (ocaml/dune#9496, fixes ocaml/dune#7908,
  @rgrinberg).

- Correctly ignore warning flags in vendored projects (ocaml/dune#9515, @rgrinberg)

- Use watch exclusions in watch mode on MacOS (ocaml/dune#9643, fixes ocaml/dune#9517,
  @PoorlyDefinedBehaviour)

- Fix merlin configuration for `(include_subdirs qualified)` modules (ocaml/dune#9659,
  fixes ocaml/dune#8297, @rgrinberg)

- Fix handling of `enabled_if` in binary install stanzas. Previously, we'd
  ignore the result of `enabled_if` when evaluating `%{bin:..}` (ocaml/dune#9707,
  @rgrinberg)
nberth pushed a commit to nberth/opam-repository that referenced this pull request Jun 18, 2024
CHANGES:

### Added

- Add command `dune cache clear` to completely delete all traces of the Dune
  cache. (ocaml/dune#8975, @nojb)

- Allow to disable Coq 0.8 deprecation warning (ocaml/dune#9439, @ejgallego)

- Allow `OCAMLFIND_TOOLCHAIN` to be set per context in the workspace file
  through the `env` stanza. (ocaml/dune#9449, @rgrinberg)

- Menhir: generate `.conflicts` file by default. Add new field to the
  `(menhir)` stanza to control the generation of this file: `(explain <blang
  expression>)`. Introduce `(menhir (flags ...) (explain ...))` field in the
  `(env)` stanza, delete `(menhir_flags)` field. All changes are guarded under
  a new version of the Menhir extension, 3.0. (ocaml/dune#9512, @nojb)

- Directory targets can now be cached. (ocaml/dune#9535, @rleshchinskiy)

- It is now possible to use special forms such as `(:include)` and variables
  `%{read-lines:}` in `(modules)` and similar fields. Note that the
  dependencies introduced in this way (ie the files being read) must live in a
  different directory than the stanza making use of them. (ocaml/dune#9578, @nojb)

- Remove warning 30 from default set for projects where dune lang is at least
  3.13 (ocaml/dune#9568, @gasche)

- Add `coqdoc_flags` field to `coq` field of `env` stanza allowing the setting
  of workspace-wide defaults for `coqdoc_flags`. (ocaml/dune#9280, fixes ocaml/dune#9139, @Alizter)

- ctypes: fix an error where `(ctypes)` with no `(function_description)` would
  cause an error trying refer to a nonexistent `_stubs.a` dependency (ocaml/dune#9302,
  fix ocaml/dune#9300, @emillon)

### Changed

- Check that package names in `(depends)` and related fields in `dune-project`
  are well-formed. (ocaml/dune#9472, fixes ocaml/dune#9270, @ElectreAAS)

### Fixed

- Do not ignore `(formatting ..)` settings in context or workspace files
  (ocaml/dune#8447, @rgrinberg)

- Fixed a bug where Dune was incorrectly parsing the output of coqdep when it
  was escaped, as is the case on Windows. (ocaml/dune#9231, fixes ocaml/dune#9218, @Alizter)

- Copying mode for sandboxes will now follow symbolic links (ocaml/dune#9282, @rgrinberg)

- Forbid the empty `(binaries ..)` field in the `env` stanza in the workspace
  file unless language version is at least 3.2.

- [coq] Fix bug in computation of flags when composed with boot theories.
  (ocaml/dune#9347, fixes ocaml/dune#7909, @ejgallego)

- Fixed a bug where the `(select)` field of the `(libraries)` field of the
  `(test)` stanza wasn't working properly. (ocaml/dune#9387, fixes ocaml/dune#9365, @Alizter)

- Fix handling of the `PATH` argument to `dune init proj NAME PATH`. An
  intermediate directory called `NAME` is no longer created if `PATH` is
  supplied, so `dune init proj my_project .` will now initialize a project in
  the current working directory. (ocaml/dune#9447, fixes ocaml/dune#9209, @shonfeder)

- Experimental doc rules: Correctly handle the case when a package depends upon
  its own sublibraries (ocaml/dune#9461, fixes ocaml/dune#9456, @jonludlam)

- Resolve various public binaries to their build location, rather than to where
  they're copied in the `_build/install` directory (ocaml/dune#9496, fixes ocaml/dune#7908,
  @rgrinberg).

- Correctly ignore warning flags in vendored projects (ocaml/dune#9515, @rgrinberg)

- Use watch exclusions in watch mode on MacOS (ocaml/dune#9643, fixes ocaml/dune#9517,
  @PoorlyDefinedBehaviour)

- Fix merlin configuration for `(include_subdirs qualified)` modules (ocaml/dune#9659,
  fixes ocaml/dune#8297, @rgrinberg)

- Fix handling of `enabled_if` in binary install stanzas. Previously, we'd
  ignore the result of `enabled_if` when evaluating `%{bin:..}` (ocaml/dune#9707,
  @rgrinberg)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

[coq] Composition with (boot) theories hangs with a cycle in Dune > 3.7 when coq lang > 0.6
2 participants