diff --git a/doc/changes/added/11752.md b/doc/changes/added/11752.md new file mode 100644 index 00000000000..448ef294b6e --- /dev/null +++ b/doc/changes/added/11752.md @@ -0,0 +1,2 @@ +- Support for generating `_CoqProject` files for `coq.theory` stanzas. + (#11752, @rlepigre) diff --git a/doc/coq.rst b/doc/coq.rst index faf8ddc80ef..f89a70e1931 100644 --- a/doc/coq.rst +++ b/doc/coq.rst @@ -67,6 +67,7 @@ The Coq theory stanza is very similar in form to the OCaml (plugins ) (flags ) (modules_flags ) + (generate_project_file) (coqdep_flags ) (coqdoc_flags ) (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`). + faster, at the cost of skipping proof checking. + (Appeared in :ref:`Coq lang 0.8`) + +- 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 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. diff --git a/src/dune_rules/coq/coq_rules.ml b/src/dune_rules/coq/coq_rules.ml index 9d5109fd72a..e4080e9f258 100644 --- a/src/dune_rules/coq/coq_rules.ml +++ b/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: diff --git a/src/dune_rules/coq/coq_stanza.ml b/src/dune_rules/coq/coq_stanza.ml index 5a1097507d1..32154a3437f 100644 --- a/src/dune_rules/coq/coq_stanza.ml +++ b/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 diff --git a/src/dune_rules/coq/coq_stanza.mli b/src/dune_rules/coq/coq_stanza.mli index eb211babb4a..c523d10e4d0 100644 --- a/src/dune_rules/coq/coq_stanza.mli +++ b/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 diff --git a/test/blackbox-tests/test-cases/coq/coqproject-multiple-theories.t b/test/blackbox-tests/test-cases/coq/coqproject-multiple-theories.t new file mode 100644 index 00000000000..34360e51e71 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/coqproject-multiple-theories.t @@ -0,0 +1,26 @@ +Testing the _CoqProject generation. + + $ cat > dune-project < (lang dune 3.21) + > (using coq 0.11) + > EOF + + $ cat > dune < (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] diff --git a/test/blackbox-tests/test-cases/coq/coqproject-per-module-flags.t b/test/blackbox-tests/test-cases/coq/coqproject-per-module-flags.t new file mode 100644 index 00000000000..3b61b2d93dd --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/coqproject-per-module-flags.t @@ -0,0 +1,22 @@ +Testing the _CoqProject generation. + + $ cat > dune-project < (lang dune 3.21) + > (using coq 0.11) + > EOF + + $ cat > dune < (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] diff --git a/test/blackbox-tests/test-cases/coq/coqproject.t b/test/blackbox-tests/test-cases/coq/coqproject.t new file mode 100644 index 00000000000..0327071d2b6 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/coqproject.t @@ -0,0 +1,17 @@ +Testing the _CoqProject generation. + + $ cat > dune-project < (lang dune 3.21) + > (using coq 0.11) + > EOF + + $ cat > dune < (coq.theory + > (name a) + > (generate_project_file)) + > EOF + + $ touch foo.v + + $ dune build + $ [ -f _CoqProject ]