From 5bf25dfce23da1cee04b1c886e026f0dbc902c9c Mon Sep 17 00:00:00 2001
From: charguer
Date: Fri, 8 Nov 2019 11:06:10 +0100
Subject: From CoqIDE or -vos or -vok compilation, load .vo when .vos is
 missing (fixing bug #11057). With this new behavior, it is not needed to .vos
 files in user contribs. Also, this commit adds a feature: upon creation of a
 .vo file, an empty .vok file is touched.

---
 toplevel/ccompile.ml  | 7 +++++--
 toplevel/coqcargs.mli | 2 +-
 2 files changed, 6 insertions(+), 3 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index 3cbbf3d186..3c198dc600 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -150,8 +150,11 @@ let compile opts copts ~echo ~f_in ~f_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 when producing a .vo in standard mode *)
-      if mode = BuildVo then create_empty_file (long_f_dot_out ^ "s");
+      (* Produce an empty .vos file and an empty .vok file when producing a .vo in standard mode *)
+      if mode = BuildVo then begin
+        create_empty_file (long_f_dot_out ^ "s");
+        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 ()
diff --git a/toplevel/coqcargs.mli b/toplevel/coqcargs.mli
index 677a3f2e48..18c51f4229 100644
--- a/toplevel/coqcargs.mli
+++ b/toplevel/coqcargs.mli
@@ -10,7 +10,7 @@
 
 (** Compilation modes:
   - BuildVo      : process statements and proofs (standard compilation),
-                   and also output an empty .vos file
+                   and also output an empty .vos file and .vok file
   - BuildVio     : process statements, delay proofs in futures
   - Vio2Vo       : load delayed proofs and process them
   - BuildVos     : process statements, and discard proofs,
-- 
cgit v1.2.3