Generate "_CoqProject" files for Coq theories

doc/changes/added/11752.md

@@ -0,0 +1,2 @@
+- Support for generating `_CoqProject` files for `coq.theory` stanzas.
+  (#11752, @rlepigre)

doc/coq.rst

@@ -67,6 +67,7 @@ The Coq theory stanza is very similar in form to the OCaml
      (plugins <ocaml_plugins>)
      (flags <coq_flags>)
      (modules_flags <flags_map>)
+     (generate_project_file)
      (coqdep_flags <coqdep_flags>)
      (coqdoc_flags <coqdoc_flags>)
      (coqdoc_header <coqdoc_header>)
@@ -190,8 +191,16 @@ The semantics of the fields are:
 - If the ``(mode vos)`` field is present, only Coq compiled interface files
   ``.vos`` will be produced for the theory. This is mainly useful in conjunction
   with ``dune coq top``, since this makes the compilation of dependencies much
-  faster, at the cost of skipping proof checking. (Appeared in :ref:`Coq lang
-  0.8<coq-lang>`).
+  faster, at the cost of skipping proof checking.
+  (Appeared in :ref:`Coq lang 0.8<coq-lang>`)
+
+- If the ``(generate_project_file)`` is present, a ``_CoqProject`` file is
+  generated in the Coq theory's directory (it is promoted to the source tree).
+  This file should be suitable for editor compatibility, and it provides an
+  alternative to using ``dune coq top``. It is however limited in two ways: it
+  is incompatible with the ``(modules_flags ...)`` field, and it cannot be
+  used for two Coq theories declared in the same directory.
+  (Appeared in :ref:`Coq lang 0.11<coq-lang>`)
 
 Coq Dependencies
 ~~~~~~~~~~~~~~~~
@@ -369,9 +378,9 @@ The Coq lang can be modified by adding the following to a
 The supported Coq language versions (not the version of Coq) are:
 
 - ``0.11``: Support for the ``(coqdoc_header ...)`` and ``(coqdoc_footer ...)``
-  fields.
+  fields, and for ``_CoqProject`` file generation.
 - ``0.10``: Support for the ``(coqdep_flags ...)`` field.
-- ``0.9``: Support for per-module flags with the ``(module_flags ...)``` field.
+- ``0.9``: Support for per-module flags with the ``(modules_flags ...)``` field.
 - ``0.8``: Support for composition with installed Coq theories;
   support for ``vos`` builds.
 

src/dune_rules/coq/coq_rules.ml

@@ -520,6 +520,131 @@ let dep_theory_file ~dir ~wrapper_name =
   |> Path.Build.set_extension ~ext:".theory.d"
 ;;
 
+let theory_coq_args
+      ~sctx
+      ~dir
+      ~wrapper_name
+      ~boot_flags
+      ~stanza_flags
+      ~ml_flags
+      ~theories_deps
+      ~theory_dirs
+  =
+  let+ coq_stanza_flags =
+    let+ expander = Super_context.expander sctx ~dir in
+    let coq_flags =
+      let coq_flags = coq_flags ~expander ~dir ~stanza_flags ~per_file_flags:None in
+      (* By default we have the -q flag. We don't want to pass this to coqtop to
+         allow users to load their .coqrc files for interactive development.
+         Therefore we manually scrub the -q setting when passing arguments to
+         coqtop. *)
+      let rec remove_q = function
+        | "-q" :: l -> remove_q l
+        | x :: l -> x :: remove_q l
+        | [] -> []
+      in
+      let open Action_builder.O in
+      coq_flags >>| remove_q
+    in
+    Command.Args.dyn coq_flags (* stanza flags *)
+  in
+  let coq_native_flags =
+    let mode = Coq_mode.VoOnly in
+    coqc_native_flags ~sctx ~dir ~theories_deps ~theory_dirs ~mode
+  in
+  let file_flags = coqc_file_flags ~dir ~theories_deps ~wrapper_name ~ml_flags in
+  [ coq_stanza_flags; coq_native_flags; Dyn boot_flags; S file_flags ]
+;;
+
+let setup_coqproject_for_theory_rule
+      ~scope
+      ~sctx
+      ~dir
+      ~loc
+      ~theories_deps
+      ~wrapper_name
+      ~use_stdlib
+      ~ml_flags
+      ~coq_lang_version
+      ~stanza_flags
+      ~theory_dirs
+      coq_modules
+  =
+  (* Process coqdep and generate rules *)
+  let boot_type =
+    match coq_modules with
+    | [] -> Resolve.Memo.return Bootstrap.empty
+    | m :: _ -> Bootstrap.make ~scope ~use_stdlib ~wrapper_name ~coq_lang_version m
+  in
+  let boot_flags = Resolve.Memo.read boot_type |> Action_builder.map ~f:Bootstrap.flags in
+  let* args =
+    theory_coq_args
+      ~sctx
+      ~dir
+      ~wrapper_name
+      ~boot_flags
+      ~stanza_flags
+      ~ml_flags
+      ~theories_deps
+      ~theory_dirs
+  in
+  let contents : string With_targets.t =
+    let open With_targets.O in
+    let dir = Path.build dir in
+    let+ args_bld = Command.expand ~dir (Command.Args.S args)
+    and+ args_src =
+      let dir = Path.source (Path.drop_build_context_exn dir) in
+      Command.expand ~dir (Command.Args.S args)
+    in
+    let contents = Buffer.create 73 in
+    let rec add_args args_bld args_src =
+      match args_bld, args_src with
+      | (("-R" | "-Q") as o) :: db :: mb :: args_bld, _ :: ds :: ms :: args_src ->
+        Buffer.add_string contents o;
+        Buffer.add_char contents ' ';
+        Buffer.add_string contents db;
+        Buffer.add_char contents ' ';
+        Buffer.add_string contents mb;
+        Buffer.add_char contents '\n';
+        if db <> ds
+        then (
+          Buffer.add_string contents o;
+          Buffer.add_char contents ' ';
+          Buffer.add_string contents ds;
+          Buffer.add_char contents ' ';
+          Buffer.add_string contents ms;
+          Buffer.add_char contents '\n');
+        add_args args_bld args_src
+      | "-I" :: _ :: args_bld, "-I" :: d :: args_src ->
+        Buffer.add_string contents "-I ";
+        Buffer.add_string contents d;
+        Buffer.add_char contents '\n';
+        add_args args_bld args_src
+      | o :: args_bld, _ :: args_src ->
+        Buffer.add_string contents "-arg ";
+        Buffer.add_string contents o;
+        Buffer.add_char contents '\n';
+        add_args args_bld args_src
+      | [], [] -> ()
+      | _, _ -> assert false
+    in
+    add_args args_bld args_src;
+    Buffer.contents contents
+  in
+  let mode =
+    let open Rule.Promote in
+    let lifetime = Lifetime.Until_clean in
+    Rule.Mode.Promote { lifetime; into = None; only = None }
+  in
+  let coqproject = Path.Build.relative dir "_CoqProject" in
+  Super_context.add_rule
+    ~mode
+    ~loc
+    sctx
+    ~dir
+    (Action_builder.write_file_dyn coqproject contents.build)
+;;
+
 let setup_coqdep_for_theory_rule
       ~sctx
       ~dir
@@ -1050,18 +1175,34 @@ let setup_theory_rules ~sctx ~dir ~dir_contents (s : Coq_stanza.Theory.t) =
     | m :: _ -> Bootstrap.make ~scope ~use_stdlib ~wrapper_name ~coq_lang_version m
   in
   let boot_flags = Resolve.Memo.read boot_type |> Action_builder.map ~f:Bootstrap.flags in
-  setup_coqdep_for_theory_rule
-    ~sctx
-    ~dir
-    ~loc
-    ~theories_deps
-    ~wrapper_name
-    ~source_rule
-    ~ml_flags
-    ~mlpack_rule
-    ~boot_flags
-    ~stanza_coqdep_flags:s.coqdep_flags
-    coq_modules
+  (if not (snd s.generate_project_file)
+   then Memo.return ()
+   else
+     setup_coqproject_for_theory_rule
+       ~scope
+       ~sctx
+       ~dir
+       ~loc
+       ~theories_deps
+       ~wrapper_name
+       ~use_stdlib
+       ~ml_flags
+       ~coq_lang_version
+       ~stanza_flags
+       ~theory_dirs
+       coq_modules)
+  >>> setup_coqdep_for_theory_rule
+        ~sctx
+        ~dir
+        ~loc
+        ~theories_deps
+        ~wrapper_name
+        ~source_rule
+        ~ml_flags
+        ~mlpack_rule
+        ~boot_flags
+        ~stanza_coqdep_flags:s.coqdep_flags
+        coq_modules
   >>> Memo.parallel_iter
         coq_modules
         ~f:

src/dune_rules/coq/coq_stanza.ml

@@ -169,6 +169,7 @@ module Theory = struct
     ; modules : Ordered_set_lang.t
     ; modules_flags : (Coq_module.Name.t * Ordered_set_lang.Unexpanded.t) list option
     ; boot : bool
+    ; generate_project_file : Loc.t * bool
     ; enabled_if : Blang.t
     ; buildable : Buildable.t
     ; coqdep_flags : Ordered_set_lang.Unexpanded.t
@@ -230,6 +231,18 @@ module Theory = struct
       | (loc, _) :: _ -> boot_has_deps loc)
   ;;
 
