From ad088a5da41f415ceb96a53c09531d0440db12f7 Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Thu, 23 Mar 2023 08:42:05 +0100 Subject: [PATCH] [coq] support for vos builds. This is configured using a new [vos] mode, that can be configured in the [coq.theory] stanza. Signed-off-by: Rodolphe Lepigre --- CHANGES.md | 5 ++ bin/coq/coqtop.ml | 15 ++++-- doc/coq.rst | 6 +++ src/dune_rules/coq/coq_mode.ml | 2 + src/dune_rules/coq/coq_mode.mli | 1 + src/dune_rules/coq/coq_module.ml | 4 +- src/dune_rules/coq/coq_rules.ml | 33 +++++++++--- src/dune_rules/coq/coq_rules.mli | 1 + src/dune_rules/dune_rules.ml | 1 + .../test-cases/coq/vos-build.t/bar.v | 3 ++ .../test-cases/coq/vos-build.t/base.opam | 0 .../test-cases/coq/vos-build.t/dune | 10 ++++ .../test-cases/coq/vos-build.t/dune-project | 2 + .../test-cases/coq/vos-build.t/dune-vo | 10 ++++ .../test-cases/coq/vos-build.t/foo.v | 1 + .../test-cases/coq/vos-build.t/run.t | 51 +++++++++++++++++++ 16 files changed, 134 insertions(+), 11 deletions(-) create mode 100644 test/blackbox-tests/test-cases/coq/vos-build.t/bar.v create mode 100644 test/blackbox-tests/test-cases/coq/vos-build.t/base.opam create mode 100644 test/blackbox-tests/test-cases/coq/vos-build.t/dune create mode 100644 test/blackbox-tests/test-cases/coq/vos-build.t/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/vos-build.t/dune-vo create mode 100644 test/blackbox-tests/test-cases/coq/vos-build.t/foo.v create mode 100644 test/blackbox-tests/test-cases/coq/vos-build.t/run.t diff --git a/CHANGES.md b/CHANGES.md index 1d4e1a7b676..9af1caf41ee 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,11 @@ Unreleased ---------- +- Preliminary support for Coq compiled intefaces (`.vos` files) enabled via + `(mode vos)` in `coq.theory` stanzas. This can be used in combination with + `dune coq top` to obtain fast re-building of dependencies (with no checking + of proofs) prior to stepping into a file. (#7406, @rlepigre) + - Fix `dune install` when cross compiling (#7410, fixes #6191, @anmonteiro, @rizo) diff --git a/bin/coq/coqtop.ml b/bin/coq/coqtop.ml index 525f9c5e875..56abe2d0306 100644 --- a/bin/coq/coqtop.ml +++ b/bin/coq/coqtop.ml @@ -81,7 +81,7 @@ let term = let stanza = Dune_rules.Coq_sources.lookup_module coq_src coq_module in - let args, use_stdlib, coq_lang_version, wrapper_name = + let args, use_stdlib, coq_lang_version, wrapper_name, mode = match stanza with | None -> User_error.raise @@ -93,17 +93,24 @@ let term = ~dir_contents:dc theory coq_module , theory.buildable.use_stdlib , theory.buildable.coq_lang_version - , Dune_rules.Coq_lib_name.wrapper (snd theory.name) ) + , Dune_rules.Coq_lib_name.wrapper (snd theory.name) + , theory.buildable.mode ) | Some (`Extraction extr) -> ( Dune_rules.Coq_rules.coqtop_args_extraction ~sctx ~dir extr coq_module , extr.buildable.use_stdlib , extr.buildable.coq_lang_version - , "DuneExtraction" ) + , "DuneExtraction" + , extr.buildable.mode ) in let* (_ : unit * Dep.Fact.t Dep.Map.t) = let deps_of = - Dune_rules.Coq_rules.deps_of ~dir ~use_stdlib ~wrapper_name + let mode = + match mode with + | None -> Dune_rules.Coq_mode.VoOnly + | Some mode -> mode + in + Dune_rules.Coq_rules.deps_of ~dir ~use_stdlib ~wrapper_name ~mode ~coq_lang_version coq_module in Action_builder.(run deps_of) Eager diff --git a/doc/coq.rst b/doc/coq.rst index 7265c7ffaa4..fed9b5f9f4d 100644 --- a/doc/coq.rst +++ b/doc/coq.rst @@ -152,6 +152,12 @@ The semantics of the fields are: Previous versions of Dune before 3.7 would disable the native rules depending on whether or not the ``dev`` profile was selected. +- From version :ref:`Coq lang 0.8` onwards, ``(mode vos)`` makes it + so that only Coq compiled interface files are produced for the theory. This + is mainly useful in conjunction with ``dune coq top``, since this makes the + compilation of dependencies much faster (thought the proofs they contain are + not checked). + Coq Dependencies ~~~~~~~~~~~~~~~~ diff --git a/src/dune_rules/coq/coq_mode.ml b/src/dune_rules/coq/coq_mode.ml index b512dc3214f..a2ffeffbbe3 100644 --- a/src/dune_rules/coq/coq_mode.ml +++ b/src/dune_rules/coq/coq_mode.ml @@ -10,11 +10,13 @@ type t = | Legacy | VoOnly | Native + | VosOnly let decode ~coq_syntax = Dune_lang.Decoder.( enum' [ ("vo", return VoOnly) + ; ("vos", return VosOnly) ; ( "native" , Dune_sexp.Syntax.deprecated_in coq_syntax (0, 7) ~extra_info: diff --git a/src/dune_rules/coq/coq_mode.mli b/src/dune_rules/coq/coq_mode.mli index 2f9dbdde53c..f2d227aa983 100644 --- a/src/dune_rules/coq/coq_mode.mli +++ b/src/dune_rules/coq/coq_mode.mli @@ -10,5 +10,6 @@ type t = | Legacy | VoOnly | Native + | VosOnly val decode : coq_syntax:Dune_lang.Syntax.t -> t Dune_lang.Decoder.t diff --git a/src/dune_rules/coq/coq_module.ml b/src/dune_rules/coq/coq_module.ml index 7fe823d8129..1867b870d1d 100644 --- a/src/dune_rules/coq/coq_module.ml +++ b/src/dune_rules/coq/coq_module.ml @@ -88,11 +88,13 @@ let obj_files x ~wrapper_name ~mode ~obj_dir ~obj_files_mode = ( Path.Build.relative vo_dir x , Filename.(concat (concat install_vo_dir ".coq-native") x) )) cmxs_obj - | VoOnly | Legacy -> [] + | VoOnly | VosOnly | Legacy -> [] in let obj_files = match obj_files_mode with + | Build when mode = VosOnly -> [ x.name ^ ".vos" ] | Build -> [ x.name ^ ".vo"; x.name ^ ".glob" ] + | Install when mode = VosOnly -> [ x.name ^ ".vos" ] | Install -> [ x.name ^ ".vo" ] in List.map obj_files ~f:(fun fname -> diff --git a/src/dune_rules/coq/coq_rules.ml b/src/dune_rules/coq/coq_rules.ml index 10dac21e098..0bb5d6ba921 100644 --- a/src/dune_rules/coq/coq_rules.ml +++ b/src/dune_rules/coq/coq_rules.ml @@ -132,6 +132,16 @@ let coqc_native_flags ~sctx ~dir ~theories_deps ~theory_dirs ; "-native-compiler" ; "ondemand" ] + | VosOnly -> + Command.Args.As + [ "-vos" + ; "-w" + ; "-deprecated-native-compiler-option" + ; "-w" + ; "-native-compiler-disabled" + ; "-native-compiler" + ; "ondemand" + ] | Native -> let args = let open Action_builder.O in @@ -294,7 +304,7 @@ let setup_coqdep_for_theory_rule ~sctx ~dir ~loc ~theories_deps ~wrapper_name let file_flags = [ Command.Args.S (coqc_file_flags ~dir ~theories_deps ~wrapper_name ~boot_type ~ml_flags) - ; As [ "-dyndep"; "opt" ] + ; As [ "-dyndep"; "opt"; "-vos" ] ; Deps sources ] in @@ -350,10 +360,15 @@ let get_dep_map ~dir ~wrapper_name : Path.t list Dep_map.t Action_builder.t = ; ("entry 2", Dyn.list Path.to_dyn r2) ] -let deps_of ~dir ~boot_type ~wrapper_name coq_module = +let deps_of ~dir ~boot_type ~wrapper_name ~mode coq_module = let open Action_builder.O in let vo_target = - Path.Build.set_extension ~ext:".vo" (Coq_module.source coq_module) + let ext = + match mode with + | Coq_mode.VosOnly -> ".vos" + | _ -> ".vo" + in + Path.Build.set_extension ~ext (Coq_module.source coq_module) in get_dep_map ~dir ~wrapper_name >>= fun dep_map -> match Dep_map.find dep_map (Path.build vo_target) with @@ -397,6 +412,12 @@ let generic_coq_args ~sctx ~dir ~wrapper_name ~boot_type ~mode ~coq_prog Command.Args.dyn coq_flags (* stanza flags *) in let coq_native_flags = + let mode = + (* Tweak the modes for coqtop since it has no "-vos" option *) + match (mode, coq_prog) with + | Coq_mode.VosOnly, `Coqtop -> Coq_mode.VoOnly + | _ -> mode + in coqc_native_flags ~sctx ~dir ~theories_deps ~theory_dirs ~mode in let file_flags = @@ -429,7 +450,7 @@ let setup_coqc_rule ~loc ~dir ~sctx ~coqc_dir ~file_targets ~stanza_flags generic_coq_args ~sctx ~dir ~wrapper_name ~boot_type ~stanza_flags ~ml_flags ~theories_deps ~theory_dirs ~mode ~coq_prog:`Coqc coq_module in - let deps_of = deps_of ~dir ~boot_type ~wrapper_name coq_module in + let deps_of = deps_of ~dir ~boot_type ~wrapper_name ~mode coq_module in let open Action_builder.With_targets.O in Super_context.add_rule ~loc ~dir sctx (Action_builder.with_no_targets deps_of @@ -807,10 +828,10 @@ let coqtop_args_extraction ~sctx ~dir (s : Coq_stanza.Extraction.t) coq_module = ~theory_dirs:Path.Build.Set.empty coq_module (* Version for export *) -let deps_of ~dir ~use_stdlib ~wrapper_name ~coq_lang_version coq_module = +let deps_of ~dir ~use_stdlib ~wrapper_name ~mode ~coq_lang_version coq_module = let open Action_builder.O in let* boot_type = Action_builder.of_memo (boot_type ~dir ~use_stdlib ~wrapper_name ~coq_lang_version coq_module) in - deps_of ~dir ~boot_type ~wrapper_name coq_module + deps_of ~dir ~boot_type ~wrapper_name ~mode coq_module diff --git a/src/dune_rules/coq/coq_rules.mli b/src/dune_rules/coq/coq_rules.mli index 40425239188..8d0c404d012 100644 --- a/src/dune_rules/coq/coq_rules.mli +++ b/src/dune_rules/coq/coq_rules.mli @@ -11,6 +11,7 @@ val deps_of : dir:Path.Build.t -> use_stdlib:bool -> wrapper_name:string + -> mode:Coq_mode.t -> coq_lang_version:Dune_sexp.Syntax.Version.t -> Coq_module.t -> unit Dune_engine.Action_builder.t diff --git a/src/dune_rules/dune_rules.ml b/src/dune_rules/dune_rules.ml index 022931a5fb7..2fd83356005 100644 --- a/src/dune_rules/dune_rules.ml +++ b/src/dune_rules/dune_rules.ml @@ -44,6 +44,7 @@ module Dep_rules = Dep_rules module Dep_graph = Dep_graph module Preprocess = Preprocess module Preprocessing = Preprocessing +module Coq_mode = Coq_mode module Coq_rules = Coq_rules module Coq_module = Coq_module module Coq_sources = Coq_sources diff --git a/test/blackbox-tests/test-cases/coq/vos-build.t/bar.v b/test/blackbox-tests/test-cases/coq/vos-build.t/bar.v new file mode 100644 index 00000000000..4627b76131c --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/vos-build.t/bar.v @@ -0,0 +1,3 @@ +From basic Require Import foo. + +Definition mynum (i : mynat) := 3. diff --git a/test/blackbox-tests/test-cases/coq/vos-build.t/base.opam b/test/blackbox-tests/test-cases/coq/vos-build.t/base.opam new file mode 100644 index 00000000000..e69de29bb2d diff --git a/test/blackbox-tests/test-cases/coq/vos-build.t/dune b/test/blackbox-tests/test-cases/coq/vos-build.t/dune new file mode 100644 index 00000000000..fb485f824d9 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/vos-build.t/dune @@ -0,0 +1,10 @@ +(coq.theory + (name basic) + (package base) + (modules :standard) + (mode vos) + (synopsis "Test Coq library")) + +(rule + (alias default) + (action (echo "%{read:base.install}"))) diff --git a/test/blackbox-tests/test-cases/coq/vos-build.t/dune-project b/test/blackbox-tests/test-cases/coq/vos-build.t/dune-project new file mode 100644 index 00000000000..8b858cdefd7 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/vos-build.t/dune-project @@ -0,0 +1,2 @@ +(lang dune 3.8) +(using coq 0.8) diff --git a/test/blackbox-tests/test-cases/coq/vos-build.t/dune-vo b/test/blackbox-tests/test-cases/coq/vos-build.t/dune-vo new file mode 100644 index 00000000000..87b4de1f55d --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/vos-build.t/dune-vo @@ -0,0 +1,10 @@ +(coq.theory + (name basic) + (package base) + (modules :standard) + (mode vo) + (synopsis "Test Coq library")) + +(rule + (alias default) + (action (echo "%{read:base.install}"))) diff --git a/test/blackbox-tests/test-cases/coq/vos-build.t/foo.v b/test/blackbox-tests/test-cases/coq/vos-build.t/foo.v new file mode 100644 index 00000000000..53e0ce1b152 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/vos-build.t/foo.v @@ -0,0 +1 @@ +Definition mynat := nat. diff --git a/test/blackbox-tests/test-cases/coq/vos-build.t/run.t b/test/blackbox-tests/test-cases/coq/vos-build.t/run.t new file mode 100644 index 00000000000..1b5e7031537 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/vos-build.t/run.t @@ -0,0 +1,51 @@ + $ dune build --display short foo.vos + coqdep .basic.theory.d + coqc foo.vos + + $ dune clean + $ dune build --display short bar.vos + coqdep .basic.theory.d + coqc foo.vos + coqc bar.vos + + $ cat foo.v | dune coq top -- foo.v 2>/dev/null | sed '/^Welcome to Coq/d' + mynat is defined + $ cat bar.v | dune coq top -- bar.v 2>/dev/null | sed '/^Welcome to Coq/d' + mynum is defined + + $ dune clean + $ dune build --display short --debug-dependency-path @all + coqdep .basic.theory.d + coqc foo.vos + coqc bar.vos + $ dune build --debug-dependency-path @default + lib: [ + "_build/install/default/lib/base/META" + "_build/install/default/lib/base/dune-package" + "_build/install/default/lib/base/opam" + ] + lib_root: [ + "_build/install/default/lib/coq/user-contrib/basic/bar.v" {"coq/user-contrib/basic/bar.v"} + "_build/install/default/lib/coq/user-contrib/basic/bar.vos" {"coq/user-contrib/basic/bar.vos"} + "_build/install/default/lib/coq/user-contrib/basic/foo.v" {"coq/user-contrib/basic/foo.v"} + "_build/install/default/lib/coq/user-contrib/basic/foo.vos" {"coq/user-contrib/basic/foo.vos"} + ] + +Checking that we can go back to vo mode (without cleaning). + + $ mv dune-vo dune + $ dune build --display short --debug-dependency-path @all + coqc foo.{glob,vo} + coqc bar.{glob,vo} + $ dune build --debug-dependency-path @default + lib: [ + "_build/install/default/lib/base/META" + "_build/install/default/lib/base/dune-package" + "_build/install/default/lib/base/opam" + ] + lib_root: [ + "_build/install/default/lib/coq/user-contrib/basic/bar.v" {"coq/user-contrib/basic/bar.v"} + "_build/install/default/lib/coq/user-contrib/basic/bar.vo" {"coq/user-contrib/basic/bar.vo"} + "_build/install/default/lib/coq/user-contrib/basic/foo.v" {"coq/user-contrib/basic/foo.v"} + "_build/install/default/lib/coq/user-contrib/basic/foo.vo" {"coq/user-contrib/basic/foo.vo"} + ]