diff options
| author | Emilio Jesus Gallego Arias | 2018-11-17 02:48:09 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-17 16:51:54 +0100 |
| commit | 360fafb7781ca12e533f7ee55da6a4a4324e2a19 (patch) | |
| tree | e964d5a8a434e49d352ff3522bc34465ddf7ccf2 | |
| parent | e64491ec388b004e9753ca8669a7db4b25268a3b (diff) | |
[ci] Uniformize casing of makefile targets and ci variables.
This is convenient as to have better automation.
| -rw-r--r-- | .gitlab-ci.yml | 6 | ||||
| -rw-r--r-- | Makefile.ci | 6 | ||||
| -rwxr-xr-x | dev/ci/ci-aac-tactics.sh | 8 | ||||
| -rwxr-xr-x | dev/ci/ci-aac_tactics.sh | 8 | ||||
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 40 | ||||
| -rwxr-xr-x | dev/ci/ci-color.sh | 4 | ||||
| -rwxr-xr-x | dev/ci/ci-compcert.sh | 4 | ||||
| -rwxr-xr-x | dev/ci/ci-coq_dpdgraph.sh (renamed from dev/ci/ci-coq-dpdgraph.sh) | 0 | ||||
| -rwxr-xr-x | dev/ci/ci-elpi.sh | 4 | ||||
| -rwxr-xr-x | dev/ci/ci-equations.sh | 4 | ||||
| -rwxr-xr-x | dev/ci/ci-plugin_tutorial.sh (renamed from dev/ci/ci-plugin-tutorial.sh) | 0 | ||||
| -rwxr-xr-x | dev/ci/ci-vst.sh | 4 |
12 files changed, 44 insertions, 44 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 1c5c8efc19..7dda19192d 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -362,7 +362,7 @@ validate:edge+flambda: OPAM_SWITCH: edge OPAM_VARIANT: "+flambda" -ci-aac-tactics: +ci-aac_tactics: <<: *ci-template ci-bedrock2: @@ -378,7 +378,7 @@ ci-color: ci-compcert: <<: *ci-template-flambda -ci-coq-dpdgraph: +ci-coq_dpdgraph: <<: *ci-template ci-coquelicot: @@ -438,7 +438,7 @@ ci-paramcoq: ci-pidetop: <<: *ci-template -ci-plugin-tutorial: +ci-plugin_tutorial: <<: *ci-template ci-quickchick: diff --git a/Makefile.ci b/Makefile.ci index e8fea11bdb..88ea64974a 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -9,12 +9,12 @@ ########################################################################## CI_TARGETS= \ - ci-aac-tactics \ + ci-aac_tactics \ ci-bedrock2 \ ci-bignums \ ci-color \ ci-compcert \ - ci-coq-dpdgraph \ + ci-coq_dpdgraph \ ci-coquelicot \ ci-corn \ ci-cpdt \ @@ -38,7 +38,7 @@ CI_TARGETS= \ ci-mtac2 \ ci-paramcoq \ ci-pidetop \ - ci-plugin-tutorial \ + ci-plugin_tutorial \ ci-quickchick \ ci-sf \ ci-simple-io \ diff --git a/dev/ci/ci-aac-tactics.sh b/dev/ci/ci-aac-tactics.sh deleted file mode 100755 index 896a0ddf66..0000000000 --- a/dev/ci/ci-aac-tactics.sh +++ /dev/null @@ -1,8 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -git_download aactactics - -( cd "${CI_BUILD_DIR}/aactactics" && make && make install ) diff --git a/dev/ci/ci-aac_tactics.sh b/dev/ci/ci-aac_tactics.sh new file mode 100755 index 0000000000..19f1f43746 --- /dev/null +++ b/dev/ci/ci-aac_tactics.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download aac_tactics + +( cd "${CI_BUILD_DIR}/aac_tactics" && make && make install ) diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 3137576207..4d5834eeb6 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -113,16 +113,16 @@ ######################################################################## # CompCert ######################################################################## -: "${CompCert_CI_REF:=master}" -: "${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert}" -: "${CompCert_CI_ARCHIVEURL:=${CompCert_CI_GITURL}/archive}" +: "${compcert_CI_REF:=master}" +: "${compcert_CI_GITURL:=https://github.com/AbsInt/CompCert}" +: "${compcert_CI_ARCHIVEURL:=${compcert_CI_GITURL}/archive}" ######################################################################## # VST ######################################################################## -: "${VST_CI_REF:=master}" -: "${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST}" -: "${VST_CI_ARCHIVEURL:=${VST_CI_GITURL}/archive}" +: "${vst_CI_REF:=master}" +: "${vst_CI_GITURL:=https://github.com/PrincetonUniversity/VST}" +: "${vst_CI_ARCHIVEURL:=${vst_CI_GITURL}/archive}" ######################################################################## # cross-crypto @@ -153,7 +153,7 @@ : "${formal_topology_CI_ARCHIVEURL:=${formal_topology_CI_GITURL}/archive}" ######################################################################## -# coq-dpdgraph +# coq_dpdgraph ######################################################################## : "${coq_dpdgraph_CI_REF:=coq-master}" : "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph}" @@ -162,9 +162,9 @@ ######################################################################## # CoLoR ######################################################################## -: "${CoLoR_CI_REF:=master}" -: "${CoLoR_CI_GITURL:=https://github.com/fblanqui/color}" -: "${CoLoR_CI_ARCHIVEURL:=${CoLoR_CI_GITURL}/archive}" +: "${color_CI_REF:=master}" +: "${color_CI_GITURL:=https://github.com/fblanqui/color}" +: "${color_CI_ARCHIVEURL:=${color_CI_GITURL}/archive}" ######################################################################## # SF @@ -196,16 +196,16 @@ ######################################################################## # Equations ######################################################################## -: "${Equations_CI_REF:=master}" -: "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations}" -: "${Equations_CI_ARCHIVEURL:=${Equations_CI_GITURL}/archive}" +: "${equations_CI_REF:=master}" +: "${equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations}" +: "${equations_CI_ARCHIVEURL:=${equations_CI_GITURL}/archive}" ######################################################################## # Elpi ######################################################################## -: "${Elpi_CI_REF:=coq-master}" -: "${Elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi}" -: "${Elpi_CI_ARCHIVEURL:=${Elpi_CI_GITURL}/archive}" +: "${elpi_CI_REF:=coq-master}" +: "${elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi}" +: "${elpi_CI_ARCHIVEURL:=${elpi_CI_GITURL}/archive}" ######################################################################## # fcsl-pcm @@ -257,11 +257,11 @@ : "${menhirlib_CI_ARCHIVEURL:=${menhirlib_CI_GITURL}/-/archive}" ######################################################################## -# aac-tactics +# aac_tactics ######################################################################## -: "${aactactics_CI_REF:=master}" -: "${aactactics_CI_GITURL:=https://github.com/coq-community/aac-tactics}" -: "${aactactics_CI_ARCHIVEURL:=${aactactics_CI_GITURL}/archive}" +: "${aac_tactics_CI_REF:=master}" +: "${aac_tactics_CI_GITURL:=https://github.com/coq-community/aac-tactics}" +: "${aac_tactics_CI_ARCHIVEURL:=${aac_tactics_CI_GITURL}/archive}" ######################################################################## # paramcoq diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index dc696f69d9..a0094b1006 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download CoLoR +git_download color -( cd "${CI_BUILD_DIR}/CoLoR" && make ) +( cd "${CI_BUILD_DIR}/color" && make ) diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index 01c35ceb4a..59a85e4726 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -3,7 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download CompCert +git_download compcert -( cd "${CI_BUILD_DIR}/CompCert" && \ +( cd "${CI_BUILD_DIR}/compcert" && \ ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq_dpdgraph.sh index 2373ea6c62..2373ea6c62 100755 --- a/dev/ci/ci-coq-dpdgraph.sh +++ b/dev/ci/ci-coq_dpdgraph.sh diff --git a/dev/ci/ci-elpi.sh b/dev/ci/ci-elpi.sh index 9b4a06fd5b..d60bf34ba2 100755 --- a/dev/ci/ci-elpi.sh +++ b/dev/ci/ci-elpi.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download Elpi +git_download elpi -( cd "${CI_BUILD_DIR}/Elpi" && make && make install ) +( cd "${CI_BUILD_DIR}/elpi" && make && make install ) diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh index 998d50faa7..b58a794da2 100755 --- a/dev/ci/ci-equations.sh +++ b/dev/ci/ci-equations.sh @@ -3,7 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download Equations +git_download equations -( cd "${CI_BUILD_DIR}/Equations" && coq_makefile -f _CoqProject -o Makefile && \ +( cd "${CI_BUILD_DIR}/equations" && coq_makefile -f _CoqProject -o Makefile && \ make && make test-suite && make examples && make install) diff --git a/dev/ci/ci-plugin-tutorial.sh b/dev/ci/ci-plugin_tutorial.sh index 6c26a71a21..6c26a71a21 100755 --- a/dev/ci/ci-plugin-tutorial.sh +++ b/dev/ci/ci-plugin_tutorial.sh diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh index 0fec19205a..169d1a41db 100755 --- a/dev/ci/ci-vst.sh +++ b/dev/ci/ci-vst.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download VST +git_download vst -( cd "${CI_BUILD_DIR}/VST" && make IGNORECOQVERSION=true ) +( cd "${CI_BUILD_DIR}/vst" && make IGNORECOQVERSION=true ) |
