diff options
| -rw-r--r-- | .travis.yml | 30 | ||||
| -rw-r--r-- | 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" @@ -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)) |