From 7676ac43b762eab1606e6dfd0693f16239489263 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Mon, 23 Oct 2017 01:54:20 -0400
Subject: Add nonautogenerated-specific{,-display} targets

---
 Makefile           | 7 ++++++-
 etc/ci/smithers.sh | 1 +
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index a281ea213..fac405d08 100644
--- a/Makefile
+++ b/Makefile
@@ -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
-- 
cgit v1.2.3