Implementing support for vos/vok files.

A .vos file stores the result of compiling statements (defs, lemmas)
but not proofs.
A .vok file is an empty file that denotes successful compilation of
the full contents of a .v file.
Unlike a .vio file, a .vos file does not store suspended proofs,
so it is more lightweight. It cannot be completed into a .vo file.

22 files changed, 500 insertions, 169 deletions

diff --git a/.gitignore b/.gitignore
index ad5204847c..7b3eadf33b 100644
--- a/.gitignore
+++ b/.gitignore
@@ -2,6 +2,8 @@
 *.d
 *.d.raw
 *.vio
+*.vos
+*.vok
 *.vo
 *.cm*
 *.annot
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 48d5f4075e..be74b86b30 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -184,6 +184,13 @@ and ``coqtop``, unless stated otherwise:
 :-verbose: Output the content of the input file as it is compiled.
   This option is available for ``coqc`` only; it is the counterpart of
   -compile-verbose.
+:-vos: Indicate |Coq| to skip the processing of opaque proofs
+  (i.e., proofs ending with ``Qed`` or ``Admitted``), output a ``.vos`` files
+  instead of a ``.vo`` file, and to load ``.vos`` files instead of ``.vo`` files
+  when interpreting ``Require`` commands.
+:-vok: Indicate |Coq| to check a file completely, to load ``.vos`` files instead
+  of ``.vo`` files when interpreting ``Require`` commands, and to output an empty
+  ``.vok`` files upon success instead of writing a ``.vo`` file.
 :-w (all|none|w₁,…,wₙ): Configure the display of warnings. This
   option expects all, none or a comma-separated list of warning names or
   categories (see Section :ref:`controlling-display`).
@@ -245,6 +252,86 @@ and ``coqtop``, unless stated otherwise:
   currently associated color and exit.
 :-h, --help: Print a short usage and exit.
 
+
+
+Compiled interfaces (produced using ``-vos``)
+----------------------------------------------
+
+
+Compiled interfaces help saving time while developing Coq formalizations,
+by compiling the formal statements exported by a library independently of
+the proofs that it contains.
+
+   .. warning::
+
+      Compiled interfaces should only be used for development purposes.
+      At the end of the day, one still needs to proof check all files
+      by producing standard ``.vo`` files. (Technically, when using ``-vos``,
+      fewer universe constraints are collected.)
+
+   .. warning::
+
+      In the current implementation, the use of the command ``Include`` for
+      importing modules compiled using `-vos` might not work properly.
+
+
+**Typical usage.**
+
+Assume a file ``foo.v`` that depends on two files ``bar1.v`` and ``bar2.v``. The
+command ``make foo.requires_vos`` will compile ``bar1.v`` and ``bar2.v`` using
+the option ``-vos`` to skip the proofs, producing ``bar1.vos`` and ``bar2.vos``.
+At this point, one is ready to work interactively on the file ``foo.v``, even
+though it was never needed to compile the proofs involved in the ``bar*.v``
+files.
+
+Assume a set of files ``f1.v ... fn.v`` with linear dependencies. The command
+``make vos`` enables compiling the statements (i.e. excluding the proofs) in all
+the files. Next, ``make -j vok`` enables compiling all the proofs in parallel.
+Thus, calling ``make -j vok`` directly enables taking advantage of a maximal
+amount of parallelism during the compilation of the set of files.
+
+Note that this comes at the cost of parsing and typechecking all definitions
+twice, once for the ``.vos`` file and once for the ``.vok`` file. However, if
+files contain nontrivial proofs, or if the files have many linear chains of
+dependencies, or if one has many cores available, compilation should be faster
+overall.
+
+**Need for ``Proof using``**
+
+When a theorem is part of a section, typechecking the statement of this theorem
+might be insufficient for deducing the type of this statement as of at the end
+of the section. Indeed, the proof of the theorem could make use of section
+variables or section hypotheses that are not mentioned in the statement of the
+theorem.
+
+For this reason, proofs inside section should begin with :cmd:`Proof using`
+instead of :cmd:`Proof`, where after the ``using`` clause one should provide
+the list of the names of the section variables that are required for the proof
+but are not involved in the typechecking of the statement. Note that it is safe
+to write ``Proof using.`` instead of ``Proof.`` also for proofs that are not
+within a section.
+
+.. warn:: You should use the “Proof using [...].” syntax instead of “Proof.” to enable skipping this proof which is located inside a section. Give as argument to “Proof using” the list of section variables that are not needed to typecheck the statement but that are required by the proof.
+
+     If |Coq| is invoked using the ``-vos`` option, whenever it finds the
+     command ``Proof.`` inside a section, it will compile the proof, that is,
+     refuse to skip it, and it will raise a warning. To disable the warning, one
+     may pass the flag ``-w -proof-without-using-in-section``.
+
+**Interaction with standard compilation**
+
+When compiling a file ``foo.v`` using ``coqc`` in the standard way (i.e., without
+``-vos`` nor ``-vok``), an empty file ``foo.vos`` is created in addition to the
+regular output file ``foo.vo``. If ``coqc`` is subsequently invoked on some other
+file ``bar.v`` using option ``-vos`` or ``-vok``, and that ``bar.v`` requires
+``foo.v``, if |Coq| finds an empty file ``foo.vos``, then it will load
+``foo.vo`` instead of ``foo.vos``.
+
+The purpose of this feature is to allow users to benefit from the ``-vos``
+option even if they depend on libraries that were compiled in the traditional
+manner (i.e., never compiled using the ``-vos`` option).
+
+
 Compiled libraries checker (coqchk)
 ----------------------------------------
 
