Skip to content

Conversation

@ejgallego
Copy link
Collaborator

@ejgallego ejgallego commented Jul 16, 2025

We introduce (lang rocq), a build mode for the Rocq Prover, previously known as "Coq".

The build mode is an exact copy of the (lang coq) mode, renaming the modules, data, and some global declarations. Also, the default implicit lib is now named Corelib.

(lang coq) should be considered deprecated / frozen, and eventually removed.

There are many cleanups and improvements possible, in particular we have done, in separate commits:

  • removed support for older legacy coq modes
  • removed support for legacy plugin handling
  • removed the need for coq-* shims

All of the tests have been ported and manually verified to work (a time consuming process) As of today, all test pass.

Future work:

  • support new extraction option (-output-directory)
  • improve composition with local rocq as in (lang coq), as of today the rocqworker is not injected as a dependency
  • nix CI + develop
  • forward port _RocqProject generation
  • forward port rocqdoc headers work
  • forward port per_module fixes
  • cosmetic, turn rocq into rocq compile for --display=short
  • [CI] Remove dependency on rocq-stdlib, only extraction tests need that

Closes #11572
Cc #12788 #6445 #9348 #12734

Joint work with Li-yao Xia.

@rlepigre-skylabs-ai
Copy link

I just learned that you are working on this @ejgallego, that's great news!

There are several points that are IMO worth discussing before merging this PR:

Also, I'm happy to play a part in this if you want help.

@rlepigre-skylabs-ai
Copy link

Another candidate is going back to calling rocq dep on all files, instead of per-theory.

@ejgallego
Copy link
Collaborator Author

Hey @rlepigre-skylabs-ai !

I just learned that you are working on this @ejgallego, that's great news!

Indeed! Thanks a lot for your message. We got side-tracked by other stuff, but the idea is to merge this and #11945

There are several points that are IMO worth discussing before merging this PR:

Yes, we will forward port this in a separate PR.

  • To more easily support the above, should we remove per-module flags? (IMO they are kind of useless.)

