diff options
author | Jason Gross <jagro@google.com> | 2018-08-07 11:25:07 -0400 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2018-08-13 13:12:50 -0400 |
commit | 44d631a07795e971ee24456dca0945de2f1d55e3 (patch) | |
tree | 44888343c4c4827c739d5a8d5ac9ac090fa2b863 | |
parent | ae994ad0304006f1ea2db1b5cbb272e390230735 (diff) |
Split up new-pipeline more
Also change the travis config so that it's easier to insert new stages
without globally renaming everything
-rw-r--r-- | .travis.yml | 79 | ||||
-rw-r--r-- | Makefile | 9 |
2 files changed, 55 insertions, 33 deletions
diff --git a/.travis.yml b/.travis.yml index 1bd349df7..dbdbb8d6f 100644 --- a/.travis.yml +++ b/.travis.yml @@ -35,6 +35,7 @@ matrix: stages: - printlite lite + - pre-standalone - new-pipeline - no-curves-proofs-non-specific - curves-proofs @@ -46,114 +47,130 @@ jobs: - stage: printlite lite env: COQ_VERSION="master" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-master-daily" allow_failure: true - script: CUR=0 ./etc/ci/travis.sh printlite lite + script: 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=0 ./etc/ci/travis.sh printlite lite + script: 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=0 ./etc/ci/travis.sh printlite lite + script: 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=0 ./etc/ci/travis.sh printlite lite + script: 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=0 ./etc/ci/travis.sh printlite lite + script: 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" + script: PREV=lite CUR=pre-standalone ./etc/ci/travis.sh pre-standalone + - stage: pre-standalone + env: COQ_VERSION="v8.8" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-8.8-daily" + script: PREV=lite CUR=pre-standalone ./etc/ci/travis.sh pre-standalone + - stage: pre-standalone + env: COQ_VERSION="v8.7" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-8.7-daily" + script: PREV=lite CUR=pre-standalone ./etc/ci/travis.sh pre-standalone + - stage: pre-standalone + env: COQ_VERSION="8.8.0" COQ_PACKAGE="coq-8.8.0" PPA="ppa:jgross-h/many-coq-versions" + script: PREV=lite CUR=pre-standalone ./etc/ci/travis.sh pre-standalone + - stage: pre-standalone + env: COQ_VERSION="8.7.2" COQ_PACKAGE="coq-8.7.2" PPA="ppa:jgross-h/many-coq-versions" + script: PREV=lite CUR=pre-standalone ./etc/ci/travis.sh pre-standalone - 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 + script: PREV=pre-standalone CUR=new-pipeline ./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 + script: PREV=pre-standalone CUR=new-pipeline ./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 + script: PREV=pre-standalone CUR=new-pipeline ./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 + script: PREV=pre-standalone CUR=new-pipeline ./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 + script: PREV=pre-standalone CUR=new-pipeline ./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=1 CUR=2 ./etc/ci/travis.sh no-curves-proofs-non-specific + script: PREV=new-pipeline CUR=no-curves-proofs-non-specific ./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=1 CUR=2 ./etc/ci/travis.sh no-curves-proofs-non-specific + script: PREV=new-pipeline CUR=no-curves-proofs-non-specific ./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=1 CUR=2 ./etc/ci/travis.sh no-curves-proofs-non-specific + script: PREV=new-pipeline CUR=no-curves-proofs-non-specific ./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=1 CUR=2 ./etc/ci/travis.sh no-curves-proofs-non-specific + script: PREV=new-pipeline CUR=no-curves-proofs-non-specific ./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=1 CUR=2 ./etc/ci/travis.sh no-curves-proofs-non-specific + script: PREV=new-pipeline CUR=no-curves-proofs-non-specific ./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=2 CUR=3 ./etc/ci/travis.sh curves-proofs + script: PREV=no-curves-proofs-non-specific CUR=curves-proofs ./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=2 CUR=3 ./etc/ci/travis.sh curves-proofs + script: PREV=no-curves-proofs-non-specific CUR=curves-proofs ./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=2 CUR=3 ./etc/ci/travis.sh curves-proofs + script: PREV=no-curves-proofs-non-specific CUR=curves-proofs ./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=2 CUR=3 ./etc/ci/travis.sh curves-proofs + script: PREV=no-curves-proofs-non-specific CUR=curves-proofs ./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=2 CUR=3 ./etc/ci/travis.sh curves-proofs + script: PREV=no-curves-proofs-non-specific CUR=curves-proofs ./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=3 CUR=4 ./etc/ci/travis.sh selected-specific selected-specific-display + script: PREV=curves-proofs CUR=selected-specific ./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=3 CUR=4 ./etc/ci/travis.sh selected-specific selected-specific-display + script: PREV=curves-proofs CUR=selected-specific ./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=3 CUR=4 ./etc/ci/travis.sh selected-specific selected-specific-display + script: PREV=curves-proofs CUR=selected-specific ./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=3 CUR=4 ./etc/ci/travis.sh selected-specific selected-specific-display + script: PREV=curves-proofs CUR=selected-specific ./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=3 CUR=4 ./etc/ci/travis.sh selected-specific selected-specific-display + script: PREV=curves-proofs CUR=selected-specific ./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=4 CUR=5 ./etc/ci/travis.sh build-selected-test build-selected-bench + script: PREV=selected-specific CUR=build-selected ./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=4 CUR=5 ./etc/ci/travis.sh build-selected-test build-selected-bench + script: PREV=selected-specific CUR=build-selected ./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=5 CUR=6 ./etc/ci/travis.sh standalone-ocaml c-files test-c-files CC=gcc + script: PREV=build-selected CUR=standalone-ocaml ./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=5 CUR=6 ./etc/ci/travis.sh standalone-ocaml c-files test-c-files CC=gcc + script: PREV=build-selected CUR=standalone-ocaml ./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=6 CUR=7 ./etc/ci/travis.sh selected-test selected-bench +# script: PREV=standalone-ocaml CUR=selected-test-bench ./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=6 CUR=7 ./etc/ci/travis.sh selected-test selected-bench +# script: PREV=standalone-ocaml CUR=selected-test-bench ./etc/ci/travis.sh selected-test selected-bench after_success: - kill $PID_KEEP_ALIVE @@ -24,7 +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 \ + new-pipeline pre-standalone \ 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 \ @@ -52,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 new-pipeline,$(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 pre-standalone,$(MAKECMDGOALS)),) -include etc/coq-scripts/Makefile.vo_closure else include etc/coq-scripts/Makefile.vo_closure @@ -107,6 +107,7 @@ NO_CURVES_PROOFS_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.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)) +PRE_STANDALONE_PRE_VOFILES := $(filter src/Experiments/NewPipeline/Standalone%.vo,$(REGULAR_VOFILES)) SELECTED_PATTERN := \ src/Specific/X25519/C64/% \ @@ -159,6 +160,9 @@ endif ifneq ($(filter new-pipeline,$(MAKECMDGOALS)),) NEW_PIPELINE_VOFILES := $(call vo_closure,$(NEW_PIPELINE_PRE_VOFILES)) endif +ifneq ($(filter pre-standalone,$(MAKECMDGOALS)),) +PRE_STANDALONE_VOFILES := $(call vo_closure,$(PRE_STANDALONE_PRE_VOFILES)) +endif specific: $(SPECIFIC_VO) @@ -172,6 +176,7 @@ 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) +pre-standalone: $(PRE_STANDALONE_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) |