diff --git a/lib/flags.ml b/lib/flags.ml
index 7676665fe9..90b5f877d5 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -44,6 +44,8 @@ let with_options ol f x =
 let async_proofs_worker_id = ref "master"
 let async_proofs_is_worker () = !async_proofs_worker_id <> "master"
 
+let load_vos_libraries = ref false
+
 let debug = ref false
 
 let in_debugger = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 3f72cc4b91..76a78e61fc 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -35,6 +35,10 @@
 val async_proofs_worker_id : string ref
 val async_proofs_is_worker : unit -> bool
 
+(** Flag to indicate that .vos files should be loaded for dependencies
+    instead of .vo files. Used by -vos and -vok options. *)
+val load_vos_libraries : bool ref
+
 (** Debug flags *)
 val debug : bool ref
 val in_debugger : bool ref
diff --git a/stm/stm.ml b/stm/stm.ml
index 5c6df26cbb..c399b69a77 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2801,13 +2801,21 @@ let handle_failure (e, info) vcs =
   VCS.print ();
   Exninfo.iraise (e, info)
 
-let snapshot_vio ~doc ~output_native_objects ldir long_f_dot_vo =
+let snapshot_vio ~create_vos ~doc ~output_native_objects ldir long_f_dot_vo =
   let doc = finish ~doc in
   if List.length (VCS.branches ()) > 1 then
     CErrors.user_err ~hdr:"stm" (str"Cannot dump a vio with open proofs");
-  Library.save_library_to ~todo:(dump_snapshot ()) ~output_native_objects
-    ldir long_f_dot_vo
-    (Global.opaque_tables ());
+  (* LATER: when create_vos is true, it could be more efficient to not allocate the futures; but for now it seems useful for synchronization of the workers,
+  below, [snapshot] gets computed even if [create_vos] is true. *)
+  let (tasks,counters) = dump_snapshot() in
+  let except = List.fold_left (fun e (r,_) ->
+     Future.UUIDSet.add r.Stateid.uuid e) Future.UUIDSet.empty tasks in
+  let todo_proofs =
+    if create_vos
+      then Library.ProofsTodoSomeEmpty except
+      else Library.ProofsTodoSome (except,tasks,counters)
+    in
+  Library.save_library_to todo_proofs ~output_native_objects ldir long_f_dot_vo (Global.opaque_tables ());
   doc
 
 let reset_task_queue = Slaves.reset_task_queue
