Skip to content

Add "coqdoc_header" and "coqdoc_footer" fields.#11131

Merged
Alizter merged 1 commit intoocaml:mainfrom
rlepigre:coqdoc-header-footer
Nov 13, 2025
Merged

Add "coqdoc_header" and "coqdoc_footer" fields.#11131
Alizter merged 1 commit intoocaml:mainfrom
rlepigre:coqdoc-header-footer

Conversation

@rlepigre
Copy link
Copy Markdown
Contributor

@rlepigre rlepigre commented Nov 18, 2024

This is an attempt at fixing #11017.

Although I have a working test-case, I have not done much testing so far. I'd appreciate early feedback anyway, if you can find the time to have a quick look @Alizter, @ejgallego.

What remains to be done:

  • Check for language version in the new fields.
  • Update the documentation.
  • Add change log entry.

@rlepigre rlepigre force-pushed the coqdoc-header-footer branch from 2091f8b to 969a669 Compare November 18, 2024 23:45
@maiste maiste added the coq label Nov 19, 2024
@rlepigre rlepigre force-pushed the coqdoc-header-footer branch from 969a669 to afd123d Compare November 19, 2024 19:20
@ejgallego ejgallego self-assigned this Nov 20, 2024
@Alizter
Copy link
Copy Markdown
Collaborator

Alizter commented Nov 20, 2024

While we are here, shall we add a field_b_o for toc. It should default to enabled, but we can allow it to be set like header and footer.

@Alizter
Copy link
Copy Markdown
Collaborator

Alizter commented Nov 20, 2024

We should add a test where the header file comes as the target of another rule. We need to check that the dependencies are being correctly handled.

Variable expansion is also another one that should be checked, but I'm not certain what the best way to do that is yet.

@rlepigre
Copy link
Copy Markdown
Contributor Author

We should add a test where the header file comes as the target of another rule. We need to check that the dependencies are being correctly handled.

Variable expansion is also another one that should be checked, but I'm not certain what the best way to do that is yet.

@Alizter I added a test that should exercise both at once.

While we are here, shall we add a field_b_o for toc. It should default to enabled, but we can allow it to be set like header and footer.

I'm not sure what you have in mind here, actually. Can't we just use the (coqdoc_flags ...) field for that?

@rlepigre rlepigre force-pushed the coqdoc-header-footer branch from 883ea56 to 7b75def Compare November 21, 2024 21:39
@Alizter
Copy link
Copy Markdown
Collaborator

Alizter commented Nov 21, 2024

While we are here, shall we add a field_b_o for toc. It should default to enabled, but we can allow it to be set like header and footer.

I'm not sure what you have in mind here, actually. Can't we just use the (coqdoc_flags ...) field for that?

we already set --toc by default. I thought it might be a good idea to introduce a field for that as well. It's not a priority however, so you can disregard that comment.

and+ coq_dump = Dune_rules.Coq.Coq_rules.coq_env ~dir >>| Dune_rules.Coq.Coq_flags.dump
and+ coq_dump =
Dune_rules.Coq.Coq_rules.coq_env ~dir
>>| Dune_rules.Coq.Coq_flags.dump ~dir:(Path.build dir)
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

I played around a bit with dropping the directory here, and I couldn't find a good way to do it. I'm not too worried about this.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Yeah, I wasn't sure what to do there.

@Alizter
Copy link
Copy Markdown
Collaborator

Alizter commented Nov 22, 2024

Does it make sense to pass these flags when in latex mode? I think this might error out coqdoc. Should be simple to add a test for that.

@rlepigre rlepigre force-pushed the coqdoc-header-footer branch from 7b75def to dc1181b Compare November 22, 2024 07:17
@rlepigre
Copy link
Copy Markdown
Contributor Author

Does it make sense to pass these flags when in latex mode? I think this might error out coqdoc. Should be simple to add a test for that.

The option is actually ignored (I had tested this), but I guess there is no point in introducing potential dependencies for the latex documentation. I pushed a fix.

@Alizter
Copy link
Copy Markdown
Collaborator

Alizter commented Mar 23, 2025

ping @ejgallego this was ready for a while but seems to have been forgotten.

@ejgallego
Copy link
Copy Markdown
Collaborator

I didn't forget about this, just no cycles left, sorry. I'll try to merge this soon, but feel free to take over if you got some cycles.

@ejgallego ejgallego added the rocq label Jul 17, 2025
rlepigre-skylabs-ai added a commit to SkyLabsAI/BRiCk that referenced this pull request Nov 4, 2025
This allows enabling the dune cache for building docs, while we wait for
ocaml/dune#11131 or something similar.
rlepigre-skylabs-ai added a commit to SkyLabsAI/BRiCk that referenced this pull request Nov 4, 2025
This allows enabling the dune cache for building docs, while we wait for
ocaml/dune#11131 or something similar.
rlepigre-skylabs-ai added a commit to SkyLabsAI/BRiCk that referenced this pull request Nov 4, 2025
This allows enabling the dune cache for building docs, while we wait for
ocaml/dune#11131 or something similar.
@rlepigre rlepigre force-pushed the coqdoc-header-footer branch 2 times, most recently from c002604 to a6e5a04 Compare November 13, 2025 13:52
@rlepigre
Copy link
Copy Markdown
Contributor Author

This has been ready for a while, can we get it merged @Alizter @ejgallego?

@rlepigre rlepigre force-pushed the coqdoc-header-footer branch from a6e5a04 to 4117f02 Compare November 13, 2025 14:00
@Alizter
Copy link
Copy Markdown
Collaborator

