Commit 31285d48 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

add --enable-native-code to configure.in

Also, do not build the bytecode of the why3 library when compiling
in native code.
parent ccc5698c
...@@ -47,7 +47,6 @@ STRIP = @STRIP@ ...@@ -47,7 +47,6 @@ STRIP = @STRIP@
CC = @CC@ CC = @CC@
OCAMLC = @OCAMLC@ OCAMLC = @OCAMLC@
OCAMLOPT = @OCAMLOPT@ OCAMLOPT = @OCAMLOPT@
OCAMLDEP = @OCAMLDEP@
OCAMLLEX = @OCAMLLEX@ OCAMLLEX = @OCAMLLEX@
OCAMLYACC = @OCAMLYACC@ OCAMLYACC = @OCAMLYACC@
OCAMLDOC = @OCAMLDOC@ OCAMLDOC = @OCAMLDOC@
...@@ -58,14 +57,10 @@ COQC = @COQC@ ...@@ -58,14 +57,10 @@ COQC = @COQC@
COQDEP = @COQDEP@ COQDEP = @COQDEP@
CAMLP5O = @CAMLP5O@ CAMLP5O = @CAMLP5O@
ifeq (@enable_menhirlib@,yes) ifeq (@OCAMLBEST@,opt)
MENHIR = @MENHIR@ --table OCAMLDEP = @OCAMLDEP@ -native
MENHIRINC = -I @MENHIRLIB@
MENHIRLIB = menhirLib
else else
MENHIR = @MENHIR@ OCAMLDEP = @OCAMLDEP@
MENHIRINC =
MENHIRLIB =
endif endif
RUBBER = @RUBBER@ RUBBER = @RUBBER@
...@@ -1221,8 +1216,13 @@ clean:: ...@@ -1221,8 +1216,13 @@ clean::
# generic rules # generic rules
################ ################
ifeq (@OCAMLBEST@,opt)
%.cmi: %.mli
$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -c $(OFLAGS) $<
else
%.cmi: %.mli %.cmi: %.mli
$(if $(QUIET),@echo 'Ocamlc $<' &&) $(OCAMLC) -c $(BFLAGS) $< $(if $(QUIET),@echo 'Ocamlc $<' &&) $(OCAMLC) -c $(BFLAGS) $<
endif
%.cmo: %.ml %.cmo: %.ml
$(if $(QUIET),@echo 'Ocamlc $<' &&) $(OCAMLC) -c $(BFLAGS) $< $(if $(QUIET),@echo 'Ocamlc $<' &&) $(OCAMLC) -c $(BFLAGS) $<
......
...@@ -65,6 +65,12 @@ AC_ARG_ENABLE(local, ...@@ -65,6 +65,12 @@ AC_ARG_ENABLE(local,
[ --enable-local use Why3 in the build directory (no installation)],, [ --enable-local use Why3 in the build directory (no installation)],,
enable_local=no) enable_local=no)
# NATIVE
AC_ARG_ENABLE(native-code,
[ --enable-native-code use the native-code compiler if available],,
enable_native_code=yes)
# IDE # IDE
AC_ARG_ENABLE(ide, AC_ARG_ENABLE(ide,
...@@ -170,6 +176,13 @@ else ...@@ -170,6 +176,13 @@ else
fi fi
fi fi
# checking for native-code
if test "$enable_native_code" != yes || test "$OCAMLBEST" = byte ; then
enable_native_code=no
OCAMLBEST=byte
OCAMLOPT=no
fi
# checking for ocamlc.opt # checking for ocamlc.opt
AC_CHECK_PROG(OCAMLCDOTOPT,ocamlc.opt,ocamlc.opt,no) AC_CHECK_PROG(OCAMLCDOTOPT,ocamlc.opt,ocamlc.opt,no)
if test "$OCAMLCDOTOPT" != no ; then if test "$OCAMLCDOTOPT" != no ; then
...@@ -526,6 +539,7 @@ echo " Summary" ...@@ -526,6 +539,7 @@ echo " Summary"
echo "-----------------------------------------" echo "-----------------------------------------"
echo "OCaml version : $OCAMLVERSION" echo "OCaml version : $OCAMLVERSION"
echo "OCaml library path : $OCAMLLIB" echo "OCaml library path : $OCAMLLIB"
echo "Compile in native code : $enable_native_code"
echo "Verbose make : $enable_verbose_make" echo "Verbose make : $enable_verbose_make"
echo "Why IDE : $enable_ide $reason_ide" echo "Why IDE : $enable_ide $reason_ide"
echo "Why bench tool : $enable_bench" echo "Why bench tool : $enable_bench"
......
Supports Markdown
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