Commit 80cfd47a authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'new_ide'

parents 6edd70de 7f63d613
......@@ -82,7 +82,7 @@ EMACS = @EMACS@
#PSVIEWER = @PSVIEWER@
#PDFVIEWER = @PDFVIEWER@
INCLUDES = @WHY3INCLUDE@ @ZIPINCLUDE@ @MENHIRINCLUDE@
INCLUDES = @WHY3INCLUDE@ @ZIPINCLUDE@ @MENHIRINCLUDE@ @NUMINCLUDE@
# warnings are enabled and non fatal by default, except:
# - disabled:
......
......@@ -420,16 +420,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
......@@ -462,7 +471,7 @@ if test "$enable_zarith" = yes; then
else
BIGINTLIB=nums
BIGINTPKG=num
BIGINTINCLUDE=
BIGINTINCLUDE="$NUMINCLUDE"
fi
# checking for camlzip
......@@ -921,6 +930,8 @@ AC_SUBST(enable_compiler_plugins)
AC_SUBST(COMPILERLIBS)
AC_SUBST(COMPILERLIBSPKG)
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
......
......@@ -19,7 +19,7 @@ set -e
eval `opam config env`
./configure --enable-local
make -j2
make
if test "$1" = bench; then
bin/why3config --detect-provers
......
......@@ -538,7 +538,7 @@ let remove_node n =
end
let interpNotif (n: notification) =
Format.kasprintf PE.log_print_msg "interpNotif: %a@\n@." Itp_communication.print_notify n;
PE.log_print_msg (Format.asprintf "interpNotif: %a@\n@." Itp_communication.print_notify n);
match n with
| Reset_whole_tree -> TaskList.clear ()
| Initialized _g ->
......
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