diff --git a/stm/stm.mli b/stm/stm.mli
index 29e4b02e3f..841adcf05b 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -159,8 +159,10 @@ val join : doc:doc -> doc
    - if the worker pool is empty, all tasks are saved
    - if the worker proof is not empty, then it waits until all workers
      are done with their current jobs and then dumps (or fails if one
-     of the completed tasks is a failure) *)
-val snapshot_vio : doc:doc -> output_native_objects:bool -> DirPath.t -> string -> doc
+     of the completed tasks is a failure).
+   Note: the create_vos argument is used in the "-vos" mode, where the
+   proof tasks are not dumped into the output file. *)
+val snapshot_vio : create_vos:bool -> doc:doc -> output_native_objects:bool -> DirPath.t -> string -> doc
 
 (* Empties the task queue, can be used only if the worker pool is empty (E.g.
  * after having built a .vio in batch mode *)
diff --git a/test-suite/Makefile b/test-suite/Makefile
index c60f39231e..d9c89d7a8a 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -131,9 +131,10 @@ bugs: $(BUGS)
 
 clean:
 	rm -f trace .nia.cache .lia.cache output/MExtraction.out
+	rm -f vos/Makefile vos/Makefile.conf
 	$(SHOW) 'RM        <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>'
 	$(HIDE)find . \( \
-	  -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.log' -o -name '*.glob' \
+	  -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.vos' -o -name '*.vok' -o -name '*.log' -o -name '*.glob' \
 	  \) -exec rm -f {} +
 	$(SHOW) 'RM        <**/*.cmx> <**/*.cmi> <**/*.o> <**/*.test>'
 	$(HIDE)find unit-tests \( \
@@ -748,3 +749,23 @@ tools/%.log : tools/%/run.sh
 	    $(FAIL); \
 	  fi; \
 	) > "$@"
+
+# vos/
+
+vos: vos/run.log
+
+vos/run.log: $(wildcard vos/*.sh) $(wildcard vos/*.v)
+	@echo "TEST      vos"
+	$(HIDE)(\
+	  export COQBIN=$(BIN);\
+	  cd vos && \
+	  bash run.sh 2>&1; \
+	if [ $$? = 0 ]; then \
+	    echo $(log_success); \
+	    echo "    $<...Ok"; \
+	  else \
+	    echo $(log_failure); \
+	    echo "    $<...Error!"; \
+	    $(FAIL); \
+	  fi; \
+	) > "$@"
diff --git a/test-suite/misc/deps/deps.out b/test-suite/misc/deps/deps.out
index 5b79349fc2..d0263b8935 100644
--- a/test-suite/misc/deps/deps.out
+++ b/test-suite/misc/deps/deps.out
@@ -1 +1 @@
-misc/deps/client/bar.vo misc/deps/client/bar.glob misc/deps/client/bar.v.beautified: misc/deps/client/bar.v misc/deps/client/foo.vo misc/deps/lib/foo.vo
+misc/deps/client/bar.vo misc/deps/client/bar.glob misc/deps/client/bar.v.beautified misc/deps/client/bar.required_vo: misc/deps/client/bar.v misc/deps/client/foo.vo misc/deps/lib/foo.vo
diff --git a/test-suite/vos/A.v b/test-suite/vos/A.v
new file mode 100644
index 0000000000..11245ba015
--- /dev/null
+++ b/test-suite/vos/A.v
@@ -0,0 +1,4 @@
+Definition x := 3.
+
+Lemma xeq : x = x.
+Proof. auto. Qed.
diff --git a/test-suite/vos/B.v b/test-suite/vos/B.v
new file mode 100644
index 0000000000..735fefd745
--- /dev/null
+++ b/test-suite/vos/B.v
@@ -0,0 +1,34 @@
+Require Import A.
+
+Definition y := x.
+
+Lemma yeq : y = y.
+Proof. pose xeq. auto. Qed.
+
+
+Section Foo.
+
+Variable (HFalse : False).
+
+Lemma yeq' : y = y.
+Proof using HFalse. elimtype False. apply HFalse. Qed.
+
+End Foo.
+
+Module Type E. End E.
+
+Module M.
+  Lemma x : True.
+  Proof. trivial. Qed.
+End M.
+
+
+Module Type T.
+  Lemma x : True.
+  Proof. trivial. Qed.
+End T.
+
+Module F(X:E).
+  Lemma x : True.
+  Proof. trivial. Qed.
+End F.
diff --git a/test-suite/vos/C.v b/test-suite/vos/C.v
new file mode 100644
index 0000000000..5260b7cdaf
--- /dev/null
+++ b/test-suite/vos/C.v
@@ -0,0 +1,13 @@
+Require Import A B.
+
+Definition z := x + y.
+
+Lemma zeq : z = z.
+Proof. pose xeq. pose yeq. auto. Qed.
+
+Lemma yeq'' : y = y.
+Proof. apply yeq'. Admitted.
+
+Module M. Include B.M. End M.
+Module T. Include B.T. End T.
+Module F. Include B.F. End F.
diff --git a/test-suite/vos/run.sh b/test-suite/vos/run.sh
new file mode 100755
index 0000000000..2496fc8602
--- /dev/null
+++ b/test-suite/vos/run.sh
@@ -0,0 +1,23 @@
+#!/bin/bash
+set -e
+set -o pipefail
+export PATH="$COQBIN:$PATH"
+
+# Clean
+rm -f *.vo *.vos *.vok *.glob *.aux Makefile
+
+# Test building all vos, then all vok
+coq_makefile -R . TEST -o Makefile *.v
+make vos
+make vok
+
+# Cleanup
+make clean
+
+# Test using compilation in custom order
+set -x #echo on
+coqc A.v
+coqc -vos B.v
+coqc -vos C.v
+coqc -vok B.v
+coqc -vok C.v
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 626ac0fe67..1cceed79a4 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -408,6 +408,12 @@ checkproofs:
 		-schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)
 .PHONY: checkproofs
 
+vos: $(VOFILES:%.vo=%.vos)
+.PHONY: vos
+
+vok: $(VOFILES:%.vo=%.vok)
+.PHONY: vok
+
 validate: $(VOFILES)
 	$(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $^
 .PHONY: validate
@@ -558,6 +564,8 @@ clean::
 	$(HIDE)find . -name .coq-native -type d -empty -delete
 	$(HIDE)rm -f $(VOFILES)
 	$(HIDE)rm -f $(VOFILES:.vo=.vio)
+	$(HIDE)rm -f $(VOFILES:.vo=.vos)
+	$(HIDE)rm -f $(VOFILES:.vo=.vok)
 	$(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old)
 	$(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex
 	$(HIDE)rm -f $(VFILES:.v=.glob)
@@ -666,6 +674,14 @@ $(VFILES:.v=.vio): %.vio: %.v
 	$(SHOW)COQC -quick $<
 	$(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
 
+$(VFILES:.v=.vos): %.vos: %.v
+	$(SHOW)COQC -vos $<
+	$(HIDE)$(TIMER) $(COQC) -vos $(COQDEBUG) $(COQFLAGS) $<
+
+$(VFILES:.v=.vok): %.vok: %.v
+	$(SHOW)COQC -vok $<
+	$(HIDE)$(TIMER) $(COQC) -vok $(COQDEBUG) $(COQFLAGS) $<
+
 $(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing
 	$(SHOW)PYTHON TIMING-DIFF $<
 	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@"
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 8beb314046..ddedec12f8 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -235,15 +235,15 @@ let file_name s = function
 let depend_ML str =
   match search_mli_known str, search_ml_known str with
     | Some mlidir, Some mldir ->
-	let mlifile = file_name str mlidir
-	and mlfile = file_name str mldir in
-	(" "^mlifile^".cmi"," "^mlfile^".cmx")
+        let mlifile = file_name str mlidir
+        and mlfile = file_name str mldir in
+        (" "^mlifile^".cmi"," "^mlfile^".cmx")
     | None, Some mldir ->
-	let mlfile = file_name str mldir in
-	(" "^mlfile^".cmo"," "^mlfile^".cmx")
+        let mlfile = file_name str mldir in
+        (" "^mlfile^".cmo"," "^mlfile^".cmx")
     | Some mlidir, None ->
-	let mlifile = file_name str mlidir in
-	(" "^mlifile^".cmi"," "^mlifile^".cmi")
+        let mlifile = file_name str mlidir in
+        (" "^mlifile^".cmi"," "^mlifile^".cmi")
     | None, None -> "", ""
 
 let soustraite_fichier_ML dep md ext =
@@ -254,9 +254,9 @@ let soustraite_fichier_ML dep md ext =
     let a_faire_opt = ref "" in
     List.iter
       (fun str ->
-	 let byte,opt = depend_ML str in
-	 a_faire := !a_faire ^ byte;
-	 a_faire_opt := !a_faire_opt ^ opt)
+         let byte,opt = depend_ML str in
+         a_faire := !a_faire ^ byte;
+         a_faire_opt := !a_faire_opt ^ opt)
       (List.rev list);
     (!a_faire, !a_faire_opt)
   with
@@ -274,15 +274,15 @@ let autotraite_fichier_ML md ext =
     let a_faire_opt = ref "" in
     begin try
       while true do
-	let (Use_module str) = caml_action buf in
-	if StrSet.mem str !deja_vu then
-	  ()
-	else begin
-	  deja_vu := StrSet.add str !deja_vu;
-	  let byte,opt = depend_ML str in
-	  a_faire := !a_faire ^ byte;
-	  a_faire_opt := !a_faire_opt ^ opt
-	end
+        let (Use_module str) = caml_action buf in
+        if StrSet.mem str !deja_vu then
+          ()
+        else begin
+          deja_vu := StrSet.add str !deja_vu;
+          let byte,opt = depend_ML str in
+          a_faire := !a_faire ^ byte;
+          a_faire_opt := !a_faire_opt ^ opt
+        end
       done
     with Fin_fichier -> ()
     end;
@@ -301,14 +301,14 @@ let traite_fichier_modules md ext =
     let list = mllib_list (Lexing.from_channel chan) in
     List.fold_left
       (fun a_faire str -> match search_mlpack_known str with
-	| Some mldir ->
-	  let file = file_name str mldir in
+        | Some mldir ->
+          let file = file_name str mldir in
           a_faire @ [file]
-	| None ->
-	  match search_ml_known str with
-	    | Some mldir ->
-	      let file = file_name str mldir in
-              a_faire @ [file]
+        | None ->
+          match search_ml_known str with
+            | Some mldir ->
+              let file = file_name str mldir in
+                    a_faire @ [file]
             | None -> a_faire) [] list
   with
     | Sys_error _ -> []
@@ -329,16 +329,16 @@ let escape =
       let c = s.[i] in
       if c = ' ' || c = '#' || c = ':' (* separators and comments *)
         || c = '%' (* pattern *)
-	|| c = '?' || c = '[' || c = ']' || c = '*' (* expansion in filenames *)
-	|| i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' || 
-	    'A' <= s.[1] && s.[1] <= 'Z' || 
-	    'a' <= s.[1] && s.[1] <= 'z') (* homedir expansion *)
+        || c = '?' || c = '[' || c = ']' || c = '*' (* expansion in filenames *)
+        || i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' ||
+            'A' <= s.[1] && s.[1] <= 'Z' ||
+            'a' <= s.[1] && s.[1] <= 'z') (* homedir expansion *)
       then begin
-	let j = ref (i-1) in
-	while !j >= 0 && s.[!j] = '\\' do 
-	  Buffer.add_char s' '\\'; decr j (* escape all preceding '\' *)
-	done;
-	Buffer.add_char s' '\\';
+        let j = ref (i-1) in
+        while !j >= 0 && s.[!j] = '\\' do
+          Buffer.add_char s' '\\'; decr j (* escape all preceding '\' *)
+        done;
+        Buffer.add_char s' '\\';
       end;
       if c = '$' then Buffer.add_char s' '$';
       Buffer.add_char s' c
@@ -362,75 +362,116 @@ end
 
 module VCache = Set.Make(VData)
 
-let rec traite_fichier_Coq suffixe verbose f =
+(** To avoid reading .v files several times for computing dependencies,
+    once for .vo, once for .vio, and once for .vos extensions, the
+    following code performs a single pass and produces a structured
+    list of dependencies, separating dependencies on compiled Coq files
+    (those loaded by [Require]) from other dependencies, e.g. dependencies
+    on ".v" files (for [Load]) or ".cmx", ".cmo", etc... (for [Declare]). *)
+
+type dependency =
+  | DepRequire of string (* one basename, to which we later append .vo or .vio or .vos *)
+  | DepOther of string   (* filenames of dependencies, separated by spaces *)
+
+let string_of_dependency_list suffix_for_require deps =
+  let string_of_dep = function
+    | DepRequire basename -> basename ^ suffix_for_require
+    | DepOther s -> s
+    in
+  String.concat " " (List.map string_of_dep deps)
+
+let rec find_dependencies basename =
+  let verbose = true in (* for past/future use? *)
   try
+    (* Visited marks *)
+    let visited_ml = ref StrSet.empty in
+    let visited_v = ref VCache.empty in
+    let should_visit_v_and_mark from str =
+       if not (VCache.mem (from, str) !visited_v) then begin
+          visited_v := VCache.add (from, str) !visited_v;
+          true
+       end else false
+       in
+    (* Output: dependencies found *)
+    let dependencies = ref [] in
+    let add_dep dep =
+       dependencies := dep::!dependencies in
+    let add_dep_other s =
+       add_dep (DepOther s) in
+
+    (* Reading file contents *)
+    let f = basename ^ ".v" in
     let chan = open_in f in
     let buf = Lexing.from_channel chan in
-    let deja_vu_v = ref VCache.empty in
-    let deja_vu_ml = ref StrSet.empty in
     try
       while true do
-      	let tok = coq_action buf in
-	match tok with
-	  | Require (from, strl) ->
-	      List.iter (fun str ->
-		if not (VCache.mem (from, str) !deja_vu_v) then begin
-	          deja_vu_v := VCache.add (from, str) !deja_vu_v;
-                  try
-                    let file_str = safe_assoc from verbose f str in
-                    printf " %s%s" (canonize file_str) suffixe
-                  with Not_found ->
-		    if verbose && not (is_in_coqlib ?from str) then
-		      let str =
-			match from with
-			  | None -> str
-			  | Some pth -> pth @ str
-		      in
-                      warning_module_notfound f str
-       		end) strl
-	  | Declare sl ->
-	      let declare suff dir s =
-		let base = escape (file_name s dir) in
-                match !option_dynlink with
-                | No -> ()
-                | Byte -> printf " %s%s" base suff
-                | Opt -> printf " %s.cmxs" base
-                | Both -> printf " %s%s %s.cmxs" base suff base
-                | Variable ->
-                   printf " %s%s" base
-                    (if suff=".cmo" then "$(DYNOBJ)" else "$(DYNLIB)")
+        let tok = coq_action buf in
+        match tok with
+        | Require (from, strl) ->
+            List.iter (fun str ->
+              if should_visit_v_and_mark from str then begin
+              try
+                let file_str = safe_assoc from verbose f str in
+                add_dep (DepRequire (canonize file_str))
+              with Not_found ->
+                  if verbose && not (is_in_coqlib ?from str) then
+                    let str =
+                      match from with
+                      | None -> str
+                      | Some pth -> pth @ str
+                      in
+                  warning_module_notfound f str
+              end) strl
+        | Declare sl ->
+            let declare suff dir s =
+              let base = escape (file_name s dir) in
+              match !option_dynlink with
+              | No -> ()
+              | Byte -> add_dep_other (sprintf "%s%s" base suff)
+              | Opt -> add_dep_other (sprintf "%s.cmxs" base)
+              | Both -> add_dep_other (sprintf "%s%s" base suff);
+                        add_dep_other (sprintf "%s.cmxs" base)
+              | Variable -> add_dep_other (sprintf "%s%s" base
+                  (if suff=".cmo" then "$(DYNOBJ)" else "$(DYNLIB)"))
               in
-	      let decl str =
-                let s = basename_noext str in
-		if not (StrSet.mem s !deja_vu_ml) then begin
-		  deja_vu_ml := StrSet.add s !deja_vu_ml;
-		  match search_mllib_known s with
-		    | Some mldir -> declare ".cma" mldir s
-		    | None ->
-		      match search_mlpack_known s with
-			| Some mldir -> declare ".cmo" mldir s
-			| None ->
-			  match search_ml_known s with
-			    | Some mldir -> declare ".cmo" mldir s
-			    | None -> warning_declare f str
-		end
-	      in List.iter decl sl
-	  | Load str ->
-	      let str = Filename.basename str in
-	      if not (VCache.mem (None, [str]) !deja_vu_v) then begin
-	        deja_vu_v := VCache.add (None, [str]) !deja_vu_v;
-                try
-                  let (file_str, _) = Hashtbl.find vKnown [str] in
-                  let canon = canonize file_str in
-                  printf " %s.v" canon;
-                  traite_fichier_Coq suffixe true (canon ^ ".v")
-                with Not_found -> ()
-       	      end
-          | AddLoadPath _ | AddRecLoadPath _ -> (* TODO *) ()
-      done
-    with Fin_fichier -> close_in chan
-       | Syntax_error (i,j) -> close_in chan; error_cannot_parse f (i,j)
-  with Sys_error _ -> ()
+            let decl str =
+              let s = basename_noext str in
+              if not (StrSet.mem s !visited_ml) then begin
+                visited_ml := StrSet.add s !visited_ml;
+                match search_mllib_known s with
+                  | Some mldir -> declare ".cma" mldir s
+                  | None ->
+                    match search_mlpack_known s with
+                  | Some mldir -> declare ".cmo" mldir s
+                  | None ->
+                    match search_ml_known s with
+                      | Some mldir -> declare ".cmo" mldir s
+                      | None -> warning_declare f str
+                end
+                in
+              List.iter decl sl
+        | Load str ->
+            let str = Filename.basename str in
+            if should_visit_v_and_mark None [str] then begin
+              try
+                let (file_str, _) = Hashtbl.find vKnown [str] in
+                let canon = canonize file_str in
+                add_dep_other (sprintf "%s.v" canon);
+                let deps = find_dependencies canon in
+                List.iter add_dep deps
+              with Not_found -> ()
+            end
+        | AddLoadPath _ | AddRecLoadPath _ -> (* TODO: will this be handled? *) ()
+      done;
+      List.rev !dependencies
+    with
+    | Fin_fichier ->
+        close_in chan;
+        List.rev !dependencies
+    | Syntax_error (i,j) ->
+        close_in chan;
+        error_cannot_parse f (i,j)
+  with Sys_error _ -> [] (* TODO: report an error? *)
 
 
 let mL_dependencies () =
@@ -439,8 +480,8 @@ let mL_dependencies () =
        let fullname = file_name name dirname in
        let (dep,dep_opt) = traite_fichier_ML fullname ext in
        let intf = match search_mli_known name with
-	 | None -> ""
-	 | Some mldir -> " "^(file_name name mldir)^".cmi"
+         | None -> ""
+         | Some mldir -> " "^(file_name name mldir)^".cmi"
        in
        let efullname = escape fullname in
        printf "%s.cmo:%s%s\n" efullname dep intf;
@@ -481,12 +522,14 @@ let coq_dependencies () =
     (fun (name,_) ->
        let ename = escape name in
        let glob = if !option_noglob then "" else " "^ename^".glob" in
-       printf "%s%s%s %s.v.beautified: %s.v" ename !suffixe glob ename ename;
-       traite_fichier_Coq !suffixe true (name ^ ".v");
-       printf "\n";
-       printf "%s.vio: %s.v" ename ename;
-       traite_fichier_Coq ".vio" true (name ^ ".v");
-       printf "\n%!")
+       let deps = find_dependencies name in
+       printf "%s%s%s %s.v.beautified %s.required_vo: %s.v %s\n" ename !suffixe glob ename ename ename
+        (string_of_dependency_list !suffixe deps);
+       printf "%s.vio: %s.v %s\n" ename ename
+        (string_of_dependency_list ".vio" deps);
+       printf "%s.vos %s.vok %s.required_vos: %s.v %s\n" ename ename ename ename
+        (string_of_dependency_list ".vos" deps);
+       printf "%!")
     (List.rev !vAccu)
 
 let rec suffixes = function
@@ -505,26 +548,26 @@ let add_caml_known phys_dir _ f =
     | _ -> ()
 
 let add_coqlib_known recur phys_dir log_dir f =
-  match get_extension f [".vo"; ".vio"] with
-    | (basename, (".vo" | ".vio")) ->
+  match get_extension f [".vo"; ".vio"; ".vos"] with
+    | (basename, (".vo" | ".vio" | ".vos")) ->
         let name = log_dir@[basename] in
         let paths = if recur then suffixes name else [name] in
         List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
     | _ -> ()
 
 let add_known recur phys_dir log_dir f =
-  match get_extension f [".v"; ".vo"; ".vio"] with
+  match get_extension f [".v"; ".vo"; ".vio"; ".vos"] with
     | (basename,".v") ->
-	let name = log_dir@[basename] in
-	let file = phys_dir//basename in
-	let () = safe_hash_add compare_file clash_v vKnown (name, (file, true)) in
-	if recur then
+        let name = log_dir@[basename] in
+        let file = phys_dir//basename in
+        let () = safe_hash_add compare_file clash_v vKnown (name, (file, true)) in
+        if recur then
           let paths = List.tl (suffixes name) in
           let iter n = safe_hash_add compare_file clash_v vKnown (n, (file, false)) in
           List.iter iter paths
-    | (basename, (".vo" | ".vio")) when not(!option_boot) ->
+    | (basename, (".vo" | ".vio" | ".vos")) when not(!option_boot) ->
         let name = log_dir@[basename] in
-	let paths = if recur then suffixes name else [name] in
+        let paths = if recur then suffixes name else [name] in
         List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
     | _ -> ()
 
@@ -576,12 +619,12 @@ let rec treat_file old_dirname old_name =
   let complete_name = file_name name dirname in
   match try (stat complete_name).st_kind with _ -> S_BLK with
     | S_DIR ->
-	(if name.[0] <> '.' then
+        (if name.[0] <> '.' then
            let newdirname =
              match dirname with
                | None -> name
                | Some d -> d//name
-	   in
+           in
            Array.iter (treat_file (Some newdirname)) (Sys.readdir complete_name))
     | S_REG ->
         (match get_extension name [".v";".ml";".mli";".mlg";".mllib";".mlpack"] with
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index 3600658e23..3cbbf3d186 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -88,6 +88,10 @@ let ensure_exists_with_prefix f_in f_out src_suffix tgt_suffix =
     | Some f -> ensure tgt_suffix long_f_dot_src f in
   long_f_dot_src, long_f_dot_tgt
 
+let create_empty_file filename =
+  let f = open_out filename in
+  close_out f
+
 (* Compile a vernac file *)
 let compile opts copts ~echo ~f_in ~f_out =
   let open Vernac.State in
@@ -106,43 +110,53 @@ let compile opts copts ~echo ~f_in ~f_out =
   let output_native_objects = match opts.config.native_compiler with
     | NativeOff -> false | NativeOn {ondemand} -> not ondemand
   in
-  match copts.compilation_mode with
-  | BuildVo ->
-      let long_f_dot_v, long_f_dot_vo =
-        ensure_exists_with_prefix f_in f_out ".v" ".vo" in
-
+  let mode = copts.compilation_mode in
+  let ext_in, ext_out =
+     match mode with
+     | BuildVo -> ".v", ".vo"
+     | BuildVio -> ".v", ".vio"
+     | Vio2Vo -> ".vio", ".vo"
+     | BuildVos -> ".v", ".vos"
+     | BuildVok -> ".v", ".vok"
+  in
+  let long_f_dot_in, long_f_dot_out =
+    ensure_exists_with_prefix f_in f_out ext_in ext_out in
+  match mode with
+  | BuildVo | BuildVok ->
       let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
           Stm.new_doc
-          Stm.{ doc_type = VoDoc long_f_dot_vo;
+          Stm.{ doc_type = VoDoc long_f_dot_out;
                 iload_path; require_libs; stm_options;
               } in
       let state = { doc; sid; proof = None; time = opts.config.time } in
       let state = load_init_vernaculars opts ~state in
       let ldir = Stm.get_ldir ~doc:state.doc in
       Aux_file.(start_aux_file
-        ~aux_file:(aux_file_name_for long_f_dot_vo)
-        ~v_file:long_f_dot_v);
+        ~aux_file:(aux_file_name_for long_f_dot_out)
+        ~v_file:long_f_dot_in);
 
       Dumpglob.set_glob_output copts.glob_out;
-      Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo;
+      Dumpglob.start_dump_glob ~vfile:long_f_dot_in ~vofile:long_f_dot_out;
       Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
 
       let wall_clock1 = Unix.gettimeofday () in
       let check = Stm.AsyncOpts.(stm_options.async_proofs_mode = APoff) in
-      let state = Vernac.load_vernac ~echo ~check ~interactive:false ~state long_f_dot_v in
+      let state = Vernac.load_vernac ~echo ~check ~interactive:false ~state long_f_dot_in in
       let _doc = Stm.join ~doc:state.doc in
       let wall_clock2 = Unix.gettimeofday () in
       check_pending_proofs ();
-      Library.save_library_to ~output_native_objects ldir long_f_dot_vo (Global.opaque_tables ());
+      if mode <> BuildVok  (* Don't output proofs in -vok mode *)
+        then Library.save_library_to ~output_native_objects Library.ProofsTodoNone ldir long_f_dot_out (Global.opaque_tables ());
       Aux_file.record_in_aux_at "vo_compile_time"
         (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
       Aux_file.stop_aux_file ();
+      (* Produce an empty .vos file when producing a .vo in standard mode *)
+      if mode = BuildVo then create_empty_file (long_f_dot_out ^ "s");
+      (* Produce an empty .vok file when in -vok mode *)
+      if mode = BuildVok then create_empty_file (long_f_dot_out);
       Dumpglob.end_dump_glob ()
 
-  | BuildVio ->
-      let long_f_dot_v, long_f_dot_vio =
-        ensure_exists_with_prefix f_in f_out ".v" ".vio" in
-
+  | BuildVio | BuildVos ->
       (* We need to disable error resiliency, otherwise some errors
          will be ignored in batch mode. c.f. #6707
 
@@ -158,26 +172,26 @@ let compile opts copts ~echo ~f_in ~f_out =
 
       let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
           Stm.new_doc
-          Stm.{ doc_type = VioDoc long_f_dot_vio;
+          Stm.{ doc_type = VioDoc long_f_dot_out;
                 iload_path; require_libs; stm_options;
               } in
 
       let state = { doc; sid; proof = None; time = opts.config.time } in
       let state = load_init_vernaculars opts ~state in
       let ldir = Stm.get_ldir ~doc:state.doc in
-      let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_v in
+      let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_in in
       let doc = Stm.finish ~doc:state.doc in
       check_pending_proofs ();
-      let () = ignore (Stm.snapshot_vio ~doc ~output_native_objects ldir long_f_dot_vio) in
+      let create_vos = (mode = BuildVos) in
+      let () = ignore (Stm.snapshot_vio ~create_vos ~doc ~output_native_objects ldir long_f_dot_out) in
       Stm.reset_task_queue ()
 
   | Vio2Vo ->
-      let long_f_dot_vio, long_f_dot_vo =
-        ensure_exists_with_prefix f_in f_out ".vio" ".vo" in
+
       let sum, lib, univs, tasks, proofs =
-        Library.load_library_todo long_f_dot_vio in
-      let univs, proofs = Stm.finish_tasks long_f_dot_vo univs proofs tasks in
-      Library.save_library_raw long_f_dot_vo sum lib univs proofs
+        Library.load_library_todo long_f_dot_in in
+      let univs, proofs = Stm.finish_tasks long_f_dot_out univs proofs tasks in
+      Library.save_library_raw long_f_dot_out sum lib univs proofs
 
 let compile opts copts ~echo ~f_in ~f_out =
   ignore(CoqworkmgrApi.get 1);
diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml
index 98206fb341..178aa362c0 100644
--- a/toplevel/coqc.ml
+++ b/toplevel/coqc.ml
@@ -30,6 +30,9 @@ coqc specific options:\
 \n                         into fi.vo\
 \n  -schedule-vio-checking j f1..fn   run up to j instances of Coq to check all\
 \n                         proofs in each fi.vio\
+\n  -vos                   process statements but ignore opaque proofs, and produce a .vos file\
+\n  -vok                   process the file by loading .vos instead of .vo files for\
+\n                         dependencies, and produce an empty .vok file on success\
 \n\
 \nUndocumented:\
 \n  -vio2vo                [see manual]\
diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml
index c4e3571281..e614d4fe6d 100644
--- a/toplevel/coqcargs.ml
+++ b/toplevel/coqcargs.ml
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-type compilation_mode = BuildVo | BuildVio | Vio2Vo
+type compilation_mode = BuildVo | BuildVio | Vio2Vo | BuildVos | BuildVok
 
 type t =
   { compilation_mode : compilation_mode
@@ -166,6 +166,13 @@ let parse arglist : t =
           { oval with compilation_output_name = Some (next ()) }
         | "-quick" ->
           set_compilation_mode oval BuildVio
+        |"-vos" ->
+          Flags.load_vos_libraries := true;
+          { oval with compilation_mode = BuildVos }
+        |"-vok" ->
+          Flags.load_vos_libraries := true;
+          { oval with compilation_mode = BuildVok }
+
         | "-check-vio-tasks" ->
           let tno = get_task_list (next ()) in
           let tfile = next () in
diff --git a/toplevel/coqcargs.mli b/toplevel/coqcargs.mli
index 13bea3bf3e..677a3f2e48 100644
--- a/toplevel/coqcargs.mli
+++ b/toplevel/coqcargs.mli
@@ -8,7 +8,21 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-type compilation_mode = BuildVo | BuildVio | Vio2Vo
+(** Compilation modes:
+  - BuildVo      : process statements and proofs (standard compilation),
+                   and also output an empty .vos file
+  - BuildVio     : process statements, delay proofs in futures
+  - Vio2Vo       : load delayed proofs and process them
+  - BuildVos     : process statements, and discard proofs,
+                   and load .vos files for required libraries
+  - BuildVok     : like BuildVo, but load .vos files for required libraries
+
+  When loading the .vos version of a required library, if the file exists but is
+  empty, then we attempt to load the .vo version of that library.
+  This trick is useful to avoid the need for the user to compile .vos version
+  when an up to date .vo version is already available.
+*)
+type compilation_mode = BuildVo | BuildVio | Vio2Vo | BuildVos | BuildVok
 
 type t =
   { compilation_mode : compilation_mode
diff --git a/vernac/library.ml b/vernac/library.ml
index 8125c3de35..244424de6b 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -430,23 +430,33 @@ let error_recursively_dependent_library dir =
 (* Security weakness: file might have been changed on disk between
    writing the content and computing the checksum... *)
 
-let save_library_to ?todo ~output_native_objects dir f otab =
-  let except = match todo with
-    | None ->
-        (* XXX *)
-        (* assert(!Flags.compilation_mode = Flags.BuildVo); *)
-        assert(Filename.check_suffix f ".vo");
-        Future.UUIDSet.empty
-    | Some (l,_) ->
-        assert(Filename.check_suffix f ".vio");
-        List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e)
-          Future.UUIDSet.empty l in
+type ('document,'counters) todo_proofs =
+ | ProofsTodoNone (* for .vo *)
+ | ProofsTodoSomeEmpty of Future.UUIDSet.t (* for .vos *)
+ | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list * 'counters (* for .vio *)
+
+let save_library_to todo_proofs ~output_native_objects dir f otab =
+  assert(
+    let expected_extension = match todo_proofs with
+      | ProofsTodoNone -> ".vo"
+      | ProofsTodoSomeEmpty _ -> ".vos"
+      | ProofsTodoSome _ -> ".vio"
+      in
+    Filename.check_suffix f expected_extension);
+  let except = match todo_proofs with
+    | ProofsTodoNone -> Future.UUIDSet.empty
+    | ProofsTodoSomeEmpty except -> except
+    | ProofsTodoSome (except,l,_) -> except
+    in
   let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in
   let opaque_table, f2t_map = Opaqueproof.dump ~except otab in
   let tasks, utab =
-    match todo with
-    | None -> None, None
-    | Some (tasks, rcbackup) ->
+    match todo_proofs with
+    | ProofsTodoNone -> None, None
+    | ProofsTodoSomeEmpty _except ->
+        None,
+        Some (Univ.ContextSet.empty,false)
+    | ProofsTodoSome (_except, tasks, rcbackup) ->
         let tasks =
           List.map Stateid.(fun (r,b) ->
             try { r with uuid = Future.UUIDMap.find r.uuid f2t_map }, b
diff --git a/vernac/library.mli b/vernac/library.mli
index 6a32413248..ec485e6408 100644
--- a/vernac/library.mli
+++ b/vernac/library.mli
@@ -36,10 +36,18 @@ type seg_univ = (* all_cst, finished? *)
   Univ.ContextSet.t * bool
 type seg_proofs = Opaqueproof.opaque_proofterm array
 
-(** End the compilation of a library and save it to a ".vo" file.
+(** End the compilation of a library and save it to a ".vo" file,
+    a ".vio" file, or a ".vos" file, depending on the todo_proofs
+    argument.
     [output_native_objects]: when producing vo objects, also compile the native-code version. *)
+
+type ('document,'counters) todo_proofs =
+ | ProofsTodoNone (* for .vo *)
+ | ProofsTodoSomeEmpty of Future.UUIDSet.t (* for .vos *)
+ | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list * 'counters (* for .vio *)
+
 val save_library_to :
-  ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) ->
+  ('document,'counters) todo_proofs ->
   output_native_objects:bool ->
   DirPath.t -> string -> Opaqueproof.opaquetab -> unit
 
diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml
index bea0c943c3..b3dc254a63 100644
--- a/vernac/loadpath.ml
+++ b/vernac/loadpath.ml
@@ -138,6 +138,18 @@ let select_vo_file ~warn loadpath base =
         System.where_in_path ~warn loadpath name in
       Some (lpath, file)
     with Not_found -> None in
+  if !Flags.load_vos_libraries then begin
+    (* If the .vos file exists and is not empty, it describes the library.
+       If the .vos file exists and is empty, then load the .vo file.
+       If the .vos file is missing, then fail. *)
+    match find ".vos" with
+    | None -> Error LibNotFound
+    | Some (_, vos as resvos) ->
+        if (Unix.stat vos).Unix.st_size > 0 then Ok resvos else
+        match find ".vo" with
+        | None -> Error LibNotFound
+        | Some resvo -> Ok resvo
+  end else
   match find ".vo", find ".vio" with
   | None, None ->
     Error LibNotFound
@@ -189,8 +201,10 @@ let error_unmapped_dir qid =
             ])
 
 let error_lib_not_found qid =
+  let vos = !Flags.load_vos_libraries in
+  let vos_msg = if vos then [Pp.str " (while searching for a .vos file)"] else [] in
   CErrors.user_err ~hdr:"load_absolute_library_from"
-    Pp.(seq [ str "Cannot find library "; Libnames.pr_qualid qid; str" in loadpath"])
+    Pp.(seq ([ str "Cannot find library "; Libnames.pr_qualid qid; str" in loadpath"]@vos_msg))
 
 let try_locate_absolute_library dir =
   match locate_absolute_library dir with
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index edff80af00..ade291918e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -406,8 +406,10 @@ let err_notfound_library ?from qid =
   | Some from ->
     str " with prefix " ++ DirPath.print from ++ str "."
   in
+  let bonus =
+    if !Flags.load_vos_libraries then " (While searching for a .vos file.)" else "" in
   user_err ?loc:qid.CAst.loc ~hdr:"locate_library"
-     (strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix)
+     (strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix ++ str bonus)
 
 let print_located_library qid =
   let open Loadpath in
@@ -830,7 +832,7 @@ let vernac_scheme l =
 	       Option.iter (fun lid -> Dumpglob.dump_definition lid false "def") lid;
 	       match s with
 	       | InductionScheme (_, r, _)
-	       | CaseScheme (_, r, _) 
+               | CaseScheme (_, r, _)
 	       | EqualityScheme r -> dump_global r) l;
   Indschemes.do_scheme l