Alizter commented Nov 13, 2025

@rlepigre I can merge this once the tests have been fixed. The fix is to introduce version 0.11 of Coq lang.

@rlepigre rlepigre force-pushed the coqdoc-header-footer branch from 4117f02 to 13eebcf Compare November 13, 2025 19:01
@rlepigre
Copy link
Copy Markdown
Contributor Author

@rlepigre I can merge this once the tests have been fixed. The fix is to introduce version 0.11 of Coq lang.

Great, thank @Alizter. I think it fixed things correctly, but I'm not sure about the whole version business. Is 3.21 the right lang version to require for the 0.11 coq lang version?

Signed-off-by: Rodolphe Lepigre <lepigre@mpi-sws.org>
@rlepigre rlepigre force-pushed the coqdoc-header-footer branch from 13eebcf to 5fbfdd4 Compare November 13, 2025 19:18
@Alizter
Copy link
Copy Markdown
Collaborator

Alizter commented Nov 13, 2025

Yes, the version seems fine. We will likely cut a release for 3.21 soon anyway.

@Alizter Alizter merged commit 4e044e3 into ocaml:main Nov 13, 2025
26 checks passed
@rlepigre rlepigre deleted the coqdoc-header-footer branch November 13, 2025 21:28
@rlepigre
Copy link
Copy Markdown
Contributor Author

Great, thanks!

ejgallego added a commit to ejgallego/dune that referenced this pull request Nov 25, 2025
ejgallego added a commit to ejgallego/dune that referenced this pull request Nov 25, 2025
Co-authored-by: Rodolphe Lepigre <lepigre@mpi-sws.org>
Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
ejgallego added a commit to ejgallego/dune that referenced this pull request Nov 25, 2025
Co-authored-by: Rodolphe Lepigre <lepigre@mpi-sws.org>
Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
ejgallego added a commit to ejgallego/dune that referenced this pull request Nov 25, 2025
Co-authored-by: Rodolphe Lepigre <lepigre@mpi-sws.org>
Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
shonfeder added a commit to shonfeder/opam-repository that referenced this pull request Dec 15, 2025
CHANGES:

### Fixed

- Fix `include_subdirs qualified` incorrectly picking the furthest module
  instead of the closest when resolving module name ambiguities. (ocaml/dune#12587,
  @ElectreAAS and @Alizter)

