aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--.circleci/config.yml2
-rw-r--r--.gitlab-ci.yml2
-rw-r--r--.travis.yml23
-rw-r--r--INSTALL5
-rw-r--r--dev/build/windows/makecoq_mingw.sh4
-rw-r--r--dev/ci/appveyor.sh2
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile8
-rw-r--r--dev/ci/user-overlays/07746-cleanup-unused-various.sh6
-rw-r--r--dev/ci/user-overlays/07820-mattam82-hints-constants.sh6
-rw-r--r--dev/ci/user-overlays/07898-ppedrot-rm-campl4-remains.sh8
-rw-r--r--dev/ci/user-overlays/07902-ppedrot-camlp5-parser.sh8
-rw-r--r--dev/doc/README.md2
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:
diff --git a/INSTALL b/INSTALL
index eabc729f7..6e7903a66 100644
--- a/INSTALL
+++ b/INSTALL
@@ -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>