aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.travis.yml79
-rw-r--r--Makefile9
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
diff --git a/Makefile b/Makefile
index d66412588..c9a94ce59 100644
--- a/Makefile
+++ b/Makefile
@@ -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)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-09 11:24:26 +0000