- Fix: include the module alias in the transitive dependency closure with
  `(include_subdirs qualified)`. (ocaml/dune#12299, @anmonteiro)

- Improve error messages for invalid version formats containing non-ASCII
  characters. Previously, non-ASCII characters in version strings (e.g., `(lang
  dune è)` or `(using menhir π3.14)`) would fail with a generic "Invalid file"
  error. Now they display a clear message: "Invalid atom: contains non-ASCII
  character(s). Atoms must only contain ASCII characters." The fix is
  implemented at the lexer level, providing consistent error handling across all
  s-expression parsing. (ocaml/dune#12844, fixes ocaml/dune#12836, @benodiwal)

- Pass private modules with -H when this is available (ocaml/dune#12666, @rgrinberg)

- Allow multiple modules in `(modules_flags ...)`, in `coq.theory` (ocaml/dune#12733, @rlepigre)

- Improve error message for invalid version formats in both `(lang dune ...)` and
  `(using extension ...)` declarations. Changes "Atom of the form NNN.NNN expected"
  to "Invalid version. Version must be two numbers separated by a dot." (ocaml/dune#12833, @benodiwal)

- Fix crash when running `dune build @check` on a library with virtual modules.
  (ocaml/dune#12644, fixes ocaml/dune#12636, @Alizter)

- Provide a more informative error message when `(pkg enabled)` is put in
  `dune-project` instead of `dune-workspace`. (ocaml/dune#12802, fixes ocaml/dune#12801,
  @benodiwal)

- Improve error message when invalid version strings are used in `dune-project`
  files. Non-ASCII characters and malformed versions now show a helpful hint
  with an example of the correct format. (ocaml/dune#12794, fixes ocaml/dune#12751, @benodiwal)

- Stop hiding the `root_module` from the include path (ocaml/dune#12239, @rgrinberg)

- Allow `$ dune init` to work on absolute paths (ocaml/dune#12601, fixes ocaml/dune#7806,
  @rgrinberg)

- `(include_subdirs qualified)`: Add missing alias dependency to module group.
  (ocaml/dune#12530, @anmonteiro)

- Add Melange compilation to the `@all` alias in libraries (ocaml/dune#12628,
  @anmonteiro)

- Fix greedy version location in lang declarations. Previously, error locations for
  invalid lang versions would span multiple bytes for multi-byte UTF-8 characters,
  causing carets to appear misaligned and seemingly include the closing
  parenthesis. Now, error locations for ASCII strings show the full length (e.g.,
  "Ali" shows `^^^`), while non-ASCII strings show only the first byte (e.g., "è"
  shows `^`) to avoid multi-byte character display issues. (ocaml/dune#12869, fixes ocaml/dune#12806,
  @benodiwal)

- melange support: don't emit empty JavaScript modules for generated module
  aliases. (ocaml/dune#12464, @anmonteiro)

### Added

- (Experimental): Introduce the `library_parameter` stanza. It allows users to
  declare a parameter when using the OxCaml compiler.
  (ocaml/dune#11963, implements ocaml/dune#12084, @maiste)

- Added the ability to scroll horizontally in TUI. (ocaml/dune#12386, @Alizter)

- Feature: Include shell command that was executed when a cram test has
  occurred in the error message (ocaml/dune#12307, @rgrinberg)

-  support expanding variables in `(promote (into ..))` (ocaml/dune#12832, fixes ocaml/dune#12742,
   @anmonteiro)

- Add support for `%{cmt:...}` and `%{cmti:...}` variables to reference
  compiled annotation files (.cmt and .cmti) containing typed abstract syntax
  trees with location and type information. (ocaml/dune#12634, grants ocaml/dune#12633, @Alizter)

- Add `$ dune describe tests` to describe the tests in the workspace
  (@Gromototo, ocaml/dune#12545, fixes ocaml/dune#12030)

- Add `argv`, the process environment, and the dune version to the config event
  in the trace (ocaml/dune#12909, @rgrinberg)

- Allow `dune runtest` to properly run while a watch mode server is running.
  (ocaml/dune#12473, grants ocaml/dune#8114, @gridbugs and @ElectreAAS)

- Use copy-on-write (COW) when copying files on filesystems that support it
  (Btrfs, ZFS, XFS, etc), under Linux. (ocaml/dune#12074, fixes ocaml/dune#12071, @nojb)

- Add support for Tangled ATproto-based code repositories (ocaml/dune#12197, @avsm)

- Add support for instantiating OxCaml parameterised libraries.
  (ocaml/dune#12561, @art-w)

- Add a `(conflict_markers error|ignore)` option to the cram stanza. When
  `(conflict_markers error)` is set, the cram test will fail in the presence of
  conflict markers. Git, diff3 and jujutsu conflict markers are detected.
  (ocaml/dune#12538, ocaml/dune#12617, ocaml/dune#12655, fixes ocaml/dune#12512, @rgrinberg, @Alizter)

- Introduce a `%{ppx:lib1+..+libn}` stanza to make it possible to refer to ppx
  executables built by dune. This is useful for writing tests (ocaml/dune#12711,
  @rgrinberg)

- Introduce a `(dir ..)` field on packages defined in the `dune-project`. This
  field allows to associate a directory with a particular package. This makes
  dune automatically filter out all stanzas in this directory and its
  descendants with `--only-packages`. All users are recommended to switch to
  using this field. (ocaml/dune#12614, fixes ocaml/dune#3255, @rgrinberg)

- Add support for `DUNE_ROOT` environment variable, similar to the existing
  `--root` CLI parameter. (fixes ocaml/dune#12399 @sir4ur0n)

- Introduce an `unused-libs` alias to detect unused libraries.
  (ocaml/dune#12623, fixes ocaml/dune#650, @rgrinberg)

- Add `--files` flag to `dune describe opam-files` to print only the names of
  the opam files line by line. (ocaml/dune#9793, @reynir and @Alizter)

- `dune exec` now accepts absolute paths inside the workspace.
  (ocaml/dune#12094, @Alizter)

- Add `coqdoc_header` and `coqdoc_footer` fields to the `coq` field of the
  `env` stanza, and to the `coq.theory` stanza, allowing to configure a
  custom header or footer respectively in the HTML output of `coqdoc`.
  (ocaml/dune#11131, @rlepigre)

- Allow `dune fmt` to properly run while a watch mode server is running.
  Note that the `--preview` flag is not supported in this mode.
  (ocaml/dune#12064, @ElectreAAS)

- Support for generating `_CoqProject` files for `coq.theory` stanzas.
  (ocaml/dune#11752, @rlepigre)

- Added `(files)` stanza, similar to `(dirs)` to control which files are visible
  to Dune on a per-directory basis. (ocaml/dune#12879, @nojb)
- Add support for %{ocaml-config:ox} (ocaml/dune#12236, @jonludlam)

- Introduce `dune promotion show` command to display the contents of corrected
  files that are ready for promotion. This allows users to preview changes
  before running `dune promote`. The command accepts file arguments to show
  specific files, or displays all promotable files when called without
  arguments. (ocaml/dune#12669, fixes ocaml/dune#3883, @MixiMaxiMouse)
- New `(lang rocq)` build mode for Rocq 9.0 and later. This new mode
  is very similar to the existing `(lang coq)`, except that it doesn't
  need the `coq*` compatibility wrappers. As of today `(lang rocq)`
  doesn't support yet composed builds with Rocq itself, this will be
  added later.  `(lang coq)` is deprecated, development is frozen, and
  will be removed at some point in the future. (ocaml/dune#12035, @ejgallego,
  @Lysxia, fixes ocaml/dune#11572)

### Changed

- Don't run `ocamldep` to compute false dependencies on the `root_module`
  (ocaml/dune#12227, @rgrinberg)

- `dune format-dune-file` now uses the syntax version of the Dune project that
  contains the file being formatted (if any) instead of using the latest version
  available, which remains the default if there is no Dune project in scope.
  (ocaml/dune#11865, @nojb)

- Persistent DB and process events have been slightly modified. Persistent
  DB events have more concise names and job events always include full
  information. (ocaml/dune#12867, @rgrinberg)

- Removed the `--trace-extended` flag. Its functionality is always enabled when
  tracing is active (ocaml/dune#12908, @rgrinberg)

- The `test/dune` file generated by `dune init proj` now depends on the project library. (ocaml/dune#12791, @shonfeder)

- Starting with version 3.21 of the Dune language, Dune no longer changes the
  default set of compiler warnings. For users that would like to keep the old
  behaviour, the variable `%{dune-warnings}` can be used in an `(env)` stanza in
  a top-level Dune file: `(env (dev (flags :standard %{dune-warnings})))`.
  (ocaml/dune#12766, @nojb)
- Fix: stop generating `cmt` files for cinaps binaries (ocaml/dune#12530, @rgrinberg)
shonfeder added a commit to shonfeder/opam-repository that referenced this pull request Jan 5, 2026
CHANGES:

### Fixed

- Fix `include_subdirs qualified` incorrectly picking the furthest module
  instead of the closest when resolving module name ambiguities. (ocaml/dune#12587,
  @ElectreAAS and @Alizter)

- Fix: include the module alias in the transitive dependency closure with
  `(include_subdirs qualified)`. (ocaml/dune#12299, @anmonteiro)

- Improve error messages for invalid version formats containing non-ASCII
  characters. Previously, non-ASCII characters in version strings (e.g., `(lang
  dune è)` or `(using menhir π3.14)`) would fail with a generic "Invalid file"
  error. Now they display a clear message: "Invalid atom: contains non-ASCII
  character(s). Atoms must only contain ASCII characters." The fix is
  implemented at the lexer level, providing consistent error handling across all
  s-expression parsing. (ocaml/dune#12844, fixes ocaml/dune#12836, @benodiwal)

- Pass private modules with -H when this is available (ocaml/dune#12666, @rgrinberg)

- Allow multiple modules in `(modules_flags ...)`, in `coq.theory` (ocaml/dune#12733, @rlepigre)

- Improve error message for invalid version formats in both `(lang dune ...)` and
  `(using extension ...)` declarations. Changes "Atom of the form NNN.NNN expected"
  to "Invalid version. Version must be two numbers separated by a dot." (ocaml/dune#12833, @benodiwal)

- Fix crash when running `dune build @check` on a library with virtual modules.
  (ocaml/dune#12644, fixes ocaml/dune#12636, @Alizter)

- Provide a more informative error message when `(pkg enabled)` is put in
  `dune-project` instead of `dune-workspace`. (ocaml/dune#12802, fixes ocaml/dune#12801,
  @benodiwal)

- Improve error message when invalid version strings are used in `dune-project`
  files. Non-ASCII characters and malformed versions now show a helpful hint
  with an example of the correct format. (ocaml/dune#12794, fixes ocaml/dune#12751, @benodiwal)

- Stop hiding the `root_module` from the include path (ocaml/dune#12239, @rgrinberg)

- Allow `$ dune init` to work on absolute paths (ocaml/dune#12601, fixes ocaml/dune#7806,
  @rgrinberg)

- `(include_subdirs qualified)`: Add missing alias dependency to module group.
  (ocaml/dune#12530, @anmonteiro)

- Add Melange compilation to the `@all` alias in libraries (ocaml/dune#12628,
  @anmonteiro)

- Fix greedy version location in lang declarations. Previously, error locations for
  invalid lang versions would span multiple bytes for multi-byte UTF-8 characters,
  causing carets to appear misaligned and seemingly include the closing
  parenthesis. Now, error locations for ASCII strings show the full length (e.g.,
  "Ali" shows `^^^`), while non-ASCII strings show only the first byte (e.g., "è"
  shows `^`) to avoid multi-byte character display issues. (ocaml/dune#12869, fixes ocaml/dune#12806,
  @benodiwal)

- melange support: don't emit empty JavaScript modules for generated module
  aliases. (ocaml/dune#12464, @anmonteiro)

### Added

- (Experimental): Introduce the `library_parameter` stanza. It allows users to
  declare a parameter when using the OxCaml compiler.
  (ocaml/dune#11963, implements ocaml/dune#12084, @maiste)

- Added the ability to scroll horizontally in TUI. (ocaml/dune#12386, @Alizter)

- Feature: Include shell command that was executed when a cram test has
  occurred in the error message (ocaml/dune#12307, @rgrinberg)

-  support expanding variables in `(promote (into ..))` (ocaml/dune#12832, fixes ocaml/dune#12742,
   @anmonteiro)

- Add support for `%{cmt:...}` and `%{cmti:...}` variables to reference
  compiled annotation files (.cmt and .cmti) containing typed abstract syntax
  trees with location and type information. (ocaml/dune#12634, grants ocaml/dune#12633, @Alizter)

- Add `$ dune describe tests` to describe the tests in the workspace
  (@Gromototo, ocaml/dune#12545, fixes ocaml/dune#12030)

- Add `argv`, the process environment, and the dune version to the config event
  in the trace (ocaml/dune#12909, @rgrinberg)

- Allow `dune runtest` to properly run while a watch mode server is running.
  (ocaml/dune#12473, grants ocaml/dune#8114, @gridbugs and @ElectreAAS)

- Use copy-on-write (COW) when copying files on filesystems that support it
  (Btrfs, ZFS, XFS, etc), under Linux. (ocaml/dune#12074, fixes ocaml/dune#12071, @nojb)

- Add support for Tangled ATproto-based code repositories (ocaml/dune#12197, @avsm)

- Add support for instantiating OxCaml parameterised libraries.
  (ocaml/dune#12561, @art-w)

- Add a `(conflict_markers error|ignore)` option to the cram stanza. When
  `(conflict_markers error)` is set, the cram test will fail in the presence of
  conflict markers. Git, diff3 and jujutsu conflict markers are detected.
  (ocaml/dune#12538, ocaml/dune#12617, ocaml/dune#12655, fixes ocaml/dune#12512, @rgrinberg, @Alizter)

- Introduce a `%{ppx:lib1+..+libn}` stanza to make it possible to refer to ppx
  executables built by dune. This is useful for writing tests (ocaml/dune#12711,
  @rgrinberg)

- Introduce a `(dir ..)` field on packages defined in the `dune-project`. This
  field allows to associate a directory with a particular package. This makes
  dune automatically filter out all stanzas in this directory and its
  descendants with `--only-packages`. All users are recommended to switch to
  using this field. (ocaml/dune#12614, fixes ocaml/dune#3255, @rgrinberg)

- Add support for `DUNE_ROOT` environment variable, similar to the existing
  `--root` CLI parameter. (fixes ocaml/dune#12399 @sir4ur0n)

- Introduce an `unused-libs` alias to detect unused libraries.
  (ocaml/dune#12623, fixes ocaml/dune#650, @rgrinberg)

- Add `--files` flag to `dune describe opam-files` to print only the names of
  the opam files line by line. (ocaml/dune#9793, @reynir and @Alizter)

- `dune exec` now accepts absolute paths inside the workspace.
  (ocaml/dune#12094, @Alizter)

- Add `coqdoc_header` and `coqdoc_footer` fields to the `coq` field of the
  `env` stanza, and to the `coq.theory` stanza, allowing to configure a
  custom header or footer respectively in the HTML output of `coqdoc`.
  (ocaml/dune#11131, @rlepigre)

- Allow `dune fmt` to properly run while a watch mode server is running.
  Note that the `--preview` flag is not supported in this mode.
  (ocaml/dune#12064, @ElectreAAS)

- Support for generating `_CoqProject` files for `coq.theory` stanzas.
  (ocaml/dune#11752, @rlepigre)

- Added `(files)` stanza, similar to `(dirs)` to control which files are visible
  to Dune on a per-directory basis. (ocaml/dune#12879, @nojb)
- Add support for %{ocaml-config:ox} (ocaml/dune#12236, @jonludlam)

- Introduce `dune promotion show` command to display the contents of corrected
  files that are ready for promotion. This allows users to preview changes
  before running `dune promote`. The command accepts file arguments to show
  specific files, or displays all promotable files when called without
  arguments. (ocaml/dune#12669, fixes ocaml/dune#3883, @MixiMaxiMouse)
- New `(lang rocq)` build mode for Rocq 9.0 and later. This new mode
  is very similar to the existing `(lang coq)`, except that it doesn't
  need the `coq*` compatibility wrappers. As of today `(lang rocq)`
  doesn't support yet composed builds with Rocq itself, this will be
  added later.  `(lang coq)` is deprecated, development is frozen, and
  will be removed at some point in the future. (ocaml/dune#12035, @ejgallego,
  @Lysxia, fixes ocaml/dune#11572)

### Changed

- Don't run `ocamldep` to compute false dependencies on the `root_module`
  (ocaml/dune#12227, @rgrinberg)

- `dune format-dune-file` now uses the syntax version of the Dune project that
  contains the file being formatted (if any) instead of using the latest version
  available, which remains the default if there is no Dune project in scope.
  (ocaml/dune#11865, @nojb)

- Persistent DB and process events have been slightly modified. Persistent
  DB events have more concise names and job events always include full
  information. (ocaml/dune#12867, @rgrinberg)

- Removed the `--trace-extended` flag. Its functionality is always enabled when
  tracing is active (ocaml/dune#12908, @rgrinberg)

- The `test/dune` file generated by `dune init proj` now depends on the project library. (ocaml/dune#12791, @shonfeder)

- Starting with version 3.21 of the Dune language, Dune no longer changes the
  default set of compiler warnings. For users that would like to keep the old
  behaviour, the variable `%{dune-warnings}` can be used in an `(env)` stanza in
  a top-level Dune file: `(env (dev (flags :standard %{dune-warnings})))`.
  (ocaml/dune#12766, @nojb)
- Fix: stop generating `cmt` files for cinaps binaries (ocaml/dune#12530, @rgrinberg)
shonfeder added a commit to shonfeder/opam-repository that referenced this pull request Jan 12, 2026
CHANGES:

### Fixed

- Fix `include_subdirs qualified` incorrectly picking the furthest module
  instead of the closest when resolving module name ambiguities. (ocaml/dune#12587,
  @ElectreAAS and @Alizter)

- Fix: include the module alias in the transitive dependency closure with
  `(include_subdirs qualified)`. (ocaml/dune#12299, @anmonteiro)

- Improve error messages for invalid version formats containing non-ASCII
  characters. Previously, non-ASCII characters in version strings (e.g., `(lang
  dune è)` or `(using menhir π3.14)`) would fail with a generic "Invalid file"
  error. Now they display a clear message: "Invalid atom: contains non-ASCII
  character(s). Atoms must only contain ASCII characters." The fix is
  implemented at the lexer level, providing consistent error handling across all
  s-expression parsing. (ocaml/dune#12844, fixes ocaml/dune#12836, @benodiwal)

- Pass private modules with -H when this is available (ocaml/dune#12666, @rgrinberg)

- Allow multiple modules in `(modules_flags ...)`, in `coq.theory` (ocaml/dune#12733, @rlepigre)

- Improve error message for invalid version formats in both `(lang dune ...)` and
  `(using extension ...)` declarations. Changes "Atom of the form NNN.NNN expected"
  to "Invalid version. Version must be two numbers separated by a dot." (ocaml/dune#12833, @benodiwal)

- Fix crash when running `dune build @check` on a library with virtual modules.
  (ocaml/dune#12644, fixes ocaml/dune#12636, @Alizter)

- Provide a more informative error message when `(pkg enabled)` is put in
  `dune-project` instead of `dune-workspace`. (ocaml/dune#12802, fixes ocaml/dune#12801,
  @benodiwal)

- Improve error message when invalid version strings are used in `dune-project`
  files. Non-ASCII characters and malformed versions now show a helpful hint
  with an example of the correct format. (ocaml/dune#12794, fixes ocaml/dune#12751, @benodiwal)

- Stop hiding the `root_module` from the include path (ocaml/dune#12239, @rgrinberg)

- Allow `$ dune init` to work on absolute paths (ocaml/dune#12601, fixes ocaml/dune#7806,
  @rgrinberg)

- `(include_subdirs qualified)`: Add missing alias dependency to module group.
  (ocaml/dune#12530, @anmonteiro)

- Add Melange compilation to the `@all` alias in libraries (ocaml/dune#12628,
  @anmonteiro)

- Fix greedy version location in lang declarations. Previously, error locations for
  invalid lang versions would span multiple bytes for multi-byte UTF-8 characters,
  causing carets to appear misaligned and seemingly include the closing
  parenthesis. Now, error locations for ASCII strings show the full length (e.g.,
  "Ali" shows `^^^`), while non-ASCII strings show only the first byte (e.g., "è"
  shows `^`) to avoid multi-byte character display issues. (ocaml/dune#12869, fixes ocaml/dune#12806,
  @benodiwal)

- melange support: don't emit empty JavaScript modules for generated module
  aliases. (ocaml/dune#12464, @anmonteiro)

### Added

- (Experimental): Introduce the `library_parameter` stanza. It allows users to
  declare a parameter when using the OxCaml compiler.
  (ocaml/dune#11963, implements ocaml/dune#12084, @maiste)

- Added the ability to scroll horizontally in TUI. (ocaml/dune#12386, @Alizter)

- Feature: Include shell command that was executed when a cram test has
  occurred in the error message (ocaml/dune#12307, @rgrinberg)

-  support expanding variables in `(promote (into ..))` (ocaml/dune#12832, fixes ocaml/dune#12742,
   @anmonteiro)

- Add support for `%{cmt:...}` and `%{cmti:...}` variables to reference
  compiled annotation files (.cmt and .cmti) containing typed abstract syntax
  trees with location and type information. (ocaml/dune#12634, grants ocaml/dune#12633, @Alizter)

- Add `$ dune describe tests` to describe the tests in the workspace
  (@Gromototo, ocaml/dune#12545, fixes ocaml/dune#12030)

- Add `argv`, the process environment, and the dune version to the config event
  in the trace (ocaml/dune#12909, @rgrinberg)

- Allow `dune runtest` to properly run while a watch mode server is running.
  (ocaml/dune#12473, grants ocaml/dune#8114, @gridbugs and @ElectreAAS)

- Use copy-on-write (COW) when copying files on filesystems that support it
  (Btrfs, ZFS, XFS, etc), under Linux. (ocaml/dune#12074, fixes ocaml/dune#12071, @nojb)

- Add support for Tangled ATproto-based code repositories (ocaml/dune#12197, @avsm)

- Add support for instantiating OxCaml parameterised libraries.
  (ocaml/dune#12561, @art-w)

- Add a `(conflict_markers error|ignore)` option to the cram stanza. When
  `(conflict_markers error)` is set, the cram test will fail in the presence of
  conflict markers. Git, diff3 and jujutsu conflict markers are detected.
  (ocaml/dune#12538, ocaml/dune#12617, ocaml/dune#12655, fixes ocaml/dune#12512, @rgrinberg, @Alizter)

- Introduce a `%{ppx:lib1+..+libn}` stanza to make it possible to refer to ppx
  executables built by dune. This is useful for writing tests (ocaml/dune#12711,
  @rgrinberg)

- Introduce a `(dir ..)` field on packages defined in the `dune-project`. This
  field allows to associate a directory with a particular package. This makes
  dune automatically filter out all stanzas in this directory and its
  descendants with `--only-packages`. All users are recommended to switch to
  using this field. (ocaml/dune#12614, fixes ocaml/dune#3255, @rgrinberg)

- Add support for `DUNE_ROOT` environment variable, similar to the existing
  `--root` CLI parameter. (fixes ocaml/dune#12399 @sir4ur0n)

- Introduce an `unused-libs` alias to detect unused libraries.
  (ocaml/dune#12623, fixes ocaml/dune#650, @rgrinberg)

- Add `--files` flag to `dune describe opam-files` to print only the names of
  the opam files line by line. (ocaml/dune#9793, @reynir and @Alizter)

- `dune exec` now accepts absolute paths inside the workspace.
  (ocaml/dune#12094, @Alizter)

- Add `coqdoc_header` and `coqdoc_footer` fields to the `coq` field of the
  `env` stanza, and to the `coq.theory` stanza, allowing to configure a
  custom header or footer respectively in the HTML output of `coqdoc`.
  (ocaml/dune#11131, @rlepigre)

- Allow `dune fmt` to properly run while a watch mode server is running.
  Note that the `--preview` flag is not supported in this mode.
  (ocaml/dune#12064, @ElectreAAS)

- Support for generating `_CoqProject` files for `coq.theory` stanzas.
  (ocaml/dune#11752, @rlepigre)

- Added `(files)` stanza, similar to `(dirs)` to control which files are visible
  to Dune on a per-directory basis. (ocaml/dune#12879, @nojb)
- Add support for %{ocaml-config:ox} (ocaml/dune#12236, @jonludlam)

- Introduce `dune promotion show` command to display the contents of corrected
  files that are ready for promotion. This allows users to preview changes
  before running `dune promote`. The command accepts file arguments to show
  specific files, or displays all promotable files when called without
  arguments. (ocaml/dune#12669, fixes ocaml/dune#3883, @MixiMaxiMouse)
- New `(lang rocq)` build mode for Rocq 9.0 and later. This new mode
  is very similar to the existing `(lang coq)`, except that it doesn't
  need the `coq*` compatibility wrappers. As of today `(lang rocq)`
  doesn't support yet composed builds with Rocq itself, this will be
  added later.  `(lang coq)` is deprecated, development is frozen, and
  will be removed at some point in the future. (ocaml/dune#12035, @ejgallego,
  @Lysxia, fixes ocaml/dune#11572)

### Changed

- Don't run `ocamldep` to compute false dependencies on the `root_module`
  (ocaml/dune#12227, @rgrinberg)

- `dune format-dune-file` now uses the syntax version of the Dune project that
  contains the file being formatted (if any) instead of using the latest version
  available, which remains the default if there is no Dune project in scope.
  (ocaml/dune#11865, @nojb)

- Persistent DB and process events have been slightly modified. Persistent
  DB events have more concise names and job events always include full
  information. (ocaml/dune#12867, @rgrinberg)

- Removed the `--trace-extended` flag. Its functionality is always enabled when
  tracing is active (ocaml/dune#12908, @rgrinberg)

- The `test/dune` file generated by `dune init proj` now depends on the project library. (ocaml/dune#12791, @shonfeder)

- Starting with version 3.21 of the Dune language, Dune no longer changes the
  default set of compiler warnings. For users that would like to keep the old
  behaviour, the variable `%{dune-warnings}` can be used in an `(env)` stanza in
  a top-level Dune file: `(env (dev (flags :standard %{dune-warnings})))`.
  (ocaml/dune#12766, @nojb)
- Fix: stop generating `cmt` files for cinaps binaries (ocaml/dune#12530, @rgrinberg)
shonfeder added a commit to shonfeder/opam-repository that referenced this pull request Feb 11, 2026
CHANGES:

### Fixed

- Fix build issues on NetBSD and OpenBSD via update of vendored ocaml-lmdb
  (@Alizter, ocaml/dune#13074)

- Fix `melange.emit` not respecting the package mask via `-p <PKG>` (ocaml/dune#13522,
  @anmonteiro)

### Changed

- Stop starting RPC server with `$ dune promote` (ocaml/dune#13428, @rgrinberg)

  @ElectreAAS and @Alizter)

- Fix: include the module alias in the transitive dependency closure with
  `(include_subdirs qualified)`. (ocaml/dune#12299, @anmonteiro)

- Improve error messages for invalid version formats containing non-ASCII
  characters. Previously, non-ASCII characters in version strings (e.g., `(lang
  dune è)` or `(using menhir π3.14)`) would fail with a generic "Invalid file"
  error. Now they display a clear message: "Invalid atom: contains non-ASCII
  character(s). Atoms must only contain ASCII characters." The fix is
  implemented at the lexer level, providing consistent error handling across all
  s-expression parsing. (ocaml/dune#12844, fixes ocaml/dune#12836, @benodiwal)

- Pass private modules with -H when this is available (ocaml/dune#12666, @rgrinberg)

- Allow multiple modules in `(modules_flags ...)`, in `coq.theory` (ocaml/dune#12733, @rlepigre)

- Improve error message for invalid version formats in both `(lang dune ...)` and
  `(using extension ...)` declarations. Changes "Atom of the form NNN.NNN expected"
  to "Invalid version. Version must be two numbers separated by a dot." (ocaml/dune#12833, @benodiwal)

- Fix crash when running `dune build @check` on a library with virtual modules.
  (ocaml/dune#12644, fixes ocaml/dune#12636, @Alizter)

- Provide a more informative error message when `(pkg enabled)` is put in
  `dune-project` instead of `dune-workspace`. (ocaml/dune#12802, fixes ocaml/dune#12801,
  @benodiwal)

- Improve error message when invalid version strings are used in `dune-project`
  files. Non-ASCII characters and malformed versions now show a helpful hint
  with an example of the correct format. (ocaml/dune#12794, fixes ocaml/dune#12751, @benodiwal)

- Stop hiding the `root_module` from the include path (ocaml/dune#12239, @rgrinberg)

- Allow `$ dune init` to work on absolute paths (ocaml/dune#12601, fixes ocaml/dune#7806,
  @rgrinberg)

- `(include_subdirs qualified)`: Add missing alias dependency to module group.
  (ocaml/dune#12530, @anmonteiro)

- Add Melange compilation to the `@all` alias in libraries (ocaml/dune#12628,
  @anmonteiro)

- Fix greedy version location in lang declarations. Previously, error locations for
  invalid lang versions would span multiple bytes for multi-byte UTF-8 characters,
  causing carets to appear misaligned and seemingly include the closing
  parenthesis. Now, error locations for ASCII strings show the full length (e.g.,
  "Ali" shows `^^^`), while non-ASCII strings show only the first byte (e.g., "è"
  shows `^`) to avoid multi-byte character display issues. (ocaml/dune#12869, fixes ocaml/dune#12806,
  @benodiwal)

- melange support: don't emit empty JavaScript modules for generated module
  aliases. (ocaml/dune#12464, @anmonteiro)

### Added

- (Experimental): Introduce the `library_parameter` stanza. It allows users to
  declare a parameter when using the OxCaml compiler.
  (ocaml/dune#11963, implements ocaml/dune#12084, @maiste)

- Added the ability to scroll horizontally in TUI. (ocaml/dune#12386, @Alizter)

- Feature: Include shell command that was executed when a cram test has
  occurred in the error message (ocaml/dune#12307, @rgrinberg)

-  support expanding variables in `(promote (into ..))` (ocaml/dune#12832, fixes ocaml/dune#12742,
   @anmonteiro)

- Add support for `%{cmt:...}` and `%{cmti:...}` variables to reference
  compiled annotation files (.cmt and .cmti) containing typed abstract syntax
  trees with location and type information. (ocaml/dune#12634, grants ocaml/dune#12633, @Alizter)

- Add `$ dune describe tests` to describe the tests in the workspace
  (@Gromototo, ocaml/dune#12545, fixes ocaml/dune#12030)

- Add `argv`, the process environment, and the dune version to the config event
  in the trace (ocaml/dune#12909, @rgrinberg)

- Allow `dune runtest` to properly run while a watch mode server is running.
  (ocaml/dune#12473, grants ocaml/dune#8114, @gridbugs and @ElectreAAS)

- Use copy-on-write (COW) when copying files on filesystems that support it
  (Btrfs, ZFS, XFS, etc), under Linux. (ocaml/dune#12074, fixes ocaml/dune#12071, @nojb)

- Add support for Tangled ATproto-based code repositories (ocaml/dune#12197, @avsm)

- Add support for instantiating OxCaml parameterised libraries.
  (ocaml/dune#12561, @art-w)

- Add a `(conflict_markers error|ignore)` option to the cram stanza. When
  `(conflict_markers error)` is set, the cram test will fail in the presence of
  conflict markers. Git, diff3 and jujutsu conflict markers are detected.
  (ocaml/dune#12538, ocaml/dune#12617, ocaml/dune#12655, fixes ocaml/dune#12512, @rgrinberg, @Alizter)

- Introduce a `%{ppx:lib1+..+libn}` stanza to make it possible to refer to ppx
  executables built by dune. This is useful for writing tests (ocaml/dune#12711,
  @rgrinberg)

- Introduce a `(dir ..)` field on packages defined in the `dune-project`. This
  field allows to associate a directory with a particular package. This makes
  dune automatically filter out all stanzas in this directory and its
  descendants with `--only-packages`. All users are recommended to switch to
  using this field. (ocaml/dune#12614, fixes ocaml/dune#3255, @rgrinberg)

- Add support for `DUNE_ROOT` environment variable, similar to the existing
  `--root` CLI parameter. (fixes ocaml/dune#12399 @sir4ur0n)

- Introduce an `unused-libs` alias to detect unused libraries.
  (ocaml/dune#12623, fixes ocaml/dune#650, @rgrinberg)

- Add `--files` flag to `dune describe opam-files` to print only the names of
  the opam files line by line. (ocaml/dune#9793, @reynir and @Alizter)

- `dune exec` now accepts absolute paths inside the workspace.
  (ocaml/dune#12094, @Alizter)

- Add `coqdoc_header` and `coqdoc_footer` fields to the `coq` field of the
  `env` stanza, and to the `coq.theory` stanza, allowing to configure a
  custom header or footer respectively in the HTML output of `coqdoc`.
  (ocaml/dune#11131, @rlepigre)

- Allow `dune fmt` to properly run while a watch mode server is running.
  Note that the `--preview` flag is not supported in this mode.
  (ocaml/dune#12064, @ElectreAAS)

- Support for generating `_CoqProject` files for `coq.theory` stanzas.
  (ocaml/dune#11752, @rlepigre)

- Added `(files)` stanza, similar to `(dirs)` to control which files are visible
  to Dune on a per-directory basis. (ocaml/dune#12879, @nojb)
- Add support for %{ocaml-config:ox} (ocaml/dune#12236, @jonludlam)

- Introduce `dune promotion show` command to display the contents of corrected
  files that are ready for promotion. This allows users to preview changes
  before running `dune promote`. The command accepts file arguments to show
  specific files, or displays all promotable files when called without
  arguments. (ocaml/dune#12669, fixes ocaml/dune#3883, @MixiMaxiMouse)
- New `(lang rocq)` build mode for Rocq 9.0 and later. This new mode
  is very similar to the existing `(lang coq)`, except that it doesn't
  need the `coq*` compatibility wrappers. As of today `(lang rocq)`
  doesn't support yet composed builds with Rocq itself, this will be
  added later.  `(lang coq)` is deprecated, development is frozen, and
  will be removed at some point in the future. (ocaml/dune#12035, @ejgallego,
  @Lysxia, fixes ocaml/dune#11572)

### Changed

- Don't run `ocamldep` to compute false dependencies on the `root_module`
  (ocaml/dune#12227, @rgrinberg)

- `dune format-dune-file` now uses the syntax version of the Dune project that
  contains the file being formatted (if any) instead of using the latest version
  available, which remains the default if there is no Dune project in scope.
  (ocaml/dune#11865, @nojb)

- Persistent DB and process events have been slightly modified. Persistent
  DB events have more concise names and job events always include full
  information. (ocaml/dune#12867, @rgrinberg)

- Removed the `--trace-extended` flag. Its functionality is always enabled when
  tracing is active (ocaml/dune#12908, @rgrinberg)

- The `test/dune` file generated by `dune init proj` now depends on the project library. (ocaml/dune#12791, @shonfeder)

- Starting with version 3.21 of the Dune language, Dune no longer changes the
  default set of compiler warnings. For users that would like to keep the old
  behaviour, the variable `%{dune-warnings}` can be used in an `(env)` stanza in
  a top-level Dune file: `(env (dev (flags :standard %{dune-warnings})))`.
  (ocaml/dune#12766, @nojb)
- Fix: stop generating `cmt` files for cinaps binaries (ocaml/dune#12530, @rgrinberg)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants