[rocq] Initial support for the Rocq Prover build language

.github/workflows/workflow.yml

@@ -270,6 +270,36 @@ jobs:
           # We disable the Dune cache when running the tests
           DUNE_CACHE: disabled
 
+  rocq:
+    name: Rocq Language (Rocq 9.1.0)
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        include:
+          # Keep packages and OCaml version in sync with the version
+          # in the makefile; rocq-stdlib should be easy to remove
+          - ocaml-compiler: 5.3
+            opam-packages: rocq-core.9.1.0 rocq-stdlib.9.0.0 csexp re spawn pp uutf
+            test-target: test-rocq
+          - ocaml-compiler: 4.14
+            opam-packages: rocq-core.9.1.0 rocq-stdlib.9.0.0 csexp re spawn pp uutf rocq-native
+            test-target: test-rocq-native
+    steps:
+      - name: Checkout Code
+        uses: actions/checkout@v5
+      - name: Setup OCaml
+        uses: ocaml/setup-ocaml@v3
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-compiler }}
+          dune-cache: true
+      - name: install Rocq Prover
+        run: opam install -y ${{ matrix.opam-packages }}
+      - name: test Rocq Prover Build Language
+        run: opam exec -- make ${{ matrix.test-target }}
+        env:
+          # We disable the Dune cache when running the tests
+          DUNE_CACHE: disabled
+
   wasm:
     name: Wasm_of_ocaml
     needs: nix-build

Makefile

@@ -100,17 +100,26 @@ test-js: $(BIN)
 test-wasm: $(BIN)
 	DUNE_WASM_TEST=enable $(BIN) build @runtest-wasm
 
+.PHONY: test-coq
 test-coq: $(BIN)
 	DUNE_COQ_TEST=enable $(BIN) build @runtest-coq
 
+.PHONY: test-rocq
+test-rocq: $(BIN)
+	DUNE_ROCQ_TEST=enable $(BIN) build @runtest-rocq
+
+.PHONY: test-rocq-native
+test-rocq-native: $(BIN)
+	DUNE_ROCQ_NATIVE_TEST=enable $(BIN) build @runtest-rocq-native
+
 test-melange: $(BIN)
 	$(BIN) build @runtest-melange
 
 test-all: $(BIN)
-	$(BIN) build @runtest @runtest-js @runtest-coq @runtest-melange
+	$(BIN) build @runtest @runtest-js @runtest-coq @runtest-rocq @runtest-melange
 
 test-all-sans-melange: $(BIN)
-	$(BIN) build @runtest @runtest-js @runtest-coq
+	$(BIN) build @runtest @runtest-js @runtest-coq @runtest-rocq
 
 test-ox: $(BIN)
 	$(BIN) runtest test/blackbox-tests/test-cases/oxcaml

bin/main.ml

@@ -30,6 +30,7 @@ let all : _ Cmdliner.Cmd.t list =
   let groups =
     [ Ocaml.Ocaml_cmd.group
     ; Coq.Group.group
+    ; Rocq.group
     ; Describe.group
     ; Describe.Show.group
     ; Rpc.Group.group

bin/printenv.ml

@@ -29,6 +29,9 @@ let dump sctx ~dir =
   and+ coq_dump =
     Dune_rules.Coq.Coq_rules.coq_env ~dir
     >>| Dune_rules.Coq.Coq_flags.dump ~dir:(Path.build dir)
+  and+ rocq_dump =
+    Dune_rules.Rocq.Rocq_rules.rocq_env ~dir
+    >>| Dune_rules.Rocq.Rocq_flags.dump ~dir:(Path.build dir)
   and+ jsoo_js_dump =
     let module Js_of_ocaml = Dune_lang.Js_of_ocaml in
     let* jsoo = Action_builder.of_memo (Dune_rules.Jsoo_rules.jsoo_env ~dir ~mode:JS) in
@@ -45,6 +48,7 @@ let dump sctx ~dir =
       ; link_flags_dump
       ; menhir_dump
       ; coq_dump
+      ; rocq_dump
       ; jsoo_js_dump
       ; jsoo_wasm_dump
       ]

bin/rocq/rocq.ml

