Merge PR #15745: toplevel: fix a bug in coqc -vok invocation

Reviewed-by: gares
Reviewed-by: Blaisorblade
Ack-by: SkySkimmer
Ack-by: Alizter
Co-authored-by: gares <[email protected]>

Author: coqbot-app[bot]

doc/changelog/08-cli-tools/15745-coqc-vok.rst

@@ -0,0 +1,4 @@
+- **Fixed:**
+  a bug where :n:`coqc -vok` was not creating an empty '.vok' file.
+  (`#15745 <https://github.com/coq/coq/pull/15745>`_,
+  by Ramkumar Ramachandra).

stm/asyncTaskQueue.ml

@@ -111,7 +111,7 @@ module Make(T : Task) () = struct
                  "-async-proofs-worker-priority";
                  CoqworkmgrApi.(string_of_priority priority)]
         (* Options to discard: 0 arguments *)
-        | ("-emacs" | "--xml_format=Ppcmds" | "-batch") :: tl  ->
+        | ("-emacs" | "--xml_format=Ppcmds" | "-batch" | "-vok" | "-vos") :: tl  ->
           set_slave_opt tl
         (* Options to discard: 1 argument *)
         | ( "-async-proofs" | "-vio2vo" | "-o"

test-suite/misc/coqc_dash_o.v renamed to test-suite/misc/coqc_cmdline.v

@@ -1,12 +1,12 @@
 #!/usr/bin/env bash
 
-DOUT=misc/tmp_coqc_dash_o/
-OUT=${DOUT}coqc_dash_o.vo
+DOUT=misc/tmp_coqc_cmdline/
+OUT=${DOUT}coqc_cmdline.vo
 
 
 mkdir -p "${DOUT}"
 rm -f "${OUT}"
-$coqc misc/coqc_dash_o.v -o "${OUT}"
+$coqc misc/coqc_cmdline.v -o "${OUT}"
 if [ ! -f "${OUT}" ]; then
   printf "coqc -o not working"
   exit 1

test-suite/misc/coqc_dash_o.sh

@@ -0,0 +1,43 @@
+#!/usr/bin/env bash
+
+IN_V=misc/coqc_cmdline.v
+OUT_VO=misc/coqc_cmdline.vo
+OUT_VIO=misc/coqc_cmdline.vio
+OUT_VOS=misc/coqc_cmdline.vos
+OUT_VOK=misc/coqc_cmdline.vok
+OUT_GLOB=misc/coqc_cmdline.glob
+OUT="${OUT_VO} ${OUT_VIO} ${OUT_VOS} ${OUT_VOK} ${OUT_GLOB}"
+
+rm -f ${OUT}
+
+set -x
+
+$coqc ${IN_V} -vos
+$coqc ${IN_V} -vok
+if [ ! -f ${OUT_VOK} ]; then
+  echo "coqc -vok not working in -vos mode"
+  rm -f ${OUT}
+  exit 1
+fi
+
+rm -f ${OUT}
+
+$coqc ${IN_V} -o ${OUT_VO}
+if [ ! -f ${OUT_VOK} ]; then
+  echo "vok not produced in -o mode"
+  rm -f ${OUT}
+  exit 1
+fi
+
+rm -f ${OUT}
+
+$coqc ${IN_V} -vio
+$coqc -vio2vo ${OUT_VIO}
+if [ ! -f ${OUT_VOK} ]; then
+  echo "vok not produced in -vio2vo mode"
+  rm -f ${OUT}
+  exit 1
+fi
+
+rm -f ${OUT}
+exit 0

test-suite/misc/coqc_dash_vok.sh

@@ -122,9 +122,11 @@ let compile opts stm_options injections copts ~echo ~f_in ~f_out =
   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
+  let dump_empty_vok () =
+    let long_f_dot_vok = (chop_extension long_f_dot_out) ^ ".vok" in
+    create_empty_file long_f_dot_vok in
   match mode with
   | BuildVo | BuildVok ->
       let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
@@ -147,19 +149,19 @@ let compile opts stm_options injections copts ~echo ~f_in ~f_out =
       let _doc = Stm.join ~doc:state.doc in
       let wall_clock2 = Unix.gettimeofday () in
       check_pending_proofs long_f_dot_in;
-      (* In .vo production, dump a complete .vo file.
-         In .vok production, only dump an empty .vok file. *)
+      (* In .vo production, dump a complete .vo file. *)
       if mode = BuildVo
         then Library.save_library_to ~output_native_objects Library.ProofsTodoNone ldir 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 ();
-      (* 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
+      (* Additionally, dump an empty .vos file to make sure that
+        stale ones are never loaded *)
+      if mode = BuildVo then
         dump_empty_vos();
-        create_empty_file (long_f_dot_out ^ "k");
-      end;
+      (* In both .vo, and .vok production mode, dump an empty .vok file to
+         indicate that proofs are ok. *)
+      dump_empty_vok();
       Dumpglob.end_dump_glob ()
 
   | BuildVio | BuildVos ->