Skip to content

Fix #8042, multiple rocq.extraction in directory.#13531

Merged
Alizter merged 2 commits intoocaml:mainfrom
rlepigre-skylabs-ai:fix-8042
Feb 18, 2026
Merged

Fix #8042, multiple rocq.extraction in directory.#13531
Alizter merged 2 commits intoocaml:mainfrom
rlepigre-skylabs-ai:fix-8042

Conversation

@rlepigre-skylabs-ai
Copy link
Collaborator

@rlepigre-skylabs-ai rlepigre-skylabs-ai commented Feb 3, 2026

Fixes #8042.

@Alizter
Copy link
Collaborator

Alizter commented Feb 3, 2026

What about having a way to set the extraction directory?

@rlepigre-skylabs-ai
Copy link
Collaborator Author

rlepigre-skylabs-ai commented Feb 3, 2026

Would it be worth it, given that you can just add a copy rule?

@rlepigre-skylabs-ai
Copy link
Collaborator Author

rlepigre-skylabs-ai commented Feb 16, 2026

@Alizter should we get this in, or is there any blocker?

@Alizter
Copy link
Collaborator

Alizter commented Feb 17, 2026

@rlepigre-skylabs-ai Can you give this a rebase?

@Alizter
Copy link
Collaborator

Alizter commented Feb 17, 2026

Oh and changelog

@rlepigre-skylabs-ai
Copy link
Collaborator Author

rlepigre-skylabs-ai commented Feb 17, 2026

Seems like there is an actual issue?

@Alizter
Copy link
Collaborator

Alizter commented Feb 17, 2026 •
edited
Loading

@rlepigre-skylabs-ai Yes, the native rocq tests have some changes. If you just update the test file like the CI suggests that will work.

With nix you can do nix develop .#rocq-native -c make test-rocq-native to run the tests like the CI does.

@rlepigre-skylabs-ai
Copy link
Collaborator Author

rlepigre-skylabs-ai commented Feb 17, 2026

@Alizter sure, I was just wondering if the fact that we have this diff is a good thing or not. Seems like we now have some duplication in the name of some files (...extract_extract.cmi).

Alizter
Alizter reviewed Feb 17, 2026
View reviewed changes
@Alizter
Copy link
Collaborator

Alizter commented Feb 17, 2026

@rlepigre-skylabs-ai The awkward naming is just from picking the name as "extract" in both the prelude and the module. I don't think its a big deal.

@rlepigre-skylabs-ai
Fix ocaml#8042, multiple rocq.extraction in directory.
12c8f16 
Signed-off-by: Rodolphe Lepigre <rodolphe.lepigre@skylabs-ai.com>
@rlepigre-skylabs-ai
Copy link
Collaborator Author

rlepigre-skylabs-ai commented Feb 17, 2026

@Alizter I realized there was one hard-coded use of the wrapper name in rocqtop.ml, so I fixed it by exposing a function to get the wrapper name from the extraction stanza. Hopefully that's good enough.

@rlepigre-skylabs-ai
Factor wrapper for extraction, use in dune rocq top.
f216596 
Signed-off-by: Rodolphe Lepigre <rodolphe.lepigre@skylabs-ai.com>
@Alizter Alizter requested a review from rgrinberg February 17, 2026 18:16
@Alizter Alizter merged commit 46e51fa into ocaml:main Feb 18, 2026
29 checks passed
@shonfeder shonfeder mentioned this pull request Mar 2, 2026
Closed
shonfeder added a commit to shonfeder/opam-repository that referenced this pull request Mar 2, 2026
@shonfeder
[new release] dune (18 packages) (3.22.0~alpha0)
118a690 
CHANGES:

### Fixed

