From 565a30614c6df16466f66cac1e517f9202612709 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 17 Feb 2019 01:03:12 +0100 Subject: [azure] [ci] Build on Windows using Dune. We may want to keep the make-based and Dune job, however the make-based setup is tested by the INRIA workers so it may not be needed. In order for some test to run well, we always run in Dune with an absolute path. The easiest way to get a portable absolute path is to use OCaml itself so we introduce a small executable to do that. While we are at it, we do some cleanup of the test-suite `dune` file, in particular we remove useless comments, set `--no-buffer` so results can be seen in real time, and recognize the `NJOBS` variable as we have moved to a Dune version that supports env vars. --- test-suite/Makefile | 32 +++++++++++++----------- test-suite/dune | 65 +++++++++++-------------------------------------- test-suite/ocaml_pwd.ml | 7 ++++++ 3 files changed, 39 insertions(+), 65 deletions(-) create mode 100644 test-suite/ocaml_pwd.ml (limited to 'test-suite') diff --git a/test-suite/Makefile b/test-suite/Makefile index 03bfc5ffac..5582503d89 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -34,20 +34,24 @@ include ../Makefile.common # Default value when called from a freshly compiled Coq, but can be # easily overridden -LIB := .. + BIN := $(shell cd ..; pwd)/bin/ COQFLAGS?= -coqc_boot := $(BIN)coqc -coqlib $(LIB) -boot -q -test-mode -R prerequisite TestSuite $(COQFLAGS) -coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite $(COQFLAGS) -coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite +ifeq ($(COQLIB),) + # This method of setting `pwd` won't work on win32 OCaml + COQLIB := $(shell cd ..; pwd) +endif +export COQLIB + +coqc := $(BIN)coqc -q -R prerequisite TestSuite $(COQFLAGS) +coqchk := $(BIN)coqchk -R prerequisite TestSuite coqdoc := $(BIN)coqdoc -coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -test-mode -R prerequisite TestSuite -coqtopbyte := $(BIN)coqtop.byte +coqtop := $(BIN)coqtop -q -test-mode -R prerequisite TestSuite +coqtopbyte := $(BIN)coqtop.byte -q -coqc_interactive := $(coqc) -async-proofs-cache force -coqc_boot_interactive := $(coqc_boot) -async-proofs-cache force -coqdep := $(BIN)coqdep -coqlib $(LIB) +coqc_interactive := $(coqc) -test-mode -async-proofs-cache force +coqdep := $(BIN)coqdep VERBOSE?= SHOW := $(if $(VERBOSE),@true,@echo) @@ -398,7 +402,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) $(HIDE){ \ echo $(call log_intro,$<); \ output=$*.out.real; \ - $(coqc_boot_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 \ + $(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 \ | grep -v "Welcome to Coq" \ | grep -v "\[Loading ML file" \ | grep -v "Skipping rcfile loading" \ @@ -437,7 +441,7 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out echo $(call log_intro,$<); \ tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \ tmpexpected=`mktemp /tmp/coqcheck.XXXXXX`; \ - $(coqc_boot_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 \ + $(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 \ | grep -v "Welcome to Coq" \ | grep -v "\[Loading ML file" \ | grep -v "Skipping rcfile loading" \ @@ -492,7 +496,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG) $(HIDE){ \ echo $(call log_intro,$<); \ true "extract effective user time"; \ - res=`$(coqc_boot_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`; \ + res=`$(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`; \ R=$$?; times; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ @@ -556,7 +560,7 @@ $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG) echo $(call log_intro,$<); \ export BIN="$(BIN)"; \ export coqc="$(coqc)"; \ - export coqtop="$(coqc_boot)"; \ + export coqtop="$(coqc)"; \ export coqdep="$(coqdep)"; \ export coqtopbyte="$(coqtopbyte)"; \ "$<" 2>&1; R=$$?; times; \ @@ -578,7 +582,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake)) @echo "TEST $<" $(HIDE){ \ echo $(call log_intro,$<); \ - $(BIN)fake_ide $< "-coqlib $(LIB) -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off $(call get_coq_prog_args,"$<")" 2>&1; \ + $(BIN)fake_ide "$<" "-q -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off $(call get_coq_prog_args,"$<")" 2>&1; \ if [ $$? = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ diff --git a/test-suite/dune b/test-suite/dune index eae072553a..9efc1e2dc1 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -1,3 +1,13 @@ +; The easiest way to generate a portable absolute path is to use OCaml +; itself to print it +(executable + (name ocaml_pwd) + (modules ocaml_pwd)) + +(rule + (targets libpath.inc) + (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe ../../install/%{context_name}/lib/coq/ )))) + (rule (targets summary.log) (deps @@ -14,60 +24,13 @@ ; For fake_ide (package coqide-server) (source_tree .)) - ; Finer-grained dependencies look like this + ; Finer-grained dependencies would look like this and be generated + ; by coqdep; that would allow tests to be run incrementally. ; ../tools/CoqMakefile.in ; ../theories/Init/Prelude.vo - ; ../theories/Arith/Arith.vo - ; ../theories/Arith/Compare.vo - ; ../theories/PArith/PArith.vo - ; ../theories/QArith/QArith.vo - ; ../theories/QArith/Qcanon.vo - ; ../theories/ZArith/ZArith.vo - ; ../theories/ZArith/Zwf.vo - ; ../theories/Sets/Ensembles.vo - ; ../theories/Numbers/Natural/Peano/NPeano.vo - ; ../theories/Numbers/Cyclic/Int31/Cyclic31.vo - ; ../theories/FSets/FMaps.vo - ; ../theories/FSets/FSets.vo - ; ../theories/MSets/MSets.vo - ; ../theories/Compat/Coq87.vo - ; ../theories/Compat/Coq88.vo - ; ../theories/Relations/Relations.vo - ; ../theories/Unicode/Utf8.vo - ; ../theories/Program/Program.vo - ; ../theories/Classes/EquivDec.vo - ; ../theories/Classes/DecidableClass.vo - ; ../theories/Classes/SetoidClass.vo - ; ../theories/Classes/RelationClasses.vo - ; ../theories/Logic/Classical.vo - ; ../theories/Logic/Hurkens.vo - ; ../theories/Logic/ClassicalFacts.vo - ; ../theories/Reals/Reals.vo - ; ../theories/Lists/Streams.vo - ; ../plugins/micromega/Lia.vo - ; ../plugins/micromega/Lqa.vo - ; ../plugins/micromega/Psatz.vo - ; ../plugins/micromega/MExtraction.vo - ; ../plugins/nsatz/Nsatz.vo - ; ../plugins/omega/Omega.vo - ; ../plugins/ssr/ssrbool.vo - ; ../plugins/derive/Derive.vo - ; ../plugins/funind/Recdef.vo - ; ../plugins/extraction/Extraction.vo - ; ../plugins/extraction/ExtrOcamlNatInt.vo - ; coqtop - ; coqtop.opt - ; coqidetop.opt - ; coqqueryworker.opt - ; coqtacticworker.opt - ; coqproofworker.opt - ; coqc - ; coqchk - ; coqdoc + ; %{bin:coqc} ; %{bin:coq_makefile} ; %{bin:fake_ide} (action (progn - ; XXX: we will allow to set the NJOBS variable in a future Dune - ; version, either by using an env var or by letting Dune set `-j` - (run make -j 2 BIN= PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests})))) + (bash "make -j %{env:NJOBS=2} BIN= COQLIB=%{read:libpath.inc} PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests}")))) diff --git a/test-suite/ocaml_pwd.ml b/test-suite/ocaml_pwd.ml new file mode 100644 index 0000000000..10ca52a4a9 --- /dev/null +++ b/test-suite/ocaml_pwd.ml @@ -0,0 +1,7 @@ +let _ = + let ch_dir = Sys.argv.(1) in + Sys.chdir ch_dir; + let dir = Sys.getcwd () in + (* Needed for windows *) + let dir = Filename.quote dir in + Format.printf "%s%!" dir -- cgit v1.2.3