Raise a user error when dune install is run with package management enabled. - #14427
Merged
Conversation
shonfeder
reviewed
May 5, 2026
Leonidas-from-XIV
requested changes
May 6, 2026
Sudha247
force-pushed
the
dune-pkg-disable-dune-install
branch
from
May 6, 2026 13:39
373b03b to
f662cc8
Compare
Leonidas-from-XIV
requested changes
May 6, 2026
Leonidas-from-XIV
left a comment
Leonidas-from-XIV
left a comment
Member
There was a problem hiding this comment.
Only two changes to update the test, otherwise LGTM.
Sudha247
requested review from
Leonidas-from-XIV
and removed request for
Leonidas-from-XIV
May 7, 2026 12:29
Sudha247
force-pushed
the
dune-pkg-disable-dune-install
branch
from
May 7, 2026 12:34
f662cc8 to
ca5b6cb
Compare
Leonidas-from-XIV
approved these changes
May 7, 2026
Alizter
reviewed
May 7, 2026
Alizter
reviewed
May 7, 2026
Alizter
approved these changes
May 7, 2026
This is due to the fact that the `dune install` command is incompatible Dune pkg and is susceptible to crashes. Signed-off-by: Sudha Parimala <sudharg247@gmail.com>
Signed-off-by: Sudha Parimala <sudharg247@gmail.com>
Re-use the function in pkg_enabled, and move it to pkg_common to avoid repitition. There is already a similar function `check_pkg_management_enabled` in pkg_common, but we're not using it here because its purpose is to just see if dune-workspace has (pkg enabled), and it doesn't cover all the cases we want to check, to know whether package management is enabled. Signed-off-by: Sudha Parimala <sudharg247@gmail.com>
move the docstrings to the correct place, and add doc for pkg_enabled Signed-off-by: Sudha Parimala <sudharg247@gmail.com>
Signed-off-by: Sudha Parimala <sudharg247@gmail.com>
Sudha247
force-pushed
the
dune-pkg-disable-dune-install
branch
from
May 7, 2026 15:20
ca5b6cb to
6ce66d4
Compare
Alizter
approved these changes
May 7, 2026
Collaborator
|
Thanks, I'll merge later when the CI is green. Just needs a |
elaborate on the new pkg_enabled function, and remove opam hint from the user error Signed-off-by: Sudha Parimala <sudharg247@gmail.com>
Sudha247
force-pushed
the
dune-pkg-disable-dune-install
branch
from
May 7, 2026 16:07
6ce66d4 to
836149c
Compare
Member
Author
|
Thanks! Fixed the formatting issue. |
Alizter
added
the
package management
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
4 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.
Follow-up to #14289. Discussion on the previous PR concluded that this combination isn't supported, so this PR makes
dune installraise a clean user error instead of crashing when package management is enabled.Addresses the internal error from #14272