- `Dyn.to_string` now uses a smarter way to convert floats. This ensures that
  floats are printed with enough precision to round-trip and are valid OCaml
  lexemes. (ocaml/dune#12982, fixes ocaml/dune#12980, @Alizter)

- Fix `dune install --prefix` failing with relative paths outside the workspace
  like `../foo` (ocaml/dune#12993, fixes ocaml/dune#12241, @benodiwal)

- Delete sandboxes with broken permissions (ocaml/dune#13511, @rgrinberg)

- Fix compiling Menhir parsers that refer to sibling modules within a
  subdirectory of `(include_subdirs qualified)`. (ocaml/dune#13118, fixes ocaml/dune#11119,
  @anmonteiro)

- Fixed the dependency specification of C stubs, which could result in C
  stubs not getting rebuilt when needed (which could in turn lead to
  segmentation faults and other hard-to-track bugs).
  (ocaml/dune#13652, fixes ocaml/dune#13651, @nojb)

- Fix rpc not transferring promotion warnings to the client
  (ocaml/dune#12604, fixes ocaml/dune#12578, @ElectreAAS)

- Fix issue where `dune exec -w` was unable to kill running programs on
  rebuild. (ocaml/dune#12360, fixes ocaml/dune#12323, @Alizter)

- Resolve context and workspace binaries introduced by the respective `(env
  (binaries ..))` stanzas. (ocaml/dune#12952, fixes ocaml/dune#6220, @anmonteiro)

- Fix `diff` promotions originating from sandboxed rules. Previously, they
  would be completely ignored as the sandbox with the promoted file would be
  destroyed if the promotion fired (ocaml/dune#13520, @rgrinberg)

- Fix failure to digest installed directory targets, allowing them to be used
  as dependencies to other rules. (ocaml/dune#13045, @anmonteiro)

- Fix handling of `(select ..)` field when used with `(include_subdirs ..)`.
  `(select <path> from ..)` modules now parse `path` as a relative path
  starting from the module group root (ocaml/dune#13175, fixes ocaml/dune#4383, ocaml/dune#12450,
  @anmonteiro)

- Fix dune trying to kill processes that were already reaped due to race
  conditions (ocaml/dune#13245, @rgrinberg)

- Add `O_CLOEXEC` to all files used for stdin/stdout/stderr (ocaml/dune#13385, @rgrinberg)

- Fix `$ dune promote dir/foo` when `dir` does not exist (ocaml/dune#13493, @rgrinberg)

- Fix `(select ..)` field evaluation when a transitive library has optional
  dependencies (fixes ocaml/dune#13299, ocaml/dune#13389, @anmonteiro)

- Fix sandboxed builds of `library` stanzas that set
  `(stdlib (modules_before_stdlib ..))` (ocaml/dune#13624, @anmonteiro)

- Fixed non-build caches not following `$DUNE_CACHE_ROOT` and instead only
  relying on `$XDG_CACHE_HOME`.
  This means the normal build cache moves:
  `$DUNE_CACHE_ROOT -> $DUNE_CACHE_ROOT/db` (no changes if that variable was
  unset). Affected users can prevent a full cache invalidation by moving
  previous contents:
  `cd $DUNE_CACHE_ROOT; mkdir db; mv <contents of directory> db`.
  (ocaml/dune#11612, fixes ocaml/dune#11584, @ElectreAAS)

- `$ dune promotion list` writes output to stdout rather than stderr (ocaml/dune#13462)

- Improve handling of empty files in the `diff` action. These are now correctly
  distinguished from *empty* files. (ocaml/dune#13696, @rgrinberg)

- Pass `/dev/null` to `--diff-command` instead of non-existent files (ocaml/dune#13696,
  @rgrinberg)

- Fix failure when multiple `rocq.extraction` stanzas existing in a directory
  (ocaml/dune#13531, fixes ocaml/dune#8042, @rlepigre-skylabs-ai)

- Print `$ dune promotion show` output to stdout rather than stderr (ocaml/dune#13481,
  @rgrinberg)

- Fix deadlock in the `memo` library in the presence of dependency cycles
  (ocaml/dune#13625, @anmonteiro)

- Fix promotions that modify a directory into a file (ocaml/dune#13516, fixes ocaml/dune#4067,
  @rgrinberg)

- Fix installation of implementations of virtual libraries. This failed when
  the implementation had no private modules, but the virtual library did
  (ocaml/dune#10635, @rgrinberg)

- Respect the `(dir ..)` field on packages when setting up cram tests (ocaml/dune#13581,
  @rgrinberg)

### Added

- Add support for generating `.cms` files using oxcaml and adding `.cms` or
  `.cmt` files as compilation dependencies (ocaml/dune#13397, @spiessimon)

- Add trace events for custom actions (ocaml/dune#13265, @rgrinberg)

- Allow enabling extensions with `(using ..)` in `dune-workspace` files
  (ocaml/dune#13395, @spiessimon)

- Add sandbox extraction trace event (ocaml/dune#13544, @rgrinberg)

- Add the initial cwd to the first config event (ocaml/dune#13026, @rgrinberg)

- Dune produces trace events in `DUNE_ACTION_TRACE_DIR` if this variable
  is set. (ocaml/dune#13302, @rgrinberg)

- Add file watching events to the trace file (ocaml/dune#13038, @rgrinberg)

- Introduce the `$ dune trace cat` subcommand to view the trace file. (ocaml/dune#13055,
  @rgrinberg)

- Add diagnostic events to the trace. (ocaml/dune#13041, @rgrinberg)

- Add `DUNE_JOBS` environment variable for controlling concurrency of Dune from
  environment. The `INSIDE_DUNE` variable also now no longer controls
  concurrency (ocaml/dune#12800, @Alizter)

- Support for Rocq expected output tests (ocaml/dune#13632, @rlepigre-skylabs-ai)

- Add `rusage` information to completed processes in the trace (@rgrinberg,
  ocaml/dune#13241)

- Add process start events to the trace (ocaml/dune#13261, rgrinberg)

- Generate odoc documentation in markdown using the `@doc-markdown` alias
  (ocaml/dune#12581, @davesnx)

- Add timing information for every command executed by cram (ocaml/dune#13092,
  @rgrinberg)

- Add the workspace root to the config trace event (ocaml/dune#12922, @rgrinberg)

- Introduce the `dune-action-trace` library. This public library is to be used
  by custom actions to emit trace events while executed as part of a dune
  build. The trace events emitted through this library will be incorporated
  into dune's own trace (ocaml/dune#13348, @rgrinberg)

- Add `dune-find-dominating` to `dune.el`, a command to find the
  dominating dune file. (ocaml/dune#12696, @arvidj)

- Add a `--no-recursive` flag to `$ dune describe workspace` (ocaml/dune#13590, @rgrinberg)

- Trace events for files written directly by dune (ocaml/dune#13618, @rgrinberg)

- Allow expansion of special forms like `(:include ..)` and `%{read-lines:..}`
  in the `modules` specification for the `ocamllex`, `ocamlyacc` and `menhir`
  stanzas. (ocaml/dune#13105, ocaml/dune#13135, ocaml/dune#13157, @anmonteiro)

- Add a trace event for snapshotting the sandbox (ocaml/dune#13541, @rgrinberg)

- Add signal send and receive events to the trace (ocaml/dune#13193, @rgrinberg)

- Emit final trace event before exiting. (ocaml/dune#13018, @rgrinberg)

- `dune runtest` can now run individual test executables from `(tests)` stanzas
  and inline tests from `(library (inline_tests))` stanzas by providing their
  source files as arguments. (ocaml/dune#13064, fixes ocaml/dune#870, @Alizter)

- Add a `shell` field to the cram stanza. This field allows customizing the
  shell to be `bash` rather than `sh` (ocaml/dune#13083, @haochenx)

### Changed

- Start sandboxing the execution of tests defined with the `test` and `tests`
  stanzas (ocaml/dune#13510, ocaml/dune#13617, @rgrinberg)

- Disabled cram tests can now be run explicitly with `dune runtest disabled.t`.
  The `enabled_if` field now only controls whether a test is included in
  the `@runtest` alias. (ocaml/dune#13081, @Alizter)

- Process categories in trace events are moved to their own field in `args`
  (ocaml/dune#13024, @rgrinberg)

- Sandbox running `ocamllex` and `ocamlyacc` actions. (ocaml/dune#13098, @anmonteiro)

- Sandboxing mdx test actions is now the default starting from `0.5` (ocaml/dune#13504,
  @rgrinberg)

- Start sandboxing Melange rules by default in the `(library ..)` and
  `(melange.emit ..)` stanzas (ocaml/dune#13619, @anmonteiro)

- Introduce a promotion trace event and remove the corresponding verbose log
  message. (ocaml/dune#12949, ocaml/dune#13444, @rgrinberg)

- Change dune's trace format to emit canonical s-expressions. This improves
  performance and is better aligned with dune's usage of the format
  elsewhere. `$ dune trace cat` can also emit the trace in `--chrome-trace`
  for perfetto, or `--sexp` for regular s-expressions for interactive usage.
  (ocaml/dune#13059, @rgrinberg)

- Move all logging statements to the trace file. All log statements now contain
  structured payloads (ocaml/dune#13015, fixes ocaml/dune#12904, @rgrinberg)

- Add a target resolution event to replace the equivalent log message (ocaml/dune#12955,
  @rgrinberg)
@shonfeder shonfeder mentioned this pull request Mar 11, 2026
Closed
shonfeder added a commit to shonfeder/opam-repository that referenced this pull request Mar 11, 2026
@shonfeder
[new release] dune (18 packages) (3.22.0~alpha1)
f5aa06a 
CHANGES:

### Fixed

- `Dyn.to_string` now uses a smarter way to convert floats. This ensures that
  floats are printed with enough precision to round-trip and are valid OCaml
  lexemes. (ocaml/dune#12982, fixes ocaml/dune#12980, @Alizter)

- Fix `dune install --prefix` failing with relative paths outside the workspace
  like `../foo` (ocaml/dune#12993, fixes ocaml/dune#12241, @benodiwal)

- Place the default trace file inside the build directory at the
  workspace root, rather than relative to the current directory.
  (ocaml/dune#13735, @vouillon)

- Fixed interpreting relative paths in `%{bin:..}` and `%{bin-available:..}`.
  These are now interpreted correctly, relative to the dune file they're in.
  (ocaml/dune#13712, fixes ocaml/dune#9564, @anmonteiro)

- Delete sandboxes with broken permissions (ocaml/dune#13511, @rgrinberg)

- Fix compiling Menhir parsers that refer to sibling modules within a
  subdirectory of `(include_subdirs qualified)`. (ocaml/dune#13118, fixes ocaml/dune#11119,
  @anmonteiro)

- Fixed the dependency specification of C stubs, which could result in C
  stubs not getting rebuilt when needed (which could in turn lead to
  segmentation faults and other hard-to-track bugs).
  (ocaml/dune#13652, fixes ocaml/dune#13651, @nojb)

- Fix the Dune cache on Windows by correctly handling renames onto read-only
  files. Before this change, the Dune cache would be filled but the stored
  artifacts would not generally be usable by Dune. (ocaml/dune#13713, @Nevor)

- Fix rpc not transferring promotion warnings to the client
  (ocaml/dune#12604, fixes ocaml/dune#12578, @ElectreAAS)

- Fix issue where `dune exec -w` was unable to kill running programs on
  rebuild. (ocaml/dune#12360, fixes ocaml/dune#12323, @Alizter)

- Fix package extraction on systems with tar implementations that don't
  auto-detect compression (e.g., OpenBSD). Dune now passes explicit
  decompression flags (-z for gzip, -j for bzip2) when needed, and provides
  clear error messages for unsupported formats like XZ and LZMA. (ocaml/dune#13688,
  fixes ocaml/dune#10123, @Alizter)

- Resolve context and workspace binaries introduced by the respective `(env
  (binaries ..))` stanzas. (ocaml/dune#12952, fixes ocaml/dune#6220, @anmonteiro)

- Fix `diff` promotions originating from sandboxed rules. Previously, they
  would be completely ignored as the sandbox with the promoted file would be
  destroyed if the promotion fired (ocaml/dune#13520, @rgrinberg)

- Fix failure to digest installed directory targets, allowing them to be used
  as dependencies to other rules. (ocaml/dune#13045, @anmonteiro)

- Fix handling of `(select ..)` field when used with `(include_subdirs ..)`.
  `(select <path> from ..)` modules now parse `path` as a relative path
  starting from the module group root (ocaml/dune#13175, fixes ocaml/dune#4383, ocaml/dune#12450,
  @anmonteiro)

- Fix dune trying to kill processes that were already reaped due to race
  conditions (ocaml/dune#13245, @rgrinberg)

- Add `O_CLOEXEC` to all files used for stdin/stdout/stderr (ocaml/dune#13385, @rgrinberg)

- Fix `$ dune promote dir/foo` when `dir` does not exist (ocaml/dune#13493, @rgrinberg)

- Fix `(select ..)` field evaluation when a transitive library has optional
  dependencies (fixes ocaml/dune#13299, ocaml/dune#13389, @anmonteiro)

- Fix sandboxed builds of `library` stanzas that set
  `(stdlib (modules_before_stdlib ..))` (ocaml/dune#13624, @anmonteiro)

- Dune cache: use of hard links under Windows. (ocaml/dune#13714, @Nevor)

- Fixed non-build caches not following `$DUNE_CACHE_ROOT` and instead only
  relying on `$XDG_CACHE_HOME`.
  This means the normal build cache moves:
  `$DUNE_CACHE_ROOT -> $DUNE_CACHE_ROOT/db` (no changes if that variable was
  unset). Affected users can prevent a full cache invalidation by moving
  previous contents:
  `cd $DUNE_CACHE_ROOT; mkdir db; mv <contents of directory> db`.
  (ocaml/dune#11612, fixes ocaml/dune#11584, @ElectreAAS)

- `$ dune promotion list` writes output to stdout rather than stderr (ocaml/dune#13462)

- Improve handling of empty files in the `diff` action. These are now correctly
  distinguished from *empty* files. (ocaml/dune#13696, @rgrinberg)
- Pass `/dev/null` to `--diff-command` instead of non-existent files (ocaml/dune#13696,
  @rgrinberg)

- Fix failure when multiple `rocq.extraction` stanzas existing in a directory
  (ocaml/dune#13531, fixes ocaml/dune#8042, @rlepigre-skylabs-ai)

- Print `$ dune promotion show` output to stdout rather than stderr (ocaml/dune#13481,
  @rgrinberg)

- Fix deadlock in the `memo` library in the presence of dependency cycles
  (ocaml/dune#13625, @anmonteiro)

- Fix promotions that modify a directory into a file (ocaml/dune#13516, fixes ocaml/dune#4067,
  @rgrinberg)

- Fix installation of implementations of virtual libraries. This failed when
  the implementation had no private modules, but the virtual library did
  (ocaml/dune#10635, @rgrinberg)

- Respect the `(dir ..)` field on packages when setting up cram tests (ocaml/dune#13581,
  @rgrinberg)

### Added

- Add support for generating `.cms` files using oxcaml and adding `.cms` or
  `.cmt` files as compilation dependencies (ocaml/dune#13397, @spiessimon)

- Add trace events for custom actions (ocaml/dune#13265, @rgrinberg)

- Allow enabling extensions with `(using ..)` in `dune-workspace` files
  (ocaml/dune#13395, @spiessimon)

- Add sandbox extraction trace event (ocaml/dune#13544, @rgrinberg)

- Add the initial cwd to the first config event (ocaml/dune#13026, @rgrinberg)

- Dune dune produces trace events in `DUNE_ACTION_TRACE_DIR` if this variable
  is set. (ocaml/dune#13302, @rgrinberg)

- Add file watching events to the trace file (ocaml/dune#13038, @rgrinberg)

- Introduce the `$ dune trace cat` subcommand to view the trace file. (ocaml/dune#13055,
  @rgrinberg)

- Add diagnostic events to the trace. (ocaml/dune#13041, @rgrinberg)

- Add `DUNE_JOBS` environment variable for controlling concurrency of Dune from
  environment. The `INSIDE_DUNE` variable also now no longer controls
  concurrency (ocaml/dune#12800, @Alizter)

- Support for Rocq expected output tests (ocaml/dune#13632, @rlepigre-skylabs-ai)

- Add `rusage` information to completed processes in the trace (@rgrinberg,
  ocaml/dune#13241)

- Add process start events to the trace (ocaml/dune#13261, rgrinberg)

- Generate odoc documentation in markdown using the `@doc-markdown` alias
  (ocaml/dune#12581, @davesnx)

- Add timing information for every command executed by cram (ocaml/dune#13092,
  @rgrinberg)

- Add the workspace root to the config trace event (ocaml/dune#12922, @rgrinberg)

- Introduce the `dune-action-trace` library. This public library is to be used
  by custom actions to emit trace events while executed as part of a dune
  build. The trace events emitted through this library will be incorporated
  into dune's own trace (ocaml/dune#13348, @rgrinberg)

- Add `dune-find-dominating` to `dune.el`, a command to find the
  dominating dune file. (ocaml/dune#12696, @arvidj)

- Add a `--no-recursive` flag to `$ dune describe workspace` (ocaml/dune#13590, @rgrinberg)

- Trace events for files written directly by dune (ocaml/dune#13618, @rgrinberg)

- Allow expansion of special forms like `(:include ..)` and `%{read-lines:..}`
  in the `modules` specification for the `ocamllex`, `ocamlyacc` and `menhir`
  stanzas. (ocaml/dune#13105, ocaml/dune#13135, ocaml/dune#13157, @anmonteiro)

- Add a trace event for snapshotting the asndbox (ocaml/dune#13541, @rgrinberg)

- Add signal send and receive events to the trace (ocaml/dune#13193, @rgrinberg)

- Emit final trace event before exiting. (ocaml/dune#13018, @rgrinberg)

- `dune runtest` can now run individual test executables from `(tests)` stanzas
  and inline tests from `(library (inline_tests))` stanzas by providing their
  source files as arguments. (ocaml/dune#13064, fixes ocaml/dune#870, @Alizter)

- Add a `shell` field to the cram stanza. This field allows customizing the
  shell to be `bash` rather than `sh` (ocaml/dune#13083, @haochenx)

### Changed

- Start sandboxing the execution of tests defined with the `test` and `tests`
  stanzas (ocaml/dune#13510, ocaml/dune#13617, @rgrinberg)

- Disabled cram tests can now be run explicitly with `dune runtest disabled.t`.
  The `enabled_if` field now only controls whether a test is included in
  the `@runtest` alias. (ocaml/dune#13081, @Alizter)

- Process categories in trace events are moved to their own field in `args`
  (ocaml/dune#13024, @rgrinberg)

- Sandbox running `ocamllex` and `ocamlyacc` actions. (ocaml/dune#13098, @anmonteiro)

- Sandboxing mdx test actions is now the default starting from `0.5` (ocaml/dune#13504,
  @rgrinberg)

- Start sandboxing Melange rules by default in the `(library ..)` and
  `(melange.emit ..)` stanzas (ocaml/dune#13619, @anmonteiro)

- Introduce a promotion trace event and remove the corresponding verbose log
  message. (ocaml/dune#12949, ocaml/dune#13444, @rgrinberg)

- Change dune's trace format to emit canonical s-expressions. This improves
  performance and is better aligned with dune's usage of the format
  elsewhere. `$ dune trace cat` can also emit the trace in `--chrome-trace`
  for perfetto, or `--sexp` for regular s-expressions for interactive usage.
  (ocaml/dune#13059, @rgrinberg)

- Move all logging statements to the trace file. All log statements now contain
  structured payloads (ocaml/dune#13015, fixes ocaml/dune#12904, @rgrinberg)

- Add a target resolution event to replace the equivalent log message (ocaml/dune#12955,
  @rgrinberg)
shonfeder added a commit to shonfeder/opam-repository that referenced this pull request Mar 16, 2026
@shonfeder
[new release] dune (18 packages) (3.22.0~alpha2)
19c70fd 
CHANGES:

### Fixed

- `Dyn.to_string` now uses a smarter way to convert floats. This ensures that
  floats are printed with enough precision to round-trip and are valid OCaml
  lexemes. (ocaml/dune#12982, fixes ocaml/dune#12980, @Alizter)

- Fix `dune install --prefix` failing with relative paths outside the workspace
  like `../foo` (ocaml/dune#12993, fixes ocaml/dune#12241, @benodiwal)

- Place the default trace file inside the build directory at the
  workspace root, rather than relative to the current directory.
  (ocaml/dune#13735, @vouillon)

- Fixed interpreting relative paths in `%{bin:..}` and `%{bin-available:..}`.
  These are now interpreted correctly, relative to the dune file they're in.
  (ocaml/dune#13712, fixes ocaml/dune#9564, @anmonteiro)

- Delete sandboxes with broken permissions (ocaml/dune#13511, @rgrinberg)

- Fix compiling Menhir parsers that refer to sibling modules within a
  subdirectory of `(include_subdirs qualified)`. (ocaml/dune#13118, fixes ocaml/dune#11119,
  @anmonteiro)

- Fixed the dependency specification of C stubs, which could result in C
  stubs not getting rebuilt when needed (which could in turn lead to
  segmentation faults and other hard-to-track bugs).
  (ocaml/dune#13652, fixes ocaml/dune#13651, @nojb)

- Fix the Dune cache on Windows by correctly handling renames onto read-only
  files. Before this change, the Dune cache would be filled but the stored
  artifacts would not generally be usable by Dune. (ocaml/dune#13713, @Nevor)

- Fix rpc not transferring promotion warnings to the client
  (ocaml/dune#12604, fixes ocaml/dune#12578, @ElectreAAS)

- Fix issue where `dune exec -w` was unable to kill running programs on
  rebuild. (ocaml/dune#12360, fixes ocaml/dune#12323, @Alizter)

- Fix package extraction on systems with tar implementations that don't
  auto-detect compression (e.g., OpenBSD). Dune now passes explicit
  decompression flags (-z for gzip, -j for bzip2) when needed, and provides
  clear error messages for unsupported formats like XZ and LZMA. (ocaml/dune#13688,
  fixes ocaml/dune#10123, @Alizter)

- Resolve context and workspace binaries introduced by the respective `(env
  (binaries ..))` stanzas. (ocaml/dune#12952, fixes ocaml/dune#6220, @anmonteiro)

- Fix `diff` promotions originating from sandboxed rules. Previously, they
  would be completely ignored as the sandbox with the promoted file would be
  destroyed if the promotion fired (ocaml/dune#13520, @rgrinberg)

- Fix failure to digest installed directory targets, allowing them to be used
  as dependencies to other rules. (ocaml/dune#13045, @anmonteiro)

- Fix handling of `(select ..)` field when used with `(include_subdirs ..)`.
  `(select <path> from ..)` modules now parse `path` as a relative path
  starting from the module group root (ocaml/dune#13175, fixes ocaml/dune#4383, ocaml/dune#12450,
  @anmonteiro)

- Fix dune trying to kill processes that were already reaped due to race
  conditions (ocaml/dune#13245, @rgrinberg)

- Add `O_CLOEXEC` to all files used for stdin/stdout/stderr (ocaml/dune#13385, @rgrinberg)

- Fix `$ dune promote dir/foo` when `dir` does not exist (ocaml/dune#13493, @rgrinberg)

- Fix `(select ..)` field evaluation when a transitive library has optional
  dependencies (fixes ocaml/dune#13299, ocaml/dune#13389, @anmonteiro)

- Fix sandboxed builds of `library` stanzas that set
  `(stdlib (modules_before_stdlib ..))` (ocaml/dune#13624, @anmonteiro)

- Dune cache: use of hard links under Windows. (ocaml/dune#13714, @Nevor)

- Fixed non-build caches not following `$DUNE_CACHE_ROOT` and instead only
  relying on `$XDG_CACHE_HOME`.
  This means the normal build cache moves:
  `$DUNE_CACHE_ROOT -> $DUNE_CACHE_ROOT/db` (no changes if that variable was
  unset). Affected users can prevent a full cache invalidation by moving
  previous contents:
  `cd $DUNE_CACHE_ROOT; mkdir db; mv <contents of directory> db`.
  (ocaml/dune#11612, fixes ocaml/dune#11584, @ElectreAAS)

- `$ dune promotion list` writes output to stdout rather than stderr (ocaml/dune#13462)

- Improve handling of empty files in the `diff` action. These are now correctly
  distinguished from *empty* files. (ocaml/dune#13696, @rgrinberg)
- Pass `/dev/null` to `--diff-command` instead of non-existent files (ocaml/dune#13696,
  @rgrinberg)

- Fix failure when multiple `rocq.extraction` stanzas existing in a directory
  (ocaml/dune#13531, fixes ocaml/dune#8042, @rlepigre-skylabs-ai)

- Print `$ dune promotion show` output to stdout rather than stderr (ocaml/dune#13481,
  @rgrinberg)

- Fix deadlock in the `memo` library in the presence of dependency cycles
  (ocaml/dune#13625, @anmonteiro)

- Fix promotions that modify a directory into a file (ocaml/dune#13516, fixes ocaml/dune#4067,
  @rgrinberg)

- Fix installation of implementations of virtual libraries. This failed when
  the implementation had no private modules, but the virtual library did
  (ocaml/dune#10635, @rgrinberg)

- Respect the `(dir ..)` field on packages when setting up cram tests (ocaml/dune#13581,
  @rgrinberg)

### Added

- Add support for generating `.cms` files using oxcaml and adding `.cms` or
  `.cmt` files as compilation dependencies (ocaml/dune#13397, @spiessimon)

- Add trace events for custom actions (ocaml/dune#13265, @rgrinberg)

- Allow enabling extensions with `(using ..)` in `dune-workspace` files
  (ocaml/dune#13395, @spiessimon)

- Add sandbox extraction trace event (ocaml/dune#13544, @rgrinberg)

- Add the initial cwd to the first config event (ocaml/dune#13026, @rgrinberg)

- Dune dune produces trace events in `DUNE_ACTION_TRACE_DIR` if this variable
  is set. (ocaml/dune#13302, @rgrinberg)

- Add file watching events to the trace file (ocaml/dune#13038, @rgrinberg)

- Introduce the `$ dune trace cat` subcommand to view the trace file. (ocaml/dune#13055,
  @rgrinberg)

- Add diagnostic events to the trace. (ocaml/dune#13041, @rgrinberg)

- Add `DUNE_JOBS` environment variable for controlling concurrency of Dune from
  environment. The `INSIDE_DUNE` variable also now no longer controls
  concurrency (ocaml/dune#12800, @Alizter)

- Support for Rocq expected output tests (ocaml/dune#13632, @rlepigre-skylabs-ai)

- Add `rusage` information to completed processes in the trace (@rgrinberg,
  ocaml/dune#13241)

- Add process start events to the trace (ocaml/dune#13261, rgrinberg)

- Generate odoc documentation in markdown using the `@doc-markdown` alias
  (ocaml/dune#12581, @davesnx)

- Add timing information for every command executed by cram (ocaml/dune#13092,
  @rgrinberg)

- Add the workspace root to the config trace event (ocaml/dune#12922, @rgrinberg)

- Introduce the `dune-action-trace` library. This public library is to be used
  by custom actions to emit trace events while executed as part of a dune
  build. The trace events emitted through this library will be incorporated
  into dune's own trace (ocaml/dune#13348, @rgrinberg)

- Add `dune-find-dominating` to `dune.el`, a command to find the
  dominating dune file. (ocaml/dune#12696, @arvidj)

- Add a `--no-recursive` flag to `$ dune describe workspace` (ocaml/dune#13590, @rgrinberg)

- Trace events for files written directly by dune (ocaml/dune#13618, @rgrinberg)

- Allow expansion of special forms like `(:include ..)` and `%{read-lines:..}`
  in the `modules` specification for the `ocamllex`, `ocamlyacc` and `menhir`
  stanzas. (ocaml/dune#13105, ocaml/dune#13135, ocaml/dune#13157, @anmonteiro)

- Add a trace event for snapshotting the asndbox (ocaml/dune#13541, @rgrinberg)

- Add signal send and receive events to the trace (ocaml/dune#13193, @rgrinberg)

- Emit final trace event before exiting. (ocaml/dune#13018, @rgrinberg)

- `dune runtest` can now run individual test executables from `(tests)` stanzas
  and inline tests from `(library (inline_tests))` stanzas by providing their
  source files as arguments. (ocaml/dune#13064, fixes ocaml/dune#870, @Alizter)

- Add a `shell` field to the cram stanza. This field allows customizing the
  shell to be `bash` rather than `sh` (ocaml/dune#13083, @haochenx)

### Changed

- Start sandboxing the execution of tests defined with the `test` and `tests`
  stanzas (ocaml/dune#13510, ocaml/dune#13617, @rgrinberg)

- Disabled cram tests can now be run explicitly with `dune runtest disabled.t`.
  The `enabled_if` field now only controls whether a test is included in
  the `@runtest` alias. (ocaml/dune#13081, @Alizter)

- Process categories in trace events are moved to their own field in `args`
  (ocaml/dune#13024, @rgrinberg)

- Sandbox running `ocamllex` and `ocamlyacc` actions. (ocaml/dune#13098, @anmonteiro)

- Sandboxing mdx test actions is now the default starting from `0.5` (ocaml/dune#13504,
  @rgrinberg)

- Start sandboxing Melange rules by default in the `(library ..)` and
  `(melange.emit ..)` stanzas (ocaml/dune#13619, @anmonteiro)

- Introduce a promotion trace event and remove the corresponding verbose log
  message. (ocaml/dune#12949, ocaml/dune#13444, @rgrinberg)

- Change dune's trace format to emit canonical s-expressions. This improves
  performance and is better aligned with dune's usage of the format
  elsewhere. `$ dune trace cat` can also emit the trace in `--chrome-trace`
  for perfetto, or `--sexp` for regular s-expressions for interactive usage.
  (ocaml/dune#13059, @rgrinberg)

- Move all logging statements to the trace file. All log statements now contain
  structured payloads (ocaml/dune#13015, fixes ocaml/dune#12904, @rgrinberg)

- Add a target resolution event to replace the equivalent log message (ocaml/dune#12955,
  @rgrinberg)
@shonfeder shonfeder mentioned this pull request Mar 16, 2026
Closed
shonfeder added a commit to shonfeder/opam-repository that referenced this pull request Mar 19, 2026
@shonfeder
[new release] dune (18 packages) (3.22.0)
79d2d92 
CHANGES:

### Fixed

- `Dyn.to_string` now uses a smarter way to convert floats. This ensures that
  floats are printed with enough precision to round-trip and are valid OCaml
  lexemes. (ocaml/dune#12982, fixes ocaml/dune#12980, @Alizter)

- Fix `dune install --prefix` failing with relative paths outside the workspace
  like `../foo` (ocaml/dune#12993, fixes ocaml/dune#12241, @benodiwal)

- Place the default trace file inside the build directory at the
  workspace root, rather than relative to the current directory.
  (ocaml/dune#13735, @vouillon)

- Fixed interpreting relative paths in `%{bin:..}` and `%{bin-available:..}`.
  These are now interpreted correctly, relative to the dune file they're in.
  (ocaml/dune#13712, fixes ocaml/dune#9564, @anmonteiro)

- Delete sandboxes with broken permissions (ocaml/dune#13511, @rgrinberg)

- Fix compiling Menhir parsers that refer to sibling modules within a
  subdirectory of `(include_subdirs qualified)`. (ocaml/dune#13118, fixes ocaml/dune#11119,
  @anmonteiro)

- Fixed the dependency specification of C stubs, which could result in C
  stubs not getting rebuilt when needed (which could in turn lead to
  segmentation faults and other hard-to-track bugs).
  (ocaml/dune#13652, fixes ocaml/dune#13651, @nojb)

- Fix the Dune cache on Windows by correctly handling renames onto read-only
  files. Before this change, the Dune cache would be filled but the stored
  artifacts would not generally be usable by Dune. (ocaml/dune#13713, @Nevor)

- Fix rpc not transferring promotion warnings to the client
  (ocaml/dune#12604, fixes ocaml/dune#12578, @ElectreAAS)

- Fix issue where `dune exec -w` was unable to kill running programs on
  rebuild. (ocaml/dune#12360, fixes ocaml/dune#12323, @Alizter)

- Resolve context and workspace binaries introduced by the respective `(env
  (binaries ..))` stanzas. (ocaml/dune#12952, fixes ocaml/dune#6220, @anmonteiro)

- Fix `diff` promotions originating from sandboxed rules. Previously, they
  would be completely ignored as the sandbox with the promoted file would be
  destroyed if the promotion fired (ocaml/dune#13520, @rgrinberg)

- Fix failure to digest installed directory targets, allowing them to be used
  as dependencies to other rules. (ocaml/dune#13045, @anmonteiro)

- Fix handling of `(select ..)` field when used with `(include_subdirs ..)`.
  `(select <path> from ..)` modules now parse `path` as a relative path
  starting from the module group root (ocaml/dune#13175, fixes ocaml/dune#4383, ocaml/dune#12450,
  @anmonteiro)

- Fix dune trying to kill processes that were already reaped due to race
  conditions (ocaml/dune#13245, @rgrinberg)

- Add `O_CLOEXEC` to all files used for stdin/stdout/stderr (ocaml/dune#13385, @rgrinberg)

- Fix `$ dune promote dir/foo` when `dir` does not exist (ocaml/dune#13493, @rgrinberg)

- Fix `(select ..)` field evaluation when a transitive library has optional
  dependencies (fixes ocaml/dune#13299, ocaml/dune#13389, @anmonteiro)

- Fix sandboxed builds of `library` stanzas that set
  `(stdlib (modules_before_stdlib ..))` (ocaml/dune#13624, @anmonteiro)

- Dune cache: use of hard links under Windows. (ocaml/dune#13714, @Nevor)

- Fixed non-build caches not following `$DUNE_CACHE_ROOT` and instead only
  relying on `$XDG_CACHE_HOME`.
  This means the normal build cache moves:
  `$DUNE_CACHE_ROOT -> $DUNE_CACHE_ROOT/db` (no changes if that variable was
  unset). Affected users can prevent a full cache invalidation by moving
  previous contents:
  `cd $DUNE_CACHE_ROOT; mkdir db; mv <contents of directory> db`.
  (ocaml/dune#11612, fixes ocaml/dune#11584, @ElectreAAS)

- `$ dune promotion list` writes output to stdout rather than stderr (ocaml/dune#13462)

- Improve handling of empty files in the `diff` action. These are now correctly
  distinguished from *empty* files. (ocaml/dune#13696, @rgrinberg)
- Pass `/dev/null` to `--diff-command` instead of non-existent files (ocaml/dune#13696,
  @rgrinberg)

- Fix failure when multiple `rocq.extraction` stanzas existing in a directory
  (ocaml/dune#13531, fixes ocaml/dune#8042, @rlepigre-skylabs-ai)

- Print `$ dune promotion show` output to stdout rather than stderr (ocaml/dune#13481,
  @rgrinberg)

- Fix deadlock in the `memo` library in the presence of dependency cycles
  (ocaml/dune#13625, @anmonteiro)

- Fix promotions that modify a directory into a file (ocaml/dune#13516, fixes ocaml/dune#4067,
  @rgrinberg)

- Fix installation of implementations of virtual libraries. This failed when
  the implementation had no private modules, but the virtual library did
  (ocaml/dune#10635, @rgrinberg)

- Respect the `(dir ..)` field on packages when setting up cram tests (ocaml/dune#13581,
  @rgrinberg)

### Added

- Add support for generating `.cms` files using oxcaml and adding `.cms` or
  `.cmt` files as compilation dependencies (ocaml/dune#13397, @spiessimon)

- Add trace events for custom actions (ocaml/dune#13265, @rgrinberg)

- Allow enabling extensions with `(using ..)` in `dune-workspace` files
  (ocaml/dune#13395, @spiessimon)

- Add sandbox extraction trace event (ocaml/dune#13544, @rgrinberg)

- Add the initial cwd to the first config event (ocaml/dune#13026, @rgrinberg)

- Dune dune produces trace events in `DUNE_ACTION_TRACE_DIR` if this variable
  is set. (ocaml/dune#13302, @rgrinberg)

- Add file watching events to the trace file (ocaml/dune#13038, @rgrinberg)

- Introduce the `$ dune trace cat` subcommand to view the trace file. (ocaml/dune#13055,
  @rgrinberg)

- Add diagnostic events to the trace. (ocaml/dune#13041, @rgrinberg)

- Add `DUNE_JOBS` environment variable for controlling concurrency of Dune from
  environment. The `INSIDE_DUNE` variable also now no longer controls
  concurrency (ocaml/dune#12800, @Alizter)

- Support for Rocq expected output tests (ocaml/dune#13632, @rlepigre-skylabs-ai)

- Add `rusage` information to completed processes in the trace (@rgrinberg,
  ocaml/dune#13241)

- Add process start events to the trace (ocaml/dune#13261, rgrinberg)

- Generate odoc documentation in markdown using the `@doc-markdown` alias
  (ocaml/dune#12581, @davesnx)

- Add timing information for every command executed by cram (ocaml/dune#13092,
  @rgrinberg)

- Add the workspace root to the config trace event (ocaml/dune#12922, @rgrinberg)

- Introduce the `dune-action-trace` library. This public library is to be used
  by custom actions to emit trace events while executed as part of a dune
  build. The trace events emitted through this library will be incorporated
  into dune's own trace (ocaml/dune#13348, @rgrinberg)

- Add `dune-find-dominating` to `dune.el`, a command to find the
  dominating dune file. (ocaml/dune#12696, @arvidj)

- Add a `--no-recursive` flag to `$ dune describe workspace` (ocaml/dune#13590, @rgrinberg)

- Trace events for files written directly by dune (ocaml/dune#13618, @rgrinberg)

- Allow expansion of special forms like `(:include ..)` and `%{read-lines:..}`
  in the `modules` specification for the `ocamllex`, `ocamlyacc` and `menhir`
  stanzas. (ocaml/dune#13105, ocaml/dune#13135, ocaml/dune#13157, @anmonteiro)

- Add a trace event for snapshotting the asndbox (ocaml/dune#13541, @rgrinberg)

- Add signal send and receive events to the trace (ocaml/dune#13193, @rgrinberg)

- Emit final trace event before exiting. (ocaml/dune#13018, @rgrinberg)

- `dune runtest` can now run individual test executables from `(tests)` stanzas
  and inline tests from `(library (inline_tests))` stanzas by providing their
  source files as arguments. (ocaml/dune#13064, fixes ocaml/dune#870, @Alizter)

- Add a `shell` field to the cram stanza. This field allows customizing the
  shell to be `bash` rather than `sh` (ocaml/dune#13083, @haochenx)

### Changed

- Start sandboxing the execution of tests defined with the `test` and `tests`
  stanzas (ocaml/dune#13510, ocaml/dune#13617, @rgrinberg)

- Disabled cram tests can now be run explicitly with `dune runtest disabled.t`.
  The `enabled_if` field now only controls whether a test is included in
  the `@runtest` alias. (ocaml/dune#13081, @Alizter)

- Process categories in trace events are moved to their own field in `args`
  (ocaml/dune#13024, @rgrinberg)

- Sandbox running `ocamllex` and `ocamlyacc` actions. (ocaml/dune#13098, @anmonteiro)

- Sandboxing mdx test actions is now the default starting from `0.5` (ocaml/dune#13504,
  @rgrinberg)

- Start sandboxing Melange rules by default in the `(library ..)` and
  `(melange.emit ..)` stanzas (ocaml/dune#13619, @anmonteiro)

- Introduce a promotion trace event and remove the corresponding verbose log
  message. (ocaml/dune#12949, ocaml/dune#13444, @rgrinberg)

- Change dune's trace format to emit canonical s-expressions. This improves
  performance and is better aligned with dune's usage of the format
  elsewhere. `$ dune trace cat` can also emit the trace in `--chrome-trace`
  for perfetto, or `--sexp` for regular s-expressions for interactive usage.
  (ocaml/dune#13059, @rgrinberg)

- Move all logging statements to the trace file. All log statements now contain
  structured payloads (ocaml/dune#13015, fixes ocaml/dune#12904, @rgrinberg)

- Add a target resolution event to replace the equivalent log message (ocaml/dune#12955,
  @rgrinberg)
@shonfeder shonfeder mentioned this pull request Mar 19, 2026
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

@rgrinberg rgrinberg Awaiting requested review from rgrinberg

Assignees

No one assigned

Labels

rocq

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Having several Coq extraction stanzas leads to multiple rule error from Dune 3.7

3 participants

@rlepigre-skylabs-ai @Alizter @rgrinberg