Commit ac1f59e2 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'next' into new_ide

parents b57e40d4 273f47ff
......@@ -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:
......
......@@ -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
......@@ -863,6 +872,8 @@ AC_SUBST(HASJSOFOCAML)
AC_SUBST(META_OCAMLGRAPH)
AC_SUBST(NUMINCLUDE)
AC_SUBST(enable_zarith)
AC_SUBST(BIGINTINCLUDE)
AC_SUBST(BIGINTLIB)
......
......@@ -11,7 +11,7 @@ WORKDIR /home/why3/why3
RUN eval `opam config env` && \
./configure && \
make -j2
make
USER root
......
......@@ -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
......@@ -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
......
......@@ -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
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment