Merge PR #9326: [ci] compile with -quick & validate after vio2vo

Reviewed-by: ejgallego
Ack-by: SkySkimmer
Ack-by: gares
Ack-by: ppedrot

9 files changed, 64 insertions, 16 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 50b86b3c5d..e981c592a2 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -245,6 +245,12 @@ build:base+async:
     COQ_EXTRA_CONF: "-native-compiler yes -coqide opt"
     COQUSERFLAGS: "-async-proofs on"
 
+build:quick:
+  <<: *build-template
+  variables:
+    COQ_EXTRA_CONF: "-native-compiler no"
+    QUICK: "1"
+
 windows64:
   <<: *windows-template
   variables:
@@ -461,6 +467,11 @@ validate:edge+flambda:
     OPAM_SWITCH: edge
     OPAM_VARIANT: "+flambda"
 
+validate:quick:
+  <<: *validate-template
+  dependencies:
+    - build:quick
+
 # Libraries are by convention the projects that depend on Coq
 # but not on its ML API
 
diff --git a/Makefile b/Makefile
index f83f15e888..99d4611dce 100644
--- a/Makefile
+++ b/Makefile
@@ -269,7 +269,7 @@ cleanconfig:
 distclean: clean cleanconfig cacheclean timingclean
 
 voclean:
-	find theories plugins test-suite \( -name '*.vo' -o -name '*.glob' -o -name "*.cmxs" \
+	find theories plugins test-suite \( -name '*.vo' -o -name '*.vio' -o -name '*.glob' -o -name "*.cmxs" \
 	-o -name "*.native" -o -name "*.cmx" -o -name "*.cmi" -o -name "*.o" \) -exec rm -f {} +
 	find theories plugins test-suite -name .coq-native -empty -exec rm -rf {} +
 
diff --git a/Makefile.build b/Makefile.build
index 34d7ce42f7..e683a6bda8 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -57,6 +57,9 @@ TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line
 BEFORE ?=
 AFTER ?=
 
+# Number of parallel jobs for -schedule-vio2vo
+NJOBS ?= 2
+
 ###########################################################################
 # Default starting rule
 ###########################################################################
@@ -543,7 +546,7 @@ $(CSDPCERTBYTE): $(CSDPCERTCMO)
 
 VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m
 
-validate: $(CHICKEN) | $(ALLVO)
+validate: $(CHICKEN) | $(ALLVO:.$(VO)=.vo)
 	$(SHOW)'COQCHK <theories & plugins>'
 	$(HIDE)$(CHICKEN) -boot $(VALIDOPTS) $(ALLMODS)
 
@@ -779,13 +782,19 @@ $(PLUGMLLIBDFILE).d: $(D_DEPEND_BEFORE_SRC) $(filter plugins/%, $(MLLIBFILES) $(
 # since they are all mentioned in at least one Declare ML Module in some .v
 
 coqlib: theories plugins
+ifdef QUICK
+	$(SHOW)'COQC -schedule-vio2vo $(NJOBS) theories/**.vio plugins/**.vio'
+	$(HIDE)$(BOOTCOQC:-compile=-schedule-vio2vo) $(NJOBS) \
+		$(THEORIESVO) $(PLUGINSVO)
+endif
+
 coqlib.timing.diff: theories.timing.diff plugins.timing.diff
 
 theories: $(THEORIESVO)
 plugins: $(PLUGINSVO)
 
-theories.timing.diff: $(THEORIESVO:.vo=.v.timing.diff)
-plugins.timing.diff: $(PLUGINSVO:.vo=.v.timing.diff)
+theories.timing.diff: $(THEORIESVO:.$(VO)=.v.timing.diff)
+plugins.timing.diff: $(PLUGINSVO:.$(VO)=.v.timing.diff)
 
 .PHONY: coqlib theories plugins coqlib.timing.diff theories.timing.diff plugins.timing.diff
 
@@ -802,6 +811,10 @@ theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP)
 	$(HIDE)rm -f theories/Init/$*.glob
 	$(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq $(TIMING_ARG) $(TIMING_EXTRA)
 
+theories/Init/%.vio: theories/Init/%.v $(VO_TOOLS_DEP)
+	$(SHOW)'COQC -quick -noinit $<'
+	$(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq -quick -noglob
+
 # The general rule for building .vo files :
 
 %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP)
@@ -814,6 +827,10 @@ ifdef VALIDATE
 	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
 endif
 
+%.vio: %.v theories/Init/Prelude.vio $(VO_TOOLS_DEP)
+	$(SHOW)'COQC -quick $<'
+	$(HIDE)$(BOOTCOQC) $< -quick -noglob
+
 %.v.timing.diff: %.v.before-timing %.v.after-timing
 	$(SHOW)PYTHON TIMING-DIFF $<
 	$(HIDE)$(MAKE) --no-print-directory print-pretty-single-time-diff BEFORE=$*.v.before-timing AFTER=$*.v.after-timing TIME_OF_PRETTY_BUILD_FILE="$@"
diff --git a/Makefile.dev b/Makefile.dev
index 9659f602d7..13b85dfad4 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -63,7 +63,7 @@ revision:
 
 coqlight: theories-light tools coqbinaries
 
-states: theories/Init/Prelude.vo
+states: theories/Init/Prelude.$(VO)
 
 miniopt: $(COQTOPEXE) pluginsopt
 minibyte: $(COQTOPBYTE) pluginsbyte
diff --git a/Makefile.doc b/Makefile.doc
index 48cdcebddb..7ac710b8c9 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -141,7 +141,7 @@ else
 doc/stdlib/Library.coqdoc.tex: | $(COQDOC) $(THEORIESLIGHTVO)
 endif
 	$(COQDOC) -q -boot --gallina --body-only --latex --stdout \
-            -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@
+            -R theories Coq $(THEORIESLIGHTVO:.$(VO)=.v) >> $@
 
 doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.tex
 	(cd doc/stdlib;\
diff --git a/Makefile.ide b/Makefile.ide
index cae77ee348..23ce83d263 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -70,7 +70,7 @@ SOURCEVIEWSHARE=$(shell pkg-config --variable=prefix gtksourceview-2.0)/share
 .PHONY: ide-toploop ide-byteloop ide-optloop
 
 # target to build CoqIde (native version) and the stuff needed to lauch it
-coqide: coqide-files coqide-opt theories/Init/Prelude.vo
+coqide: coqide-files coqide-opt theories/Init/Prelude.$(VO)
 
 # target to build CoqIde (in native and byte versions), and no more
 # NB: this target is used in the opam package coq-coqide
diff --git a/Makefile.vofiles b/Makefile.vofiles
index d0ae317335..d5217ef4b7 100644
--- a/Makefile.vofiles
+++ b/Makefile.vofiles
@@ -2,14 +2,20 @@
 # This file calls [find] and as such is not suitable for inclusion in
 # the test suite Makefile, unlike Makefile.common.
 
+ifdef QUICK
+VO=vio
+else
+VO=vo
+endif
+
 ###########################################################################
 # vo files
 ###########################################################################
 
-THEORIESVO := $(patsubst %.v,%.vo,$(shell find theories -type f -name "*.v"))
-PLUGINSVO := $(patsubst %.v,%.vo,$(shell find plugins -type f -name "*.v"))
+THEORIESVO := $(patsubst %.v,%.$(VO),$(shell find theories -type f -name "*.v"))
+PLUGINSVO := $(patsubst %.v,%.$(VO),$(shell find plugins -type f -name "*.v"))
 ALLVO := $(THEORIESVO) $(PLUGINSVO)
-VFILES := $(ALLVO:.vo=.v)
+VFILES := $(ALLVO:.$(VO)=.v)
 
 ## More specific targets
 
@@ -20,22 +26,27 @@ THEORIESLIGHTVO:= \
 # remove .vo, replace theories and plugins by Coq, and replace slashes by dots
 vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=))))
 
-ALLMODS:=$(call vo_to_mod,$(ALLVO))
+ALLMODS:=$(call vo_to_mod,$(ALLVO:.$(VO)=.vo))
 
 
 # Converting a stdlib filename into native compiler filenames
 # Used for install targets
-vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.cm*)))))
+vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.cm*)))))
 
-vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.o)))))
+vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.o)))))
+
+ifdef QUICK
+GLOBFILES:=
+else
+GLOBFILES:=$(ALLVO:.$(VO)=.glob)
+endif
 
-GLOBFILES:=$(ALLVO:.vo=.glob)
 ifdef NATIVECOMPUTE
 NATIVEFILES := $(call vo_to_cm,$(ALLVO)) $(call vo_to_obj,$(ALLVO))
 else
 NATIVEFILES :=
 endif
-LIBFILES:=$(ALLVO) $(NATIVEFILES) $(VFILES) $(GLOBFILES)
+LIBFILES:=$(ALLVO:.$(VO)=.vo) $(NATIVEFILES) $(VFILES) $(GLOBFILES)
 
 # For emacs:
 # Local Variables:
diff --git a/checker/check.ml b/checker/check.ml
index 30437e8bd0..b2930d9535 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -329,7 +329,7 @@ let intern_from_file (dir, f) =
         user_err ~hdr:"intern_from_file"
           (str "The file "++str f++str " contains unfinished tasks");
       if opaque_csts <> None then begin
-       chk_pp (str " (was a vio file) ");
+       Flags.if_verbose chk_pp (str " (was a vio file) ");
       Option.iter (fun (_,_,b) -> if not b then
         user_err ~hdr:"intern_from_file"
           (str "The file "++str f++str " is still a .vio"))
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index 64f19e1fd9..69c1d9bd23 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -95,6 +95,7 @@ let schedule_vio_checking j fs =
     done;
     let pid, ret = Unix.wait () in
     if ret <> Unix.WEXITED 0 then rc := 1;
+    Worker.kill (Pool.find pid !pool);
     pool := Pool.remove pid !pool;
   done;
   exit !rc
@@ -124,6 +125,7 @@ let schedule_vio_compilation j fs =
     | s :: rest -> s :: filter_argv b rest in
   let prog = Sys.argv.(0) in  
   let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in
+  let all_jobs = !jobs in
   let make_job () =
     let f, t = List.hd !jobs in
     jobs := List.tl !jobs;
@@ -137,8 +139,15 @@ let schedule_vio_compilation j fs =
     done;
     let pid, ret = Unix.wait () in
     if ret <> Unix.WEXITED 0 then rc := 1;
+    Worker.kill (Pool.find pid !pool);
     pool := Pool.remove pid !pool;
   done;
+  if !rc = 0 then begin
+    (* set the access and last modification time of all files to the same t
+     * not to confuse make into thinking that some of them are outdated *)
+    let t = Unix.gettimeofday () in
+    List.iter (fun (f,_) -> Unix.utimes (f^".vo") t t) all_jobs;
+  end;
   exit !rc