diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/ci-common.sh | 21 | ||||
| -rw-r--r-- | dev/ci/docker/bionic_coq/Dockerfile | 5 | ||||
| -rw-r--r-- | dev/ci/user-overlays/09439-sep-variance.sh | 14 | ||||
| -rw-r--r-- | dev/include | 2 | ||||
| -rwxr-xr-x | dev/lint-repository.sh | 13 | ||||
| -rw-r--r-- | dev/top_printers.dbg | 2 | ||||
| -rw-r--r-- | dev/top_printers.ml | 2 | ||||
| -rw-r--r-- | dev/top_printers.mli | 2 |
8 files changed, 37 insertions, 24 deletions
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index a5aa54144c..b4d2a9ca4e 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -62,27 +62,30 @@ git_download() { local PROJECT=$1 local DEST="$CI_BUILD_DIR/$PROJECT" + local GITURL_VAR="${PROJECT}_CI_GITURL" + local GITURL="${!GITURL_VAR}" + local REF_VAR="${PROJECT}_CI_REF" + local REF="${!REF_VAR}" if [ -d "$DEST" ]; then echo "Warning: download and unpacking of $PROJECT skipped because $DEST already exists." elif [ "$FORCE_GIT" = "1" ] || [ "$CI" = "" ]; then - local GITURL_VAR="${PROJECT}_CI_GITURL" - local GITURL="${!GITURL_VAR}" - local REF_VAR="${PROJECT}_CI_REF" - local REF="${!REF_VAR}" git clone "$GITURL" "$DEST" cd "$DEST" git checkout "$REF" else # When possible, we download tarballs to reduce bandwidth and latency local ARCHIVEURL_VAR="${PROJECT}_CI_ARCHIVEURL" local ARCHIVEURL="${!ARCHIVEURL_VAR}" - local REF_VAR="${PROJECT}_CI_REF" - local REF="${!REF_VAR}" mkdir -p "$DEST" cd "$DEST" - wget "$ARCHIVEURL/$REF.tar.gz" - tar xvfz "$REF.tar.gz" --strip-components=1 - rm -f "$REF.tar.gz" + local COMMIT=$(git ls-remote "$GITURL" "refs/heads/$REF" | cut -f 1) + if [[ "$COMMIT" == "" ]]; then + # $REF must have been a tag or hash, not a branch + COMMIT="$REF" + fi + wget "$ARCHIVEURL/$COMMIT.tar.gz" + tar xvfz "$COMMIT.tar.gz" --strip-components=1 + rm -f "$COMMIT.tar.gz" fi } diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 4cd7faf757..43278c37b1 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2019-01-28-V1" +# CACHEKEY: "bionic_coq-V2019-02-17-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -56,9 +56,6 @@ ENV COMPILER_EDGE="4.07.1" \ COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \ BASE_OPAM_EDGE="dune-release.1.1.0" -RUN opam switch create $COMPILER_EDGE && eval $(opam env) && \ - opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM_EDGE - # EDGE+flambda switch, we install CI_OPAM as to be able to use # `ci-template-flambda` with everything. RUN opam switch create "${COMPILER_EDGE}+flambda" && eval $(opam env) && \ diff --git a/dev/ci/user-overlays/09439-sep-variance.sh b/dev/ci/user-overlays/09439-sep-variance.sh new file mode 100644 index 0000000000..cca85a2f68 --- /dev/null +++ b/dev/ci/user-overlays/09439-sep-variance.sh @@ -0,0 +1,14 @@ + +if [ "$CI_PULL_REQUEST" = "9439" ] || [ "$CI_BRANCH" = "sep-variance" ]; then + elpi_CI_REF=sep-variance + elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi + + equations_CI_REF=sep-variance + equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations + + mtac2_CI_REF=sep-variance + mtac2_CI_GITURL=https://github.com/SkySkimmer/mtac2 + + paramcoq_CI_REF=sep-variance + paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq +fi diff --git a/dev/include b/dev/include index b982f4c9fa..c5de83b900 100644 --- a/dev/include +++ b/dev/include @@ -41,8 +41,6 @@ #install_printer (* univ context *) ppuniverse_context;; #install_printer (* univ context future *) ppuniverse_context_future;; #install_printer (* univ context set *) ppuniverse_context_set;; -#install_printer (* cumulativity info *) ppcumulativity_info;; -#install_printer (* abstract cumulativity info *) ppabstract_cumulativity_info;; #install_printer (* univ set *) ppuniverse_set;; #install_printer (* univ instance *) ppuniverse_instance;; #install_printer (* univ subst *) ppuniverse_subst;; diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh index f588c20d02..2e8a7455de 100755 --- a/dev/lint-repository.sh +++ b/dev/lint-repository.sh @@ -9,10 +9,17 @@ CODE=0 -# We assume that all merge commits are from the main branch +if [[ $(git log -n 1 --pretty='format:%s') == "Bot merge"* ]]; then + # The FIRST parent of bot merges is from the PR, the second is + # current master + head=$(git rev-parse HEAD~) +else + head=$(git rev-parse HEAD) +fi + +# We assume that all non-bot merge commits are from the main branch # For Coq it is extremely rare for this assumption to be broken -read -r base < <(git log -n 1 --merges --pretty='format:%H') -head=$(git rev-parse HEAD) +read -r base < <(git log -n 1 --merges --pretty='format:%H' "$head") dev/lint-commits.sh "$base" "$head" || CODE=1 diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg index eab88c7290..a6ecec7e33 100644 --- a/dev/top_printers.dbg +++ b/dev/top_printers.dbg @@ -70,8 +70,6 @@ install_printer Top_printers.ppevar_universe_context install_printer Top_printers.ppconstraints install_printer Top_printers.ppuniverseconstraints install_printer Top_printers.ppuniverse_context_future -install_printer Top_printers.ppcumulativity_info -install_printer Top_printers.ppabstract_cumulativity_info install_printer Top_printers.ppuniverses install_printer Top_printers.ppnamedcontextval install_printer Top_printers.ppenv diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 2629cf8626..a3d2f33216 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -222,8 +222,6 @@ let ppuniverseconstraints c = pp (UnivProblem.Set.pr c) let ppuniverse_context_future c = let ctx = Future.force c in ppuniverse_context ctx -let ppcumulativity_info c = pp (Univ.pr_cumulativity_info Univ.Level.pr c) -let ppabstract_cumulativity_info c = pp (Univ.pr_abstract_cumulativity_info Univ.Level.pr c) let ppuniverses u = pp (UGraph.pr_universes Level.pr u) let ppnamedcontextval e = let env = Global.env () in diff --git a/dev/top_printers.mli b/dev/top_printers.mli index 4d874cdd12..cb32d2294c 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -145,8 +145,6 @@ val ppevar_universe_context : UState.t -> unit val ppconstraints : Univ.Constraint.t -> unit val ppuniverseconstraints : UnivProblem.Set.t -> unit val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit -val ppcumulativity_info : Univ.CumulativityInfo.t -> unit -val ppabstract_cumulativity_info : Univ.ACumulativityInfo.t -> unit val ppuniverses : UGraph.t -> unit val ppnamedcontextval : Environ.named_context_val -> unit |