Move new-pipeline to its own stage

It's starting to get pretty slow.

2 files changed, 47 insertions, 22 deletions

diff --git a/.travis.yml b/.travis.yml
index 58c9f29fb..1bd349df7 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -35,6 +35,7 @@ matrix:
 
 stages:
   - printlite lite
+  - new-pipeline
   - no-curves-proofs-non-specific
   - curves-proofs
   - selected-specific selected-specific-display
@@ -61,82 +62,98 @@ jobs:
       env: COQ_VERSION="8.7.2"  COQ_PACKAGE="coq-8.7.2" PPA="ppa:jgross-h/many-coq-versions"
       script: CUR=0 ./etc/ci/travis.sh printlite lite
 
+    - stage: new-pipeline
+      env: COQ_VERSION="master" COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-master-daily"
+      script: PREV=0 CUR=1 ./etc/ci/travis.sh new-pipeline
+    - stage: new-pipeline
+      env: COQ_VERSION="v8.8"   COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-8.8-daily"
+      script: PREV=0 CUR=1 ./etc/ci/travis.sh new-pipeline
+    - stage: new-pipeline
+      env: COQ_VERSION="v8.7"   COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-8.7-daily"
+      script: PREV=0 CUR=1 ./etc/ci/travis.sh new-pipeline
+    - stage: new-pipeline
+      env: COQ_VERSION="8.8.0"  COQ_PACKAGE="coq-8.8.0" PPA="ppa:jgross-h/many-coq-versions"
+      script: PREV=0 CUR=1 ./etc/ci/travis.sh new-pipeline
+    - stage: new-pipeline
+      env: COQ_VERSION="8.7.2"  COQ_PACKAGE="coq-8.7.2" PPA="ppa:jgross-h/many-coq-versions"
+      script: PREV=0 CUR=1 ./etc/ci/travis.sh new-pipeline
+
     - stage: no-curves-proofs-non-specific
       env: COQ_VERSION="master" COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-master-daily"
-      script: PREV=0 CUR=1 ./etc/ci/travis.sh no-curves-proofs-non-specific
+      script: PREV=1 CUR=2 ./etc/ci/travis.sh no-curves-proofs-non-specific
     - stage: no-curves-proofs-non-specific
       env: COQ_VERSION="v8.8"   COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-8.8-daily"
-      script: PREV=0 CUR=1 ./etc/ci/travis.sh no-curves-proofs-non-specific
+      script: PREV=1 CUR=2 ./etc/ci/travis.sh no-curves-proofs-non-specific
     - stage: no-curves-proofs-non-specific
       env: COQ_VERSION="v8.7"   COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-8.7-daily"
-      script: PREV=0 CUR=1 ./etc/ci/travis.sh no-curves-proofs-non-specific
+      script: PREV=1 CUR=2 ./etc/ci/travis.sh no-curves-proofs-non-specific
     - stage: no-curves-proofs-non-specific
       env: COQ_VERSION="8.8.0"  COQ_PACKAGE="coq-8.8.0" PPA="ppa:jgross-h/many-coq-versions"
-      script: PREV=0 CUR=1 ./etc/ci/travis.sh no-curves-proofs-non-specific
+      script: PREV=1 CUR=2 ./etc/ci/travis.sh no-curves-proofs-non-specific
     - stage: no-curves-proofs-non-specific
       env: COQ_VERSION="8.7.2"  COQ_PACKAGE="coq-8.7.2" PPA="ppa:jgross-h/many-coq-versions"
-      script: PREV=0 CUR=1 ./etc/ci/travis.sh no-curves-proofs-non-specific
+      script: PREV=1 CUR=2 ./etc/ci/travis.sh no-curves-proofs-non-specific
 
     - stage: curves-proofs
       env: COQ_VERSION="master" COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-master-daily"
       allow_failure: true
-      script: PREV=1 CUR=2 ./etc/ci/travis.sh curves-proofs
+      script: PREV=2 CUR=3 ./etc/ci/travis.sh curves-proofs
     - stage: curves-proofs
       env: COQ_VERSION="v8.8"   COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-8.8-daily"
       allow_failure: true
-      script: PREV=1 CUR=2 ./etc/ci/travis.sh curves-proofs
+      script: PREV=2 CUR=3 ./etc/ci/travis.sh curves-proofs
     - stage: curves-proofs
       env: COQ_VERSION="v8.7"   COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-8.7-daily"
       allow_failure: true
-      script: PREV=1 CUR=2 ./etc/ci/travis.sh curves-proofs
+      script: PREV=2 CUR=3 ./etc/ci/travis.sh curves-proofs
     - stage: curves-proofs
       env: COQ_VERSION="8.8.0"  COQ_PACKAGE="coq-8.8.0" PPA="ppa:jgross-h/many-coq-versions"