@@ -0,0 +1,20 @@
+(***********************************************)
+(* This file is licensed under The MIT License *)
+(* (c) MINES ParisTech 2018-2019               *)
+(* (c) INRIA 2019-2024                         *)
+(* (c) Emilio J. Gallego Arias 2024-2025       *)
+(* (c) CNRS 2025                               *)
+(***********************************************)
+(* Written by: Ali Caglayan                    *)
+(* Written by: Emilio Jesús Gallego Arias      *)
+(* Written by: Rudi Grinberg                   *)
+(* Written by: Rodolphe Lepigre                *)
+(***********************************************)
+
+open Import
+
+let doc = "Command group related to Rocq."
+let sub_commands_synopsis = Common.command_synopsis [ "rocq top FILE -- ARGS" ]
+let man = [ `Blocks sub_commands_synopsis ]
+let info = Cmd.info ~doc ~man "rocq"
+let group = Cmd.group info [ Rocqtop.command ]

bin/rocq/rocq.mli

@@ -0,0 +1,16 @@
+(***********************************************)
+(* This file is licensed under The MIT License *)
+(* (c) MINES ParisTech 2018-2019               *)
+(* (c) INRIA 2019-2024                         *)
+(* (c) Emilio J. Gallego Arias 2024-2025       *)
+(* (c) CNRS 2025                               *)
+(***********************************************)
+(* Written by: Ali Caglayan                    *)
+(* Written by: Emilio Jesús Gallego Arias      *)
+(* Written by: Rudi Grinberg                   *)
+(* Written by: Rodolphe Lepigre                *)
+(***********************************************)
+
+open Import
+
+val group : unit Cmd.t

bin/rocq/rocqtop.ml

@@ -0,0 +1,174 @@
+(***********************************************)
+(* This file is licensed under The MIT License *)
+(* (c) MINES ParisTech 2018-2019               *)
+(* (c) INRIA 2019-2024                         *)
+(* (c) Emilio J. Gallego Arias 2024-2025       *)
+(* (c) CNRS 2025                               *)
+(***********************************************)
+(* Written by: Ali Caglayan                    *)
+(* Written by: Emilio Jesús Gallego Arias      *)
+(* Written by: Rudi Grinberg                   *)
+(* Written by: Rodolphe Lepigre                *)
+(***********************************************)
+
+open Import
+
+let doc = "Execute a Rocq toplevel with the local configuration."
+
+let man =
+  [ `S "DESCRIPTION"
+  ; `P
+      {|$(b,dune rocq top FILE -- ARGS) runs the Rocq toplevel to process the
+          given $(b,FILE). The given arguments are completed according to the
+          local configuration. This is equivalent to running $(b,rocq top ARGS)
+          with a $(b,_RocqProject) file containing the local configurations
+          from the $(b,dune) files, but does not require maintaining a
+          $(b,_RocqProject) file.|}
+  ; `Blocks Common.help_secs
+  ]
+;;
+
+let info = Cmd.info "top" ~doc ~man
+
+let term =
+  let+ default_builder = Common.Builder.term
+  and+ context =
+    let doc = Some "Run the Rocq toplevel in this build context." in
+    Common.context_arg ~doc
+  and+ rocqtop =
+    let doc = Some "Run the given toplevel command instead of the default." in
+    Arg.(value & opt string "rocq" & info [ "toplevel" ] ~docv:"CMD" ~doc)
+  and+ rocq_file_arg =
+    Arg.(required & pos 0 (some string) None (Arg.info [] ~doc:None ~docv:"ROCQFILE"))
+  and+ extra_args =
+    Arg.(value & pos_right 0 string [] (Arg.info [] ~doc:None ~docv:"ARGS"))
+  and+ no_rebuild =
+    Arg.(
+      value
+      & flag
+      & info [ "no-build" ] ~doc:(Some "Don't rebuild dependencies before executing."))
+  in
+  let common, config =
+    let builder =
+      if no_rebuild then Common.Builder.forbid_builds default_builder else default_builder
+    in
+    Common.init builder
+  in
+  let rocq_file_arg = Common.prefix_target common rocq_file_arg |> Path.Local.of_string in
+  let rocqtop, args, env =
+    Scheduler.go_with_rpc_server ~common ~config
+    @@ fun () ->
+    let open Fiber.O in
+    let* setup = Import.Main.setup () in
+    let* setup = Memo.run setup in
+    let sctx = Import.Main.find_scontext_exn setup ~name:context in
+    let context = Dune_rules.Super_context.context sctx in
+    let rocq_file_build =
+      Path.Build.append_local (Context.build_dir context) rocq_file_arg
+    in
+    let dir =
+      (match Path.Local.parent rocq_file_arg with
+       | None -> Path.Local.root
+       | Some dir -> dir)
+      |> Path.Build.append_local (Context.build_dir context)
+    in
+    let* rocqtop, rocq_arg, args, env =
+      build_exn
+      @@ fun () ->
+      let open Memo.O in
+      let* (tr : Dune_rules.Dir_contents.triage) =
+        Dune_rules.Dir_contents.triage sctx ~dir
+      in
+      let dir =
+        match tr with
+        | Group_part dir -> dir
+        | Standalone_or_root _ -> dir
+      in
+      let* dc = Dune_rules.Dir_contents.get sctx ~dir in
+      let* rocq_src = Dune_rules.Dir_contents.rocq dc in
+      let rocq_module =
+        let source = rocq_file_build in
+        match Dune_rules.Rocq.Rocq_sources.find_module ~source rocq_src with
+        | Some m -> snd m
+        | None ->
+          let hints =
+            [ Pp.textf "Is the file part of a stanza?"
+            ; Pp.textf "Has the file been written to disk?"
+            ]
+          in
+          User_error.raise
+            ~hints
+            [ Pp.textf "Cannot find file: %s" (rocq_file_arg |> Path.Local.to_string) ]
+      in
+      let stanza = Dune_rules.Rocq.Rocq_sources.lookup_module rocq_src rocq_module in
+      let args, use_stdlib, wrapper_name, mode =
+        match stanza with
+        | None ->
+          User_error.raise
+            [ Pp.textf
+                "File not part of any stanza: %s"
+                (rocq_file_arg |> Path.Local.to_string)
+            ]
+        | Some (`Theory theory) ->
+          ( Dune_rules.Rocq.Rocq_rules.rocqtop_args_theory
+              ~sctx
+              ~dir
+              ~dir_contents:dc
+              theory
+              rocq_module
+          , theory.buildable.use_stdlib
+          , Dune_rules.Rocq.Rocq_lib_name.wrapper (snd theory.name)
+          , theory.buildable.mode )
+        | Some (`Extraction extr) ->
+          ( Dune_rules.Rocq.Rocq_rules.rocqtop_args_extraction ~sctx ~dir extr rocq_module
+          , extr.buildable.use_stdlib
+          , "DuneExtraction"
+          , extr.buildable.mode )
+      in
+      (* Run rocqdep *)
+      let* (_ : unit * Dep.Fact.t Dep.Map.t) =
+        let deps_of =
+          if no_rebuild
+          then Action_builder.return ()
+          else (
+            let mode =
+              match mode with
+              | None -> Dune_rules.Rocq.Rocq_mode.VoOnly
+              | Some mode -> mode
+            in
+            Dune_rules.Rocq.Rocq_rules.deps_of
+              ~dir
+              ~use_stdlib
+              ~wrapper_name
+              ~mode
+              rocq_module)
+        in
+        Action_builder.evaluate_and_collect_facts deps_of
+      in
+      let real_binary, rocq_arg =
+        if String.equal "rocq" rocqtop then "rocq", [ "top" ] else rocqtop, []
+      in
+      let* prog = Super_context.resolve_program_memo sctx ~dir ~loc:None real_binary in
+      let prog = Action.Prog.ok_exn prog in
+      let* () = Build_system.build_file prog in
+      (* Get args *)
+      let* (args, _) : string list * Dep.Fact.t Dep.Map.t =
+        let* args = args in
+        let dir = Path.external_ Path.External.initial_cwd in
+        let args = Dune_rules.Command.expand ~dir (S args) in
+        Action_builder.evaluate_and_collect_facts args.build
+      in
+      let+ env = Super_context.context_env sctx in
+      Path.to_string prog, rocq_arg, args, env
+    in
+    (* Careful about the first argument to "rocq" *)
+    let args =
+      let topfile = Path.to_absolute_filename (Path.build rocq_file_build) in
+      rocq_arg @ ("-topfile" :: topfile :: args) @ extra_args
+    in
+    Fiber.return (rocqtop, args, env)
+  in
+  restore_cwd_and_execve (Common.root common) rocqtop args env
+;;
+
+let command = Cmd.v info term

bin/rocq/rocqtop.mli

@@ -0,0 +1,16 @@
+(***********************************************)
+(* This file is licensed under The MIT License *)
+(* (c) MINES ParisTech 2018-2019               *)
+(* (c) INRIA 2019-2024                         *)
+(* (c) Emilio J. Gallego Arias 2024-2025       *)
+(* (c) CNRS 2025                               *)
+(***********************************************)
+(* Written by: Ali Caglayan                    *)
+(* Written by: Emilio Jesús Gallego Arias      *)
+(* Written by: Rudi Grinberg                   *)
+(* Written by: Rodolphe Lepigre                *)
+(***********************************************)
+
+open Import
+
+val command : unit Cmd.t

doc/changes/added/12035.md

@@ -0,0 +1,7 @@
+- 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. (#12035, @ejgallego,
+  @lysxia, fixes #11572)

doc/concepts/variables.rst

@@ -75,7 +75,8 @@ Dune supports the following variables:
   variable ``<var>``, or ``<default>`` if it does not exist.
   For example, ``%{env:BIN=/usr/bin}``.
   Available since Dune 1.4.0.
-- There are some Coq-specific variables detailed in :ref:`coq-variables`.
+- There are some Rocq-specific and Coq-specific variables detailed in
+  :ref:`rocq-variables` and :ref:`coq-variables`.
 
 In addition, ``(action ...)`` fields support the following special variables: