Commit bf3e01d6 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'bugfix/v0.87'

parents 0fbe64ff e929c65f
......@@ -110,6 +110,9 @@ OFLAGS += -bin-annot
BFLAGS += -bin-annot
endif
# see http://caml.inria.fr/mantis/view.php?id=4991
CMIHACK = -intf-suffix .cmi
# external libraries common to all binaries
EXTOBJS = @MENHIRLIB@
......@@ -261,9 +264,9 @@ lib/why3/why3.cmo: $(LIBCMO)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
lib/why3/why3.cmx: $(LIBCMX)
lib/why3/why3.cmx: $(LIBCMX) lib/why3/why3.cmo
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^
$(HIDE)$(OCAMLOPT) $(OFLAGS) $(CMIHACK) -pack -o $@ $(filter %.cmx, $^)
# clean and depend
......@@ -1340,9 +1343,9 @@ lib/why3/why3extract.cmo: $(OCAMLLIBS_CMO)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
lib/why3/why3extract.cmx: $(OCAMLLIBS_CMX)
lib/why3/why3extract.cmx: $(OCAMLLIBS_CMX) lib/why3/why3extract.cmo
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^
$(HIDE)$(OCAMLOPT) $(OFLAGS) $(CMIHACK) -pack -o $@ $(filter %.cmx, $^)
install_no_local_lib::
$(MKDIR_P) $(OCAMLINSTALLLIB)/why3
......@@ -1858,16 +1861,26 @@ clean::
# suppress "unused rec" warning for Menhir-produced files
%.cmx: %.ml %.mly
$(SHOW) 'Ocamlopt $<'
$(HIDE)$(OCAMLOPT) -c $(OFLAGS) -w -39 $<
$(HIDE)$(OCAMLOPT) -c $(OFLAGS) -w -39 $(CMIHACK) $<
%.cmo: %.ml
$(SHOW) 'Ocamlc $<'
$(HIDE)$(OCAMLC) -c $(BFLAGS) $<
%.cmx: %.ml
%.cmx: %.ml %.mli
$(SHOW) 'Ocamlopt $<'
$(HIDE)$(OCAMLOPT) -c $(OFLAGS) $<
# the generic rule cannot be applied since ocaml would confuse
# lib/why3/why3extract.cmi for the interface (!!!)
src/tools/why3extract.cmx: src/tools/why3extract.ml
$(SHOW) 'Ocamlopt $<'
$(HIDE)$(OCAMLOPT) -c $(OFLAGS) $<
%.cmx: %.ml
$(SHOW) 'Ocamlopt $<'
$(HIDE)$(OCAMLOPT) -c $(OFLAGS) $(CMIHACK) $<
%.cma:
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) -a $(BFLAGS) -o $@ $^
......@@ -1894,7 +1907,9 @@ clean::
%.dep: %.ml
$(SHOW) 'Ocamldep $<'
$(HIDE)$(OCAMLDEP) $(DEPFLAGS) $< $(TOTARGET)
$(HIDE)($(OCAMLDEP) $(DEPFLAGS) $<; \
echo '$*.cmx : $*.cmi'; \
echo '$*.cmi : $*.cmo') $(TOTARGET)
%.opt:
$(SHOW) 'Linking $@'
......
......@@ -708,11 +708,8 @@ dnl AC_CHECK_PROGS(PDFVIEWER,xpdf acroread evince)
VERSION=$PACKAGE_VERSION
BUILDDATE="$(date)"
# substitutions to perform
AC_SUBST(VERSION)
AC_SUBST(BUILDDATE)
AC_SUBST(enable_verbose_make)
......
......@@ -5,7 +5,7 @@ invalid "Completion found"
timeout "Ran out of time"
timeout "CPU time limit exceeded"
outofmemory "Out of Memory"
unknown "No Proof Found" ""
unknown "No proof found" ""
fail "Failure.*" "\"\\0\""
time "why3cpulimit time : %s s"
......
......@@ -23,7 +23,6 @@ fi
echo "
let version = \"@VERSION@\"
let builddate = \"@BUILDDATE@\"
let libdir = $libdir
let datadir = $datadir
......
......@@ -42,8 +42,8 @@ let option_list = [
Arg.Unit (fun _ -> printf "%s@." Config.datadir; exit 0),
" print location of non-binary data (theories, modules, etc)";
"--version",
Arg.Unit (fun _ -> printf "Why3 platform, version %s (build date: %s)@."
Config.version Config.builddate; exit 0),
Arg.Unit (fun _ -> printf "Why3 platform, version %s@."
Config.version; exit 0),
" print version information";
]
......
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