-      script: PREV=1 CUR=2 ./etc/ci/travis.sh curves-proofs
+      script: PREV=2 CUR=3 ./etc/ci/travis.sh curves-proofs
     - stage: curves-proofs
       env: COQ_VERSION="8.7.2"  COQ_PACKAGE="coq-8.7.2" PPA="ppa:jgross-h/many-coq-versions"
-      script: PREV=1 CUR=2 ./etc/ci/travis.sh curves-proofs
+      script: PREV=2 CUR=3 ./etc/ci/travis.sh curves-proofs
 
     - stage: selected-specific selected-specific-display
       env: COQ_VERSION="master" COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-master-daily"
       allow_failure: true
-      script: PREV=2 CUR=3 ./etc/ci/travis.sh selected-specific selected-specific-display
+      script: PREV=3 CUR=4 ./etc/ci/travis.sh selected-specific selected-specific-display
     - stage: selected-specific selected-specific-display
       env: COQ_VERSION="v8.8"   COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-8.8-daily"
       allow_failure: true
-      script: PREV=2 CUR=3 ./etc/ci/travis.sh selected-specific selected-specific-display
+      script: PREV=3 CUR=4 ./etc/ci/travis.sh selected-specific selected-specific-display
     - stage: selected-specific selected-specific-display
       env: COQ_VERSION="v8.7"   COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-8.7-daily"
       allow_failure: true
-      script: PREV=2 CUR=3 ./etc/ci/travis.sh selected-specific selected-specific-display
+      script: PREV=3 CUR=4 ./etc/ci/travis.sh selected-specific selected-specific-display
     - stage: selected-specific selected-specific-display
       env: COQ_VERSION="8.8.0"  COQ_PACKAGE="coq-8.8.0" PPA="ppa:jgross-h/many-coq-versions"
-      script: PREV=2 CUR=3 ./etc/ci/travis.sh selected-specific selected-specific-display
+      script: PREV=3 CUR=4 ./etc/ci/travis.sh selected-specific selected-specific-display
     - stage: selected-specific selected-specific-display
       env: COQ_VERSION="8.7.2"  COQ_PACKAGE="coq-8.7.2" PPA="ppa:jgross-h/many-coq-versions"
-      script: PREV=2 CUR=3 ./etc/ci/travis.sh selected-specific selected-specific-display
+      script: PREV=3 CUR=4 ./etc/ci/travis.sh selected-specific selected-specific-display
 
     - stage: build-selected-test build-selected-bench
       env: COQ_VERSION="8.8.0"  COQ_PACKAGE="coq-8.8.0" PPA="ppa:jgross-h/many-coq-versions"
-      script: PREV=3 CUR=4 ./etc/ci/travis.sh build-selected-test build-selected-bench
+      script: PREV=4 CUR=5 ./etc/ci/travis.sh build-selected-test build-selected-bench
     - stage: build-selected-test build-selected-bench
       env: COQ_VERSION="8.7.2"  COQ_PACKAGE="coq-8.7.2" PPA="ppa:jgross-h/many-coq-versions"
-      script: PREV=3 CUR=4 ./etc/ci/travis.sh build-selected-test build-selected-bench
+      script: PREV=4 CUR=5 ./etc/ci/travis.sh build-selected-test build-selected-bench
 
     - stage: standalone-ocaml
       env: COQ_VERSION="8.8.0"  COQ_PACKAGE="coq-8.8.0" PPA="ppa:jgross-h/many-coq-versions"
-      script: PREV=4 CUR=5 ./etc/ci/travis.sh standalone-ocaml c-files test-c-files CC=gcc
+      script: PREV=5 CUR=6 ./etc/ci/travis.sh standalone-ocaml c-files test-c-files CC=gcc
     - stage: standalone-ocaml
       env: COQ_VERSION="8.7.2"  COQ_PACKAGE="coq-8.7.2" PPA="ppa:jgross-h/many-coq-versions"
-      script: PREV=4 CUR=5 ./etc/ci/travis.sh standalone-ocaml c-files test-c-files CC=gcc
+      script: PREV=5 CUR=6 ./etc/ci/travis.sh standalone-ocaml c-files test-c-files CC=gcc
 
 #    - stage: selected-test selected-bench
 #      env: COQ_VERSION="8.8.0"  COQ_PACKAGE="coq-8.8.0" PPA="ppa:jgross-h/many-coq-versions"
 #      allow_failure: true
-#      script: PREV=4 CUR=5 ./etc/ci/travis.sh selected-test selected-bench
+#      script: PREV=6 CUR=7 ./etc/ci/travis.sh selected-test selected-bench
 #    - stage: selected-test selected-bench
 #      env: COQ_VERSION="8.7.2"  COQ_PACKAGE="coq-8.7.2" PPA="ppa:jgross-h/many-coq-versions"
 #      allow_failure: true
