ocaml · ejgallego · Mar 29, 2023 · Mar 23, 2023
diff --git 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
@@ -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

@@ -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<coq-lang>` 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
diff --git a/test/blackbox-tests/test-cases/coq/vos-build.t/dune 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
@@ -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
@@ -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
@@ -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
@@ -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"}
+  ]
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		From basic Require Import foo.

		Definition mynum (i : mynat) := 3.