diff options
| author | Théo Zimmermann | 2020-05-14 12:50:52 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-14 12:51:07 +0200 |
| commit | efa36e61d6eb5421c3c16d66c6d390268892edf2 (patch) | |
| tree | b9fce2d32359ed28c074a4ebdb6c40ba93d479ed /dev | |
| parent | 26cd7d093822556fc919dc7e27cac0196f564fc2 (diff) | |
| parent | 6f2b88649ec0c1e27befe7bcd2cdbec0ccee95d6 (diff) | |
Fix conflicts with latest master.
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 7 | ||||
| -rwxr-xr-x | dev/ci/ci-sf.sh | 23 | ||||
| -rw-r--r-- | dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh | 6 |
3 files changed, 18 insertions, 18 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index b87a9c0392..5f7d0b5789 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -351,3 +351,10 @@ : "${metacoq_CI_REF:=master}" : "${metacoq_CI_GITURL:=https://github.com/MetaCoq/metacoq}" : "${metacoq_CI_ARCHIVEURL:=${metacoq_CI_GITURL}/archive}" + +######################################################################## +# SF suite +######################################################################## +: "${sf_CI_REF:=master}" +: "${sf_CI_GITURL:=https://github.com/DeepSpec/sf}" +: "${sf_CI_ARCHIVEURL:=${sf_CI_GITURL}/archive}" diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index b9d6215e60..d46e53717f 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -3,22 +3,9 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -CIRCLE_SF_TOKEN=00127070c10f5f09574b050e4f08e924764680d2 +git_download sf -# "latest" is disabled due to lack of build credits upstream, thus artifacts fail -# data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/latest/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -) -data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/1411/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -) - -mkdir -p "${CI_BUILD_DIR}" && cd "${CI_BUILD_DIR}" - -sf_lf_CI_TARURL=$(echo "$data" | jq -rc '.[] | select (.path == "lf.tgz") | .url') -sf_plf_CI_TARURL=$(echo "$data" | jq -rc '.[] | select (.path == "plf.tgz") | .url') -sf_vfa_CI_TARURL=$(echo "$data" | jq -rc '.[] | select (.path == "vfa.tgz") | .url') - -wget -O - "${sf_lf_CI_TARURL}?circle-token=${CIRCLE_SF_TOKEN}" | tar xvz -wget -O - "${sf_plf_CI_TARURL}?circle-token=${CIRCLE_SF_TOKEN}" | tar xvz -wget -O - "${sf_vfa_CI_TARURL}?circle-token=${CIRCLE_SF_TOKEN}" | tar xvz - -( cd lf && make clean && make ) -( cd plf && make clean && make ) -( cd vfa && make clean && make ) +( cd lf-current && make clean && make ) +( cd plf-current && make clean && make ) +( cd vfa-current && make clean && make ) +# ( cd qc-current && make clean && make ) diff --git a/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh b/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh new file mode 100644 index 0000000000..50eaf0b109 --- /dev/null +++ b/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "8808" ] || [ "$CI_BRANCH" = "master+support-binder+term-in-abbrev" ]; then + + elpi_CI_REF=master+adapt-coq8808-syndef-same-expressiveness-notation + elpi_CI_GITURL=https://github.com/herbelin/coq-elpi + +fi |