IMHO we can just say that both can't work together, there are some folks trying to use this feature, so I'd like to keep it.

  • Similarly, should we enforce at most one theory stanza per directory? (I personally always do that, can't imagine this breaking too much stuff.)

This would certainly break a lot of stuff tho, what would we gain?

  • Should we sort out the .vos / .vok mess?

Happy to work on this but IMHO we can do in a separate PR.

Yes, we will also forward port this.

Also, I'm happy to play a part in this if you want help.

Absolutely, @Lysxia and I will send a mail soon to coordiante.

Another candidate is going back to calling rocq dep on all files, instead of per-theory.

This should be easy to do if we want, tho for some users it would mean a large performance regression. But IMHO unrelated to this PR which is to enable Rocq users no to have to depend on the coq-* compatibility wrappers.

@rlepigre-skylabs-ai
Copy link

This should be easy to do if we want, tho for some users it would mean a large performance regression. But IMHO unrelated to this PR which is to enable Rocq users no to have to depend on the coq-* compatibility wrappers.

I think this was originally due to performance issues in coqdep that have now kind of been fixed, but I could be wrong. For us, at this point, this would be a performance improvement I believe.

@ejgallego
Copy link
Collaborator Author

I think this was originally due to performance issues in coqdep that have now kind of been fixed, but I could be wrong.

Do you have pointer? The original performance problem is that in one rocqdep call per file, rocqdep will still scan the whole user-contrib tree. This has a huge impact in practice, even in fast systems like Linux.

For us, at this point, this would be a performance improvement I believe.

I'd be happy to make this configurable, the original Coq mode used this system so it is easy just to look at the commit and add back that code with a flag.

Once we have that we could test for numbers, but my original experiments showed a large overhead of repeated rocqdep calls.

@ejgallego ejgallego force-pushed the rocq_lang branch 4 times, most recently from e176b80 to 934466c Compare November 25, 2025 19:04
ejgallego and others added 12 commits November 25, 2025 20:19
We introduce `(lang rocq)`, a build mode for the Rocq Prover,
previously known as "Coq".

The build mode is an exact copy of the `(lang coq)` mode, renaming the
modules, data, and some global declarations. Also, the default
implicit lib is now named `Corelib`.

(lang coq): should be considered deprecated / frozen, and eventually
removed.

There are many cleanups and improvements possible, these will be done
in later commits.

All of the tests have been ported and manually verified to work (a
time consuming process) As of today, all test pass.

The test suite has been tested against Rocq 9.1, with the `coq`
compatibility package added.

Co-authored-by: Li-yao Xia <[email protected]>
Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
For now a copy of Coq's one, with minor updates.

Co-authored-by: Li-yao Xia <[email protected]>
Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
Co-authored-by: Rodolphe Lepigre <[email protected]>
Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
…aml#12733"

Co-authored-by: Rodolphe Lepigre <[email protected]>
Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
…caml#11752

Co-authored-by: Rodolphe Lepigre <[email protected]>
Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
Co-authored-by: Li-yao Xia <[email protected]>
Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
Not needed anymore as Rocq dropped support for non-findlib loading.

Co-authored-by: Li-yao Xia <[email protected]>
Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
This is smaller than expected, we still need to pass the native
options and warnings due to upstream.

Co-authored-by: Li-yao Xia <[email protected]>
Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
Beware both `rocq c --config` and `coqc --config` still output `COQ*`
variable names.

Co-authored-by: Li-yao Xia <[email protected]>
Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
Co-authored-by: Li-yao Xia <[email protected]>
Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
We remove the need for installing coqc shims, and adapt the test suite
accordingly.

There is one mayor caveat and one minor caveat:

- the major caveat is that in builds composed with Rocq, dune will
  only search for `rocq`, but we don't inject a dependency on
  `rocqworker` which is also needed, but a private binary. This means
  that users should ensure manually `rocqworker` is built when using
  composed builds. We hope to fix this soon, in a different PR.

- the minor caveat is that with `--display=short` we just now display
  the `rocq` name, not `rocq compile` or `rocq dep`. This can be also
  fixed in a different PR.

Co-authored-by: Li-yao Xia <[email protected]>
Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
Co-authored-by: Li-yao Xia <[email protected]>
Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
@Alizter
Copy link
Collaborator

Alizter commented Nov 25, 2025

@gridbugs Do you know why the CI is failing here? The test that is affected is portable-lockdirs-platform-dependant-dependencies.t. AFAICT the changes in this PR are seemingly unrelated.

Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
@ejgallego ejgallego enabled auto-merge November 25, 2025 20:43
@ejgallego ejgallego merged commit d1a4553 into ocaml:main Nov 25, 2025
28 checks passed
@ejgallego ejgallego deleted the rocq_lang branch November 25, 2025 21:24
$ ls $pkg_root/
foo.0.0.1-9b0ae1f26c9a79e6ae8bca96ec389858
linux-only.0.0.1-f1f7456a7bf1c70f9203f8caadf79f6d
foo.0.0.1-5e48eb7073ada94c09fb13ac3853f1e9
Copy link
Collaborator

Choose a reason for hiding this comment

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

The fact that this had to change is worrying.

Copy link
Collaborator

Choose a reason for hiding this comment

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

It's because we use Digest_feed.generic to hash actions which contain pforms, and this change introduces a new pform constructor before the Pkg_self constructor, which is one of the pforms appearing in the build commands of the packages whose hashes are changing here. Digest_feed.generic computes a hash based on the representation of values, and variant constructors have a tag in their representation based on their position within the variant type definition. All the constructors below the new Rocq_config constructor have had their tag increased by 1.

To confirm this, apply the following patch which will cause the hashes in this test to revert to their original values:

diff --git i/src/dune_lang/pform.ml w/src/dune_lang/pform.ml
index e836d64c8..9b4601cc6 100644
--- i/src/dune_lang/pform.ml
+++ w/src/dune_lang/pform.ml
@@ -296,12 +296,12 @@ module Macro = struct
     | Path_no_dep
     | Ocaml_config
     | Coq_config
-    | Rocq_config
     | Env
     | Artifact of Artifact.t
     | Pkg
     | Pkg_self
     | Ppx
+    | Rocq_config
 
   let compare x y =
     match x, y with
diff --git i/src/dune_lang/pform.mli w/src/dune_lang/pform.mli
index ae2eba7c3..4feb23cf2 100644
--- i/src/dune_lang/pform.mli
+++ w/src/dune_lang/pform.mli
@@ -137,12 +137,12 @@ module Macro : sig
     | Path_no_dep
     | Ocaml_config
     | Coq_config
-    | Rocq_config
     | Env
     | Artifact of Artifact.t
     | Pkg
     | Pkg_self
     | Ppx
+    | Rocq_config
 
   val compare : t -> t -> Ordering.t
   val to_dyn : t -> Dyn.t

The consequence of this for users is that they'll have to rebuild many of the dependencies of projects upon updating Dune. I don't think that's a big deal since updating Dune is quite rare and I don't think that behaviour is too surprising. If we really wanted to prevent this sort of thing we'd have to stop using Dune_feed.generic and take care to manually implement hash functions in a way that isn't sensitive to these sorts of changes. Personally I don't think it's worth it.

| Coq_config, Coq_config -> Eq
| Coq_config, _ -> Lt
| _, Coq_config -> Gt
| Rocq_config, _ -> Lt
Copy link
Member

Choose a reason for hiding this comment

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

Rocq_config, Rocq_config -> Eq

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Thanks, will fix.

@Ef55 Ef55 mentioned this pull request Nov 26, 2025
4 tasks
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)
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.

Rocq support in dune

6 participants