diff options
| author | Emilio Jesus Gallego Arias | 2018-10-16 14:55:30 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-08-27 19:03:33 +0200 |
| commit | 094e4649c29e2426daca0476c140439de901dafe (patch) | |
| tree | b6ae0cbed1ef81a84807c4d376dd610b2b2d7bbd /dev/ci | |
| parent | a87c09c13028502ea86a553724a4131c5246145a (diff) | |
[numeral] [plugins] Switch from `Big_int` to ZArith.
We replace Coq's use of `Big_int` and `num` by the ZArith OCaml
library which is a more modern version.
We switch the core files and easy plugins only for now, more complex
numerical plugins will be done in their own commit.
We thus keep the num library linked for now until all plugins are
ported.
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
Diffstat (limited to 'dev/ci')
| -rwxr-xr-x | dev/ci/azure-opam.sh | 2 | ||||
| -rw-r--r-- | dev/ci/docker/bionic_coq/Dockerfile | 20 | ||||
| -rw-r--r-- | dev/ci/user-overlays/08743-ejgallego-zarith.sh | 6 |
3 files changed, 20 insertions, 8 deletions
diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh index 64936cd236..17d71ac52a 100755 --- a/dev/ci/azure-opam.sh +++ b/dev/ci/azure-opam.sh @@ -10,4 +10,4 @@ bash opam64/install.sh opam init default -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $OPAM_VARIANT --disable-sandboxing eval "$(opam env)" -opam install -y num ocamlfind dune ounit +opam install -y num ocamlfind dune ounit zarith diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 67a8415891..78c8673299 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2020-08-18-V29" +# CACHEKEY: "bionic_coq-V2020-08-28-V92" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -6,9 +6,14 @@ LABEL maintainer="e@x80.org" ENV DEBIAN_FRONTEND="noninteractive" +# We need libgmp-dev:i386 for zarith; maybe we could also install GTK +RUN dpkg --add-architecture i386 + RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ # Dependencies of the image, the test-suite and external projects m4 automake autoconf time wget rsync git gcc-multilib build-essential unzip jq \ + # Dependencies of ZArith + perl libgmp-dev libgmp-dev:i386 \ # Dependencies of lablgtk (for CoqIDE) libgtksourceview-3.0-dev \ # Dependencies of stdlib and sphinx doc @@ -35,10 +40,10 @@ ENV NJOBS="2" \ # Base opam is the set of base packages required by Coq ENV COMPILER="4.05.0" -# 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.1 ounit2.2.2.3 odoc.1.5.0" \ +# Common OPAM packages, num to be removed once the migration to +# micromega is complete, `num` also does not have a version number as +# the right version to install varies with the compiler version. +ENV BASE_OPAM="num zarith.1.9.1 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.0" \ CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \ BASE_ONLY_OPAM="elpi.1.11.0" @@ -52,9 +57,10 @@ ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.0" RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \ opam install $BASE_OPAM $COQIDE_OPAM $CI_OPAM $BASE_ONLY_OPAM -# base+32bit switch +# base+32bit switch, note the zarith hack RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ - opam install $BASE_OPAM + i386 env CC='gcc -m32' opam install zarith.1.9.1 && \ + opam install $BASE_OPAM # EDGE switch ENV COMPILER_EDGE="4.10.0" \ diff --git a/dev/ci/user-overlays/08743-ejgallego-zarith.sh b/dev/ci/user-overlays/08743-ejgallego-zarith.sh new file mode 100644 index 0000000000..da1d30c1e9 --- /dev/null +++ b/dev/ci/user-overlays/08743-ejgallego-zarith.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "11742" ] || [ "$CI_BRANCH" = "zarith+core" ]; then + + bignums_CI_REF=zarith + bignums_CI_GITURL=https://github.com/ejgallego/bignums + +fi |