+  let check_generate_project_file (loc, generate_project_file) modules_flags =
+    if generate_project_file
+    then (
+      match modules_flags with
+      | None -> ()
+      | Some _ ->
+        User_error.raise
+          ~loc
+          [ Pp.textf "(generate_project_file) is not compatible with (modules_flags ...)"
+          ])
+  ;;
+
   module Per_file = struct
     let decode_pair =
       let+ mod_ = Coq_module.Name.decode
@@ -248,6 +261,11 @@ module Theory = struct
        and+ public = coq_public_decode
        and+ synopsis = field_o "synopsis" string
        and+ boot = field_b "boot" ~check:(Dune_lang.Syntax.since coq_syntax (0, 2))
+       and+ generate_project_file =
+         located
+         @@ field_b
+              "generate_project_file"
+              ~check:(Dune_lang.Syntax.since coq_syntax (0, 11))
        and+ modules = Ordered_set_lang.field "modules"
        and+ modules_flags =
          field_o
@@ -274,6 +292,8 @@ module Theory = struct
        in
        (* boot libraries cannot depend on other theories *)
        check_boot_has_no_deps boot buildable;
+       (* project files can only be generated when no per-module flags are configured. *)
+       check_generate_project_file generate_project_file modules_flags;
        let package = merge_package_public ~package ~public in
        { name
        ; package
@@ -282,6 +302,7 @@ module Theory = struct
        ; modules
        ; modules_flags
        ; boot
+       ; generate_project_file
        ; buildable
        ; enabled_if
        ; coqdep_flags

src/dune_rules/coq/coq_stanza.mli

@@ -33,6 +33,7 @@ module Theory : sig
     ; modules : Ordered_set_lang.t
     ; modules_flags : (Coq_module.Name.t * Ordered_set_lang.Unexpanded.t) list option
     ; boot : bool
+    ; generate_project_file : Loc.t * bool
     ; enabled_if : Blang.t
     ; buildable : Buildable.t
     ; coqdep_flags : Ordered_set_lang.Unexpanded.t

test/blackbox-tests/test-cases/coq/coqproject-multiple-theories.t

@@ -0,0 +1,26 @@
+Testing the _CoqProject generation.
+
+  $ cat > dune-project <<EOF
+  > (lang dune 3.21)
+  > (using coq 0.11)
+  > EOF
+
+  $ cat > dune <<EOF
+  > (coq.theory
+  >  (name a)
+  >  (modules foo)
+  >  (generate_project_file))
+  > 
+  > (coq.theory
+  >  (name b)
+  >  (modules bar)
+  >  (generate_project_file))
+  > EOF
+
+  $ touch foo.v bar.v
+
+  $ dune build
+  Error: Multiple rules generated for _build/default/_CoqProject:
+  - dune:6
+  - dune:1
+  [1]

test/blackbox-tests/test-cases/coq/coqproject-per-module-flags.t

@@ -0,0 +1,22 @@
+Testing the _CoqProject generation.
+
+  $ cat > dune-project <<EOF
+  > (lang dune 3.21)
+  > (using coq 0.11)
+  > EOF
+
+  $ cat > dune <<EOF
+  > (coq.theory
+  >  (name a)
+  >  (modules_flags (foo (:standard -flag)))
+  >  (generate_project_file))
+  > EOF
+
+  $ touch foo.v
+
+  $ dune build
+  File "dune", line 4, characters 1-24:
+  4 |  (generate_project_file))
+       ^^^^^^^^^^^^^^^^^^^^^^^
+  Error: (generate_project_file) is not compatible with (modules_flags ...)
+  [1]

test/blackbox-tests/test-cases/coq/coqproject.t

@@ -0,0 +1,17 @@
+Testing the _CoqProject generation.
+
+  $ cat > dune-project <<EOF
+  > (lang dune 3.21)
+  > (using coq 0.11)
+  > EOF
+
+  $ cat > dune <<EOF
+  > (coq.theory
+  >  (name a)
+  >  (generate_project_file))
+  > EOF
+
+  $ touch foo.v
+
+  $ dune build
+  $ [ -f _CoqProject ]