-#      script: PREV=4 CUR=5 ./etc/ci/travis.sh selected-test selected-bench
+#      script: PREV=6 CUR=7 ./etc/ci/travis.sh selected-test selected-bench
 
 after_success:
   - kill $PID_KEEP_ALIVE
diff --git a/Makefile b/Makefile
index d239e2d3e..debe39218 100644
--- a/Makefile
+++ b/Makefile
@@ -24,6 +24,7 @@ INSTALLDEFAULTROOT := Crypto
 	nobigmem print-nobigmem \
 	specific-c specific-display display \
 	specific non-specific lite only-heavy printlite lite-display print-lite-display \
+	new-pipeline \
 	curves-proofs no-curves-proofs no-curves-proofs-non-specific \
 	selected-specific selected-specific-display nonautogenerated-specific nonautogenerated-specific-display nonautogenerated-c build-selected-test selected-test build-selected-bench selected-bench selected-c \
 	build-test test build-bench bench c \
@@ -51,7 +52,7 @@ COQ_VERSION := $(firstword $(subst $(COQ_VERSION_PREFIX),,$(shell "$(COQBIN)coqc
 -include Makefile.coq
 endif
 
-ifeq ($(filter curves-proofs no-curves-proofs no-curves-proofs-non-specific selected-specific selected-specific-display lite only-heavy printdeps printreversedeps printlite print-lite-display lite-display nobigmem print-nobigmem,$(MAKECMDGOALS)),)
+ifeq ($(filter curves-proofs no-curves-proofs no-curves-proofs-non-specific selected-specific selected-specific-display lite only-heavy printdeps printreversedeps printlite print-lite-display lite-display nobigmem print-nobigmem new-pipeline,$(MAKECMDGOALS)),)
 -include etc/coq-scripts/Makefile.vo_closure
 else
 include etc/coq-scripts/Makefile.vo_closure
@@ -86,6 +87,7 @@ LITE_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo \
 	src/Specific/NISTP256/AMD128/fe%.vo \
 	src/Specific/X25519/C64/ladderstep.vo \
 	src/Specific/X25519/C32/fe%.vo \
+	src/Experiments/NewPipeline/RewriterProofs.vo \
 	src/Experiments/NewPipeline/Toplevel2.vo \
 	src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo \
 	src/Experiments/SimplyTypedArithmetic.vo \
@@ -101,6 +103,7 @@ NO_CURVES_PROOFS_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo \
 	src/Curves/Weierstrass/Jacobian.vo
 NO_CURVES_PROOFS_NON_SPECIFIC_UNMADE_VOFILES := $(filter $(NO_CURVES_PROOFS_UNMADE_VOFILES) src/Specific/%.vo,$(VOFILES))
 REAL_SPECIFIC_GENERATED_VOFILES := $(filter $(SPECIFIC_GENERATED_VOFILES),$(VOFILES))
+NEW_PIPELINE_PRE_VOFILES := $(filter src/Experiments/NewPipeline/%,$(REGULAR_VOFILES))
 
 SELECTED_PATTERN := \
 	src/Specific/X25519/C64/% \
@@ -150,6 +153,10 @@ endif
 ifneq ($(filter selected-specific,$(MAKECMDGOALS)),)
 SELECTED_SPECIFIC_VOFILES := $(call vo_closure,$(SELECTED_SPECIFIC_PRE_VOFILES))
 endif
+ifneq ($(filter new-pipeline,$(MAKECMDGOALS)),)
+NEW_PIPELINE_VOFILES := $(call vo_closure,$(NEW_PIPELINE_PRE_VOFILES))
+endif
+
 
 specific: $(SPECIFIC_VO)
 non-specific: $(NON_SPECIFIC_VO)
@@ -161,6 +168,7 @@ only-heavy: $(HEAVY_VOFILES)
 curves-proofs: $(CURVES_PROOFS_VOFILES)
 no-curves-proofs: $(NO_CURVES_PROOFS_VOFILES)
 no-curves-proofs-non-specific: $(NO_CURVES_PROOFS_NON_SPECIFIC_VOFILES)
+new-pipeline: $(NEW_PIPELINE_VOFILES)
 specific-display: $(SPECIFIC_DISPLAY_VO:.vo=.log)
 specific-c: $(filter-out $(UNMADE_C_FILES),$(SPECIFIC_DISPLAY_VO:Display.vo=.c) $(SPECIFIC_DISPLAY_VO:Display.vo=.h))
 selected-specific: $(SELECTED_SPECIFIC_VOFILES)