From 29b2e54016410699c84432147a4b52b45f344b3e Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Thu, 1 Nov 2018 15:25:09 -0400
Subject: Add another early travis stage

This will hopefully take some burden off later travis stages and make
PR #437 easier to merge.
---
 .travis.yml | 30 +++++++++++++++++++++++++-----
 Makefile    |  7 ++++++-
 2 files changed, 31 insertions(+), 6 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index dbdbb8d6f..c7988dc90 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -34,6 +34,7 @@ matrix:
   fast_finish: true
 
 stages:
+  - some-early util
   - printlite lite
   - pre-standalone
   - new-pipeline
@@ -44,24 +45,43 @@ stages:
 
 jobs:
   include:
+    - stage: some-early util
+      env: COQ_VERSION="master" COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-master-daily"
+      allow_failure: true
+      script: CUR=early ./etc/ci/travis.sh some-early util
+    - stage: some-early util
+      env: COQ_VERSION="v8.8"   COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-8.8-daily"
+      allow_failure: true
+      script: CUR=early ./etc/ci/travis.sh some-early util
+    - stage: some-early util
+      env: COQ_VERSION="v8.7"   COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-8.7-daily"
+      allow_failure: true
+      script: CUR=early ./etc/ci/travis.sh some-early util
+    - stage: some-early util
+      env: COQ_VERSION="8.8.0"  COQ_PACKAGE="coq-8.8.0" PPA="ppa:jgross-h/many-coq-versions"
+      script: CUR=early ./etc/ci/travis.sh some-early util
+    - stage: some-early util
+      env: COQ_VERSION="8.7.2"  COQ_PACKAGE="coq-8.7.2" PPA="ppa:jgross-h/many-coq-versions"
+      script: CUR=early ./etc/ci/travis.sh some-early util
+
     - stage: printlite lite
       env: COQ_VERSION="master" COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-master-daily"
       allow_failure: true
-      script: CUR=lite ./etc/ci/travis.sh printlite lite
+      script: PREV=early CUR=lite ./etc/ci/travis.sh printlite lite
     - stage: printlite lite
       env: COQ_VERSION="v8.8"   COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-8.8-daily"
       allow_failure: true
-      script: CUR=lite ./etc/ci/travis.sh printlite lite
+      script: PREV=early CUR=lite ./etc/ci/travis.sh printlite lite
     - stage: printlite lite
       env: COQ_VERSION="v8.7"   COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-8.7-daily"
       allow_failure: true
-      script: CUR=lite ./etc/ci/travis.sh printlite lite
+      script: PREV=early CUR=lite ./etc/ci/travis.sh printlite lite
     - stage: printlite lite
       env: COQ_VERSION="8.8.0"  COQ_PACKAGE="coq-8.8.0" PPA="ppa:jgross-h/many-coq-versions"
-      script: CUR=lite ./etc/ci/travis.sh printlite lite
+      script: PREV=early CUR=lite ./etc/ci/travis.sh printlite lite
     - stage: printlite lite
       env: COQ_VERSION="8.7.2"  COQ_PACKAGE="coq-8.7.2" PPA="ppa:jgross-h/many-coq-versions"
-      script: CUR=lite ./etc/ci/travis.sh printlite lite
+      script: PREV=early CUR=lite ./etc/ci/travis.sh printlite lite
 
     - stage: pre-standalone
       env: COQ_VERSION="master" COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-master-daily"
diff --git a/Makefile b/Makefile
index c62795319..6e9ccbb4d 100644
--- a/Makefile
+++ b/Makefile
@@ -25,7 +25,7 @@ INSTALLDEFAULTROOT := Crypto
 	old-pipeline-lite print-old-pipeline-lite \
 	coq-without-new-pipeline \
 	nobigmem print-nobigmem \
-	util \
+	util some-early \
 	specific-c specific-display display \
 	specific non-specific lite only-heavy printlite lite-display print-lite-display \
 	new-pipeline pre-standalone \
@@ -117,6 +117,10 @@ NEW_PIPELINE_PRE_VOFILES := $(filter $(NEW_PIPELINE_FILTER),$(REGULAR_VOFILES))
 PRE_STANDALONE_PRE_VOFILES := $(filter src/Experiments/NewPipeline/Standalone%.vo,$(REGULAR_VOFILES))
 UTIL_PRE_VOFILES := $(filter bbv/%.vo src/Algebra/%.vo src/Tactics/%.vo src/Util/%.vo,$(REGULAR_VOFILES))
 COQ_WITHOUT_NEW_PIPELINE_VOFILES := $(filter-out $(NEW_PIPELINE_FILTER),$(REGULAR_VOFILES))
+SOME_EARLY_VOFILES := \
+	src/Experiments/NewPipeline/Arithmetic.vo \
+	src/Experiments/NewPipeline/Rewriter.vo \
+	src/Experiments/SimplyTypedArithmetic.vo
 
 SELECTED_PATTERN := \
 	src/Specific/X25519/C64/% \
@@ -206,6 +210,7 @@ specific-c: $(filter-out $(UNMADE_C_FILES),$(SPECIFIC_DISPLAY_VO:Display.vo=.c)
 selected-specific: $(SELECTED_SPECIFIC_VOFILES)
 selected-specific-display: $(SELECTED_SPECIFIC_DISPLAY_VO:.vo=.log)
 selected-c: $(filter-out $(UNMADE_C_FILES),$(SELECTED_SPECIFIC_DISPLAY_VO:Display.vo=.c) $(SELECTED_SPECIFIC_DISPLAY_VO:Display.vo=.h))
+some-early: $(SOME_EARLY_VOFILES)
 nonautogenerated-specific: $(NONAUTOGENERATED_SPECIFIC_VOFILES)
 nonautogenerated-specific-display: $(NONAUTOGENERATED_SPECIFIC_DISPLAY_VO:.vo=.log)
 nonautogenerated-c: $(filter-out $(UNMADE_C_FILES),$(NONAUTOGENERATED_SPECIFIC_DISPLAY_VO:Display.vo=.c) $(NONAUTOGENERATED_SPECIFIC_DISPLAY_VO:Display.vo=.h))
-- 
cgit v1.2.3