diff options
| -rw-r--r-- | Makefile | 7 | ||||
| -rwxr-xr-x | etc/ci/smithers.sh | 1 |
2 files changed, 7 insertions, 1 deletions
@@ -18,7 +18,7 @@ INSTALLDEFAULTROOT := Crypto specific-c specific-display display \ specific non-specific lite only-heavy printlite \ curves-proofs no-curves-proofs no-curves-proofs-non-specific \ - selected-specific selected-speicifc-display selected-test selected-bench selected-c \ + selected-specific selected-specific-display nonautogenerated-specific nonautogenerated-specific-display nonautogenerated-c selected-test selected-bench selected-c \ test bench c SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g' | uniq @@ -74,8 +74,10 @@ SELECTED_SPECIFIC_PRE_VOFILES := $(filter $(SELECTED_PATTERN),$(REGULAR_VOFILES) COQ_VOFILES := $(filter-out $(SPECIFIC_GENERATED_VOFILES),$(REGULAR_VOFILES)) SPECIFIC_VO := $(filter src/Specific/%,$(REGULAR_VOFILES)) +NONAUTOGENERATED_SPECIFIC_VO := $(filter-out $(SPECIFIC_GENERATED_VOFILES),$(SPECIFIC_VO)) NON_SPECIFIC_VO := $(filter-out $(SPECIFIC_VO),$(REGULAR_VOFILES)) SPECIFIC_DISPLAY_VO := $(filter src/Specific/%Display.vo,$(filter-out $(UNMADE_VOFILES),$(VOFILES))) +NONAUTOGENERATED_SPECIFIC_DISPLAY_VO := $(filter-out $(SPECIFIC_GENERATED_VOFILES),$(SPECIFIC_DISPLAY_VO)) DISPLAY_VO := $(SPECIFIC_DISPLAY_VO) DISPLAY_JAVA_VO := $(filter %JavaDisplay.vo,$(DISPLAY_VO)) DISPLAY_NON_JAVA_VO := $(filter-out $(DISPLAY_JAVA_VO),$(DISPLAY_VO)) @@ -117,6 +119,9 @@ specific-c: $(SPECIFIC_DISPLAY_VO:Display.vo=.c) $(SPECIFIC_DISPLAY_VO:Display.v selected-specific: $(SELECTED_SPECIFIC_VOFILES) coqprime selected-specific-display: $(SELECTED_SPECIFIC_DISPLAY_VO:.vo=.log) coqprime selected-c: $(SELECTED_SPECIFIC_DISPLAY_VO:Display.vo=.c) $(SELECTED_SPECIFIC_DISPLAY_VO:Display.vo=.h) coqprime +nonautogenerated-specific: $(NONAUTOGENERATED_SPECIFIC_VOFILES) coqprime +nonautogenerated-specific-display: $(NONAUTOGENERATED_SPECIFIC_DISPLAY_VO:.vo=.log) coqprime +nonautogenerated-c: $(NONAUTOGENERATED_SPECIFIC_DISPLAY_VO:Display.vo=.c) $(NONAUTOGENERATED_SPECIFIC_DISPLAY_VO:Display.vo=.h) coqprime display: $(DISPLAY_VO:.vo=.log) coqprime printlite:: diff --git a/etc/ci/smithers.sh b/etc/ci/smithers.sh index 3532cc3bc..dafebbda9 100755 --- a/etc/ci/smithers.sh +++ b/etc/ci/smithers.sh @@ -6,6 +6,7 @@ cd "$WORKSPACE" export PATH="/opt/coq-$coq_version/bin${PATH:+:}$PATH" . /opt/bashrc/bashrc export TARGETS="coq display bench test" +export TARGETS="coq nonautogenerated-specific nonautogenerated-specific-display bench test" rm -f BUILD.ok ((/opt/timeout/default-timeout make -j$(nproc) TIMED=1 PROFILE=1 $TARGETS || make STDTIME='/opt/timeout/time-default-timeout-coq -f "$* (real: %e, user: %U, sys: %S, mem: %M ko)"' TIMED=1 PROFILE=1 $TARGETS) && touch BUILD.ok) 2>&1 | tee time-of-build.log python ./etc/coq-scripts/timing/make-one-time-file.py time-of-build.log time-of-build-pretty.log |