diff options
| -rw-r--r-- | .circleci/config.yml | 2 | ||||
| -rw-r--r-- | .gitlab-ci.yml | 2 | ||||
| -rw-r--r-- | .travis.yml | 23 | ||||
| -rw-r--r-- | INSTALL | 5 | ||||
| -rw-r--r-- | dev/build/windows/makecoq_mingw.sh | 4 | ||||
| -rw-r--r-- | dev/ci/appveyor.sh | 2 | ||||
| -rw-r--r-- | dev/ci/docker/bionic_coq/Dockerfile | 8 | ||||
| -rw-r--r-- | dev/ci/user-overlays/07746-cleanup-unused-various.sh | 6 | ||||
| -rw-r--r-- | dev/ci/user-overlays/07820-mattam82-hints-constants.sh | 6 | ||||
| -rw-r--r-- | dev/ci/user-overlays/07898-ppedrot-rm-campl4-remains.sh | 8 | ||||
| -rw-r--r-- | dev/ci/user-overlays/07902-ppedrot-camlp5-parser.sh | 8 | ||||
| -rw-r--r-- | dev/doc/README.md | 2 |
12 files changed, 26 insertions, 50 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml index 950674b34..adab42c62 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -11,7 +11,7 @@ defaults: - image: $CI_REGISTRY_IMAGE:$CACHEKEY environment: &envvars - CACHEKEY: "bionic_coq-V2018-07-02-V4" + CACHEKEY: "bionic_coq-V2018-07-11-V2" CI_REGISTRY_IMAGE: registry.gitlab.com/coq/coq version: 2 diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 7c451af26..0ad68b508 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -9,7 +9,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2018-07-02-V4" + CACHEKEY: "bionic_coq-V2018-07-11-V2" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" diff --git a/.travis.yml b/.travis.yml index ce178c8a6..3301d97ce 100644 --- a/.travis.yml +++ b/.travis.yml @@ -39,13 +39,14 @@ env: - NJOBS=2 # system is == 4.02.3 - COMPILER="system" - - COMPILER_BE="4.06.1" + - COMPILER_BE="4.07.0" + - DUNE_VER=".1.0.0" - CAMLP5_VER=".6.14" - - CAMLP5_VER_BE=".7.05" + - CAMLP5_VER_BE=".7.06" - FINDLIB_VER=".1.4.1" - FINDLIB_VER_BE=".1.8.0" - - LABLGTK="lablgtk.2.18.3 lablgtk-extras.1.6" - - LABLGTK_BE="lablgtk.2.18.6 lablgtk-extras.1.6" + - LABLGTK="lablgtk.2.18.3 conf-gtksourceview.2" + - LABLGTK_BE="lablgtk.2.18.6 conf-gtksourceview.2" - NATIVE_COMP="yes" - COQ_DEST="-local" - MAIN_TARGET="world" @@ -196,8 +197,9 @@ matrix: - os: osx env: - TEST_TARGET="test-suite" - - COMPILER="4.02.3" - - CAMLP5_VER=".6.17" + - COMPILER="${COMPILER_BE}" + - FINDLIB_VER="${FINDLIB_VER_BE}" + - CAMLP5_VER="${CAMLP5_VER_BE}" - NATIVE_COMP="no" - COQ_DEST="-local" - EXTRA_OPAM="ounit" @@ -211,12 +213,13 @@ matrix: osx_image: xcode7.3 env: - TEST_TARGET="" - - COMPILER="4.02.3" - - CAMLP5_VER=".6.17" + - COMPILER="${COMPILER_BE}" + - FINDLIB_VER="${FINDLIB_VER_BE}" + - CAMLP5_VER="${CAMLP5_VER_BE}" - NATIVE_COMP="no" - COQ_DEST="-prefix ${PWD}/_install" - EXTRA_CONF="-coqide opt -warn-error yes" - - EXTRA_OPAM="${LABLGTK}" + - EXTRA_OPAM="${LABLGTK_BE}" before_install: - brew update - brew unlink python @@ -246,7 +249,7 @@ install: - opam switch "$COMPILER" && opam update - eval $(opam config env) - opam config list -- opam install -j ${NJOBS} -y num ocamlfind${FINDLIB_VER} jbuilder camlp5${CAMLP5_VER} ${EXTRA_OPAM} +- opam install -j ${NJOBS} -y num ocamlfind${FINDLIB_VER} dune${DUNE_VER} camlp5${CAMLP5_VER} ${EXTRA_OPAM} - opam list script: @@ -29,8 +29,9 @@ WHAT DO YOU NEED ? To compile Coq yourself, you need: - - OCaml version 4.02.3 or later + - OCaml (version >= 4.02.3) (available at https://ocaml.org/) + (This version of Coq has been tested up to OCaml 4.07.0) - The Num package, which used to be part of the OCaml standard library, if you are using an OCaml version >= 4.06.0 @@ -68,7 +69,7 @@ WHAT DO YOU NEED ? profit from Flambda, a special build of the OCaml compiler that has the Flambda optimizer enabled must be installed. For OPAM users, this amounts to installing a compiler switch ending in `+flambda`, - such as `4.06.1+flambda`. For other users, YMMV. Once `ocamlopt + such as `4.07.0+flambda`. For other users, YMMV. Once `ocamlopt -config` reports that Flambda is available, some further optimization options can be used; see the entry about -flambda-opts below for more details. diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 94e90bf4f..da5ac2b15 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -793,7 +793,7 @@ function make_ln { function make_ocaml { get_flex_dll_link_bin - if build_prep http://caml.inria.fr/pub/distrib/ocaml-4.06 ocaml-4.06.1 tar.gz 1 ; then + if build_prep http://caml.inria.fr/pub/distrib/ocaml-4.07 ocaml-4.07.0 tar.gz 1 ; then # See README.win32.adoc cp config/m-nt.h byterun/caml/m.h cp config/s-nt.h byterun/caml/s.h @@ -933,7 +933,7 @@ function make_camlp5 { make_ocaml make_findlib - if build_prep https://github.com/camlp5/camlp5/archive rel705 tar.gz 1 camlp5-rel705; then + if build_prep https://github.com/camlp5/camlp5/archive rel706 tar.gz 1 camlp5-rel706; then logn configure ./configure # Somehow my virus scanner has the boot.new/SAVED directory locked after the move for a second => repeat until success sed -i 's/mv boot.new boot/until mv boot.new boot; do sleep 1; done/' Makefile diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh index 7bf9ad8c9..d2176e326 100644 --- a/dev/ci/appveyor.sh +++ b/dev/ci/appveyor.sh @@ -2,7 +2,7 @@ set -e -x -APPVEYOR_OPAM_SWITCH=4.06.1+mingw64c +APPVEYOR_OPAM_SWITCH=4.07.0+mingw64c wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.1/opam64.tar.xz tar -xf opam64.tar.xz diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index a4ee6a379..1361392dc 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-07-02-V4" +# CACHEKEY: "bionic_coq-V2018-07-11-V2" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -28,7 +28,7 @@ RUN opam init -a -y -j $NJOBS --compiler="$COMPILER" default https://opam.ocaml. # Common OPAM packages. # `num` does not have a version number as the right version to install varies # with the compiler version. -ENV BASE_OPAM="num ocamlfind.1.8.0 jbuilder.1.0+beta20 ounit.2.0.8" \ +ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.0.0 ounit.2.0.8" \ CI_OPAM="menhir.20180530 elpi.1.0.4 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. @@ -43,8 +43,8 @@ RUN opam switch -y -j $NJOBS "${COMPILER}+32bit" && eval $(opam config env) && \ opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER # EDGE switch -ENV COMPILER_EDGE="4.06.1" \ - CAMLP5_VER_EDGE="7.05" \ +ENV COMPILER_EDGE="4.07.0" \ + CAMLP5_VER_EDGE="7.06" \ COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" RUN opam switch -y -j $NJOBS $COMPILER_EDGE && eval $(opam config env) && \ diff --git a/dev/ci/user-overlays/07746-cleanup-unused-various.sh b/dev/ci/user-overlays/07746-cleanup-unused-various.sh deleted file mode 100644 index 8688b0d53..000000000 --- a/dev/ci/user-overlays/07746-cleanup-unused-various.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "7746" ] || [ "$CI_BRANCH" = "cleanup-unused-various" ]; then - Equations_CI_BRANCH="adapt-unused" - Equations_CI_GITURL="https://github.com/SkySkimmer/Coq-Equations.git" -fi diff --git a/dev/ci/user-overlays/07820-mattam82-hints-constants.sh b/dev/ci/user-overlays/07820-mattam82-hints-constants.sh deleted file mode 100644 index 2ae86ae22..000000000 --- a/dev/ci/user-overlays/07820-mattam82-hints-constants.sh +++ /dev/null @@ -1,6 +0,0 @@ -_OVERLAY_BRANCH=hints-variables-overlay - -if [ "$CI_PULL_REQUEST" = "7820" ] || [ "$CI_BRANCH" = "_OVERLAY_BRANCH" ]; then - - Equations_CI_BRANCH="$_OVERLAY_BRANCH" -fi diff --git a/dev/ci/user-overlays/07898-ppedrot-rm-campl4-remains.sh b/dev/ci/user-overlays/07898-ppedrot-rm-campl4-remains.sh deleted file mode 100644 index 9c4c905fa..000000000 --- a/dev/ci/user-overlays/07898-ppedrot-rm-campl4-remains.sh +++ /dev/null @@ -1,8 +0,0 @@ -_OVERLAY_BRANCH=rm-campl4-remains - -if [ "$CI_PULL_REQUEST" = "7898" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then - - pidetop_CI_BRANCH="$_OVERLAY_BRANCH" - pidetop_CI_GITURL=https://github.com/ppedrot/pidetop - -fi diff --git a/dev/ci/user-overlays/07902-ppedrot-camlp5-parser.sh b/dev/ci/user-overlays/07902-ppedrot-camlp5-parser.sh deleted file mode 100644 index 735153ebd..000000000 --- a/dev/ci/user-overlays/07902-ppedrot-camlp5-parser.sh +++ /dev/null @@ -1,8 +0,0 @@ -_OVERLAY_BRANCH=camlp5-parser - -if [ "$CI_PULL_REQUEST" = "7902" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then - - ltac2_CI_BRANCH="$_OVERLAY_BRANCH" - ltac2_CI_GITURL=https://github.com/ppedrot/ltac2 - -fi diff --git a/dev/doc/README.md b/dev/doc/README.md index 1a4e40f68..223cf6286 100644 --- a/dev/doc/README.md +++ b/dev/doc/README.md @@ -7,7 +7,7 @@ Assuming one is running Ubuntu (if not, replace `apt` with the package manager o ``` $ sudo apt-get install make opam git -# At the time of writing, <latest-ocaml-version> is 4.06.1. +# At the time of writing, <latest-ocaml-version> is 4.07.0. # The latest version number is available at: https://ocaml.org/releases/ $ opam init --comp <latest-ocaml-version> |