Merge branch 'bugfix/v0.88' into next

Makefile.in

@@ -76,7 +76,7 @@ EMACS = @EMACS@
 #PSVIEWER  = @PSVIEWER@
 #PDFVIEWER = @PDFVIEWER@
 
-INCLUDES = @ZIPINCLUDE@ @MENHIRINCLUDE@
+INCLUDES = @ZIPINCLUDE@ @MENHIRINCLUDE@ @NUMINCLUDE@
 
 # warnings are enabled and non fatal by default, except:
 # - disabled:

configure.in

@@ -357,16 +357,25 @@ if test "$enable_emacs_compilation" = yes ; then
 fi
 
 # checking for Num
-DIR=
+# (ocamlfind cannot be trusted here, since the default installation path is $OCAMLLIB)
+found_num=no
 if test "$USEOCAMLFIND" = yes; then
    DIR=$(ocamlfind query num)
    if test -n "$DIR"; then
       echo "ocamlfind found num in $DIR"
+      NUMINCLUDE="-I $DIR"
+      found_num=yes
+      AC_CHECK_FILE($DIR/nums.cma,,found_num=no)
+      AC_CHECK_FILE($DIR/num.cmi,,found_num=no)
    fi
 fi
-DIR="$OCAMLLIB"
-AC_CHECK_FILE($DIR/nums.cma,,found_num=no)
-AC_CHECK_FILE($DIR/num.cmi,,found_num=no)
+if test "$found_num" = no; then
+   DIR="$OCAMLLIB"
+   NUMINCLUDE=
+   found_num=yes
+   AC_CHECK_FILE($DIR/nums.cma,,found_num=no)
+   AC_CHECK_FILE($DIR/num.cmi,,found_num=no)
+fi
 if test "$found_num" = no; then
    AC_MSG_ERROR([Library Num not found.])
 fi
@@ -399,7 +408,7 @@ if test "$enable_zarith" = yes; then
 else
    BIGINTLIB=nums
    BIGINTPKG=num
-   BIGINTINCLUDE=
+   BIGINTINCLUDE="$NUMINCLUDE"
 fi
 
 # checking for camlzip
@@ -838,6 +847,8 @@ AC_SUBST(LABLGTK2PKG)
 
 AC_SUBST(META_OCAMLGRAPH)
 
+AC_SUBST(NUMINCLUDE)
+
 AC_SUBST(enable_zarith)
 AC_SUBST(BIGINTINCLUDE)
 AC_SUBST(BIGINTLIB)

misc/Dockerfile.deploy

@@ -11,7 +11,7 @@ WORKDIR /home/why3/why3
 
 RUN eval `opam config env` && \
     ./configure && \
-    make -j2
+    make
 
 USER root
 

misc/Dockerfile.init

@@ -11,8 +11,8 @@ ENV HOME /home/why3
 WORKDIR /home/why3
 
 ARG compiler=system
-RUN opam init -a -y -j2 --compiler=$compiler
-RUN opam install -y menhir conf-gtksourceview lablgtk ocamlgraph zarith camlzip
+RUN opam init -a -y -j1 --compiler=$compiler
+RUN opam repository add coq-released https://coq.inria.fr/opam/released
 
-# Alt-Ergo
-RUN opam install alt-ergo.1.30
+ARG packages
+RUN opam install -y menhir conf-gtksourceview lablgtk ocamlgraph zarith camlzip alt-ergo $packages

misc/ci-docker.sh

@@ -3,8 +3,13 @@
 set -e
 
 autoconf && (automake --add-missing 2> /dev/null || true)
-docker build -t bench-image-$COMPILER -f misc/Dockerfile.init --build-arg compiler=$COMPILER .
-CID=$(docker create --rm -i -w /home/why3/why3 bench-image-$COMPILER /bin/sh)
+if test -n "$PACKAGES"; then
+  IMAGE=bench-image-$COMPILER--$(echo $PACKAGES | sed -e 's/ /--/g')
+else
+  IMAGE=bench-image-$COMPILER
+fi
+docker build -t $IMAGE -f misc/Dockerfile.init --build-arg compiler=$COMPILER --build-arg packages="$PACKAGES" .
+CID=$(docker create --rm -i -w /home/why3/why3 $IMAGE /bin/sh)
 docker start $CID
 docker cp . $CID:/home/why3/why3
 docker exec -u root $CID chown -R why3:why3 /home/why3/why3

misc/ci-local.sh

@@ -18,7 +18,7 @@ set -e
 eval `opam config env`
 
 ./configure --enable-local
-make -j2
+make
 
 if test "$1" = bench; then
 bin/why3config --detect-provers