Merge PR #11280: Fix #11195 and add other improvements: try loading .vio (and not just…

Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: ppedrot

14 files changed, 93 insertions, 45 deletions

diff --git a/Makefile.build b/Makefile.build
index 5b879220d0..a8ae040f8e 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -840,7 +840,7 @@ theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP)
 
 theories/Init/%.vio: theories/Init/%.v $(VO_TOOLS_DEP)
 	$(SHOW)'COQC -quick -noinit $<'
-	$(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq -quick -noglob
+	$(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq -vio -noglob
 
 # The general rule for building .vo files :
 
@@ -855,8 +855,8 @@ ifdef VALIDATE
 endif
 
 %.vio: %.v theories/Init/Prelude.vio $(VO_TOOLS_DEP)
-	$(SHOW)'COQC -quick $<'
-	$(HIDE)$(BOOTCOQC) $< -quick -noglob
+	$(SHOW)'COQC -vio $<'
+	$(HIDE)$(BOOTCOQC) $< -vio -noglob
 
 %.v.timing.diff: %.v.before-timing %.v.after-timing
 	$(SHOW)PYTHON TIMING-DIFF $<
diff --git a/doc/changelog/08-tools/11280-bugfix-11195-vos-vio-interaction.rst b/doc/changelog/08-tools/11280-bugfix-11195-vos-vio-interaction.rst
new file mode 100644
index 0000000000..97f456036d
--- /dev/null
+++ b/doc/changelog/08-tools/11280-bugfix-11195-vos-vio-interaction.rst
@@ -0,0 +1,4 @@
+- **Deprecated:**
+  The ``-quick`` command is renamed to ``-vio``, for consistency with the new ``-vos`` and ``-vok`` flags. Usage of ``-quick`` is now deprecated.
+  (`#11280 <https://github.com/coq/coq/pull/11280>`_,
+  by charguer).
diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst
index 35729d852d..7a50748c51 100644
--- a/doc/sphinx/addendum/parallel-proof-processing.rst
+++ b/doc/sphinx/addendum/parallel-proof-processing.rst
@@ -154,6 +154,18 @@ to a worker process. The threshold can be configured with
 Batch mode
 ---------------
 
+   .. warning::
+
+      The ``-vio`` flag is subsumed, for most practical usage, by the
+      the more recent ``-vos`` flag. See :ref:`compiled-interfaces`.
+
+   .. warning::
+
+      When working with ``.vio`` files, do not use the ``-vos`` option at
+      the same time, otherwise stale files might get loaded when executing
+      a ``Require``. Indeed, the loading of a nonempty ``.vos`` file is
+      assigned higher priority than the loading of a ``.vio`` file.
+
 When |Coq| is used as a batch compiler by running ``coqc``, it produces
 a ``.vo`` file for each ``.v`` file. A ``.vo`` file contains, among other
 things, theorem statements and proofs. Hence to produce a .vo |Coq|
@@ -161,10 +173,10 @@ need to process all the proofs of the ``.v`` file.
 
 The asynchronous processing of proofs can decouple the generation of a
 compiled file (like the ``.vo`` one) that can be loaded by ``Require`` from the
-generation and checking of the proof objects. The ``-quick`` flag can be
+generation and checking of the proof objects. The ``-vio`` flag can be
 passed to ``coqc`` to produce, quickly, ``.vio`` files.
 Alternatively, when using a Makefile produced by ``coq_makefile``,
-the ``quick`` target can be used to compile all files using the ``-quick`` flag.
+the ``vio`` target can be used to compile all files using the ``-vio`` flag.
 
 A ``.vio`` file can be loaded using ``Require`` exactly as a ``.vo`` file but
 proofs will not be available (the Print command produces an error).
@@ -173,7 +185,7 @@ inconsistencies might go unnoticed. A ``.vio`` file does not contain proof
 objects, but proof tasks, i.e. what a worker process can transform
 into a proof object.
 
-Compiling a set of files with the ``-quick`` flag allows one to work,
+Compiling a set of files with the ``-vio`` flag allows one to work,
 interactively, on any file without waiting for all the proofs to be
 checked.
 
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index d4a61425e1..ba43128bdc 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -253,6 +253,7 @@ and ``coqtop``, unless stated otherwise:
 :-h, --help: Print a short usage and exit.
 
 
+.. _compiled-interfaces:
 
 Compiled interfaces (produced using ``-vos``)
 ----------------------------------------------
diff --git a/lib/future.ml b/lib/future.ml
index d3ea538549..5cccd2038d 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -12,13 +12,13 @@ let not_ready_msg = ref (fun name ->
       Pp.strbrk("The value you are asking for ("^name^") is not ready yet. "^
                 "Please wait or pass "^
                 "the \"-async-proofs off\" option to CoqIDE to disable "^
-                "asynchronous script processing and don't pass \"-quick\" to "^
+                "asynchronous script processing and don't pass \"-vio\" to "^
                 "coqc."))
 let not_here_msg = ref (fun name ->
       Pp.strbrk("The value you are asking for ("^name^") is not available "^
                 "in this process. If you really need this, pass "^
                 "the \"-async-proofs off\" option to CoqIDE to disable "^
-                "asynchronous script processing and don't pass \"-quick\" to "^
+                "asynchronous script processing and don't pass \"-vio\" to "^
                 "coqc."))
 
 let customize_not_ready_msg f = not_ready_msg := f
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 1d21b4b5e0..265c2eafa7 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -643,7 +643,7 @@ vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v))
 %.vio.log:%.v
 	@echo "TEST      $<"
 	$(HIDE){ \
-	  $(coqc) -quick -R vio vio $* 2>&1 && \
+	  $(coqc) -vio -R vio vio $* 2>&1 && \
 	  $(coqc) -R vio vio -vio2vo $*.vio 2>&1 && \
 	  $(coqchk) -R vio vio -norec $(subst /,.,$*) 2>&1; \
 	  if [ $$? = 0 ]; then \
diff --git a/test-suite/misc/quick-include.sh b/test-suite/misc/quick-include.sh
index 96bdee2fc2..e60fb48bca 100755
--- a/test-suite/misc/quick-include.sh
+++ b/test-suite/misc/quick-include.sh
@@ -1,5 +1,5 @@
 #!/bin/sh
 set -e
 
-$coqc -R misc/quick-include/ QuickInclude -quick misc/quick-include/file1.v
-$coqc -R misc/quick-include/ QuickInclude -quick misc/quick-include/file2.v
+$coqc -R misc/quick-include/ QuickInclude -vio misc/quick-include/file1.v
+$coqc -R misc/quick-include/ QuickInclude -vio misc/quick-include/file2.v
diff --git a/test-suite/output/ErrorInModule.v b/test-suite/output/ErrorInModule.v
index b2e3c3e923..fbb3c6bdab 100644
--- a/test-suite/output/ErrorInModule.v
+++ b/test-suite/output/ErrorInModule.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-quick") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-vio") -*- *)
 Module M.
   Definition foo := nonexistent.
 End M.
diff --git a/test-suite/output/ErrorInSection.v b/test-suite/output/ErrorInSection.v
index 505c5ce378..a961330b81 100644
--- a/test-suite/output/ErrorInSection.v
+++ b/test-suite/output/ErrorInSection.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-quick") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-vio") -*- *)
 Section S.
   Definition foo := nonexistent.
 End S.
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 7cd5962d86..d3ed5e78b4 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -389,7 +389,11 @@ optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES))
 .PHONY: optfiles
 
 # FIXME, see Ralf's bugreport
-quick: $(VOFILES:.vo=.vio)
+# quick is deprecated, now renamed vio
+vio: $(VOFILES:.vo=.vio)
+.PHONY: vio
+quick: vio
+	$(warning "'make quick' is deprecated, use 'make vio' or consider using 'vos' files")
 .PHONY: quick
 
 vio2vo:
@@ -397,8 +401,9 @@ vio2vo:
 		-schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
 .PHONY: vio2vo
 
+# quick2vo is undocumented
 quick2vo:
-	$(HIDE)make -j $(J) quick
+	$(HIDE)make -j $(J) vio
 	$(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \
 	  viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \
 	  if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \
@@ -677,8 +682,8 @@ $(GLOBFILES): %.glob: %.v
 	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
 
 $(VFILES:.v=.vio): %.vio: %.v
-	$(SHOW)COQC -quick $<
-	$(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
+	$(SHOW)COQC -vio $<
+	$(HIDE)$(TIMER) $(COQC) -vio $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
 
 $(VFILES:.v=.vos): %.vos: %.v
 	$(SHOW)COQC -vos $<
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index 3c198dc600..dceb811d66 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -121,6 +121,10 @@ let compile opts copts ~echo ~f_in ~f_out =
   in
   let long_f_dot_in, long_f_dot_out =
     ensure_exists_with_prefix f_in f_out ext_in ext_out in
+  let dump_empty_vos () =
+    (* Produce an empty .vos file, as a way to ensure that a stale .vos can never be loaded *)
+    let long_f_dot_vos = (chop_extension long_f_dot_out) ^ ".vos" in
+    create_empty_file long_f_dot_vos in
   match mode with
   | BuildVo | BuildVok ->
       let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
@@ -145,18 +149,20 @@ let compile opts copts ~echo ~f_in ~f_out =
       let _doc = Stm.join ~doc:state.doc in
       let wall_clock2 = Unix.gettimeofday () in
       check_pending_proofs ();
-      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 ());
+      (* In .vo production, dump a complete .vo file.
+         In .vok production, only dump an empty .vok file. *)
+      if mode = BuildVo
+        then Library.save_library_to ~output_native_objects Library.ProofsTodoNone ldir long_f_dot_out (Global.opaque_tables ())
+        else create_empty_file long_f_dot_out;
       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 and an empty .vok file when producing a .vo in standard mode *)
+      (* In .vo production, dump an empty .vos file to indicate that the .vo should be loaded,
+         and dump an empty .vok file to indicate that proofs are ok. *)
       if mode = BuildVo then begin
-        create_empty_file (long_f_dot_out ^ "s");
+        dump_empty_vos();
         create_empty_file (long_f_dot_out ^ "k");
       end;
-      (* 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 | BuildVos ->
@@ -186,15 +192,22 @@ let compile opts copts ~echo ~f_in ~f_out =
       let doc = Stm.finish ~doc:state.doc in
       check_pending_proofs ();
       let create_vos = (mode = BuildVos) in
+      (* In .vos production, the output .vos file contains compiled statements.
+         In .vio production, the output .vio file contains compiled statements and suspended proofs. *)
       let () = ignore (Stm.snapshot_vio ~create_vos ~doc ~output_native_objects ldir long_f_dot_out) in
-      Stm.reset_task_queue ()
+      Stm.reset_task_queue ();
+      (* In .vio production, dump an empty .vos file to indicate that the .vio should be loaded. *)
+      if mode = BuildVio then dump_empty_vos()
 
   | Vio2Vo ->
 
       let sum, lib, univs, tasks, 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
+      Library.save_library_raw long_f_dot_out sum lib univs proofs;
+      (* Like in direct .vo production, dump an empty .vok file and an empty .vos file. *)
+      dump_empty_vos();
+      create_empty_file (long_f_dot_out ^ "k")
 
 let compile opts copts ~echo ~f_in ~f_out =
   ignore(CoqworkmgrApi.get 1);
diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml
index 178aa362c0..0c15f66c07 100644
--- a/toplevel/coqc.ml
+++ b/toplevel/coqc.ml
@@ -25,7 +25,6 @@ let coqc_specific_usage = Usage.{
 coqc specific options:\
 \n  -o f.vo                use f.vo as the output file name\
 \n  -verbose               compile and output the input file\
-\n  -quick                 quickly compile .v files to .vio files (skip proofs)\
 \n  -schedule-vio2vo j f1..fn   run up to j instances of Coq to turn each fi.vio\
 \n                         into fi.vo\
 \n  -schedule-vio-checking j f1..fn   run up to j instances of Coq to check all\
@@ -33,8 +32,10 @@ coqc specific options:\
 \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  -vio                   process statements and suspend opaque proofs, and produce a .vio file\
 \n\
 \nUndocumented:\
+\n  -quick                 (deprecated) alias for -vio\
 \n  -vio2vo                [see manual]\
 \n  -check-vio-tasks       [see manual]\
 \n"
diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml
index e614d4fe6d..0c20563d07 100644
--- a/toplevel/coqcargs.ml
+++ b/toplevel/coqcargs.ml
@@ -98,7 +98,7 @@ let set_compilation_mode opts mode =
   match opts.compilation_mode with
   | BuildVo -> { opts with compilation_mode = mode }
   | mode' when mode <> mode' ->
-    prerr_endline "Options -quick and -vio2vo are exclusive";
+    prerr_endline "Options -vio and -vio2vo are exclusive";
     exit 1
   | _ -> opts
 
@@ -126,6 +126,11 @@ let warn_deprecated_outputstate =
          (fun () ->
           Pp.strbrk "The outputstate option is deprecated and discouraged.")
 
+let warn_deprecated_quick =
+  CWarnings.create ~name:"deprecated-quick" ~category:"deprecated"
+         (fun () ->
+          Pp.strbrk "The -quick option is renamed -vio. Please consider using the -vos feature instead.")
+
 let set_outputstate opts s =
   warn_deprecated_outputstate ();
   { opts with outputstate = Some s }
@@ -165,6 +170,9 @@ let parse arglist : t =
         | "-o" ->
           { oval with compilation_output_name = Some (next ()) }
         | "-quick" ->
+          warn_deprecated_quick();
+          set_compilation_mode oval BuildVio
+        | "-vio" ->
           set_compilation_mode oval BuildVio
         |"-vos" ->
           Flags.load_vos_libraries := true;
diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml
index a8462e31e1..506b3bc505 100644
--- a/vernac/loadpath.ml
+++ b/vernac/loadpath.ml
@@ -138,27 +138,31 @@ 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]
+        and the .vos file exists
+        and this file is not empty
+     Then load this library
+     Else load the most recent between the .vo file and the .vio file,
+          or if there is only of the two files, take this one,
+          or raise an error if both are missing. *)
+  let load_most_recent_of_vo_and_vio () =
+    match find ".vo", find ".vio" with
+    | None, None ->
+      Error LibNotFound
+    | Some res, None | None, Some res ->
+      Ok res
+    | Some (_, vo), Some (_, vi as resvi)
+      when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
+      warn_several_object_files (vi, vo);
+      Ok resvi
+    | Some resvo, Some _ ->
+      Ok resvo
+    in
   if !Flags.load_vos_libraries then begin
-    (* If the .vos file exists and is not empty, it describes the library.
-       Otherwise, load the .vo file, or fail if is missing. *)
     match find ".vos" with
     | Some (_, vos as resvos) when (Unix.stat vos).Unix.st_size > 0 -> Ok resvos
-    | _ ->
-        match find ".vo" with
-        | None -> Error LibNotFound
-        | Some resvo -> Ok resvo
-  end else
-  match find ".vo", find ".vio" with
-  | None, None ->
-    Error LibNotFound
-  | Some res, None | None, Some res ->
-    Ok res
-  | Some (_, vo), Some (_, vi as resvi)
-    when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
-    warn_several_object_files (vi, vo);
-    Ok resvi
-  | Some resvo, Some _ ->
-    Ok resvo
+    | _ -> load_most_recent_of_vo_and_vio()
+  end else load_most_recent_of_vo_and_vio()
 
 let locate_absolute_library dir : CUnix.physical_path locate_result =
   (* Search in loadpath *)