Commit 7d9776f4 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'bugfix/v0.87'

parents e2c7febe 3e87d19e
...@@ -124,8 +124,6 @@ EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS)) $(addsuffix .cmx,$(EXTOBJS)) ...@@ -124,8 +124,6 @@ EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS)) $(addsuffix .cmx,$(EXTOBJS))
INSTALLED_LIB_EXTS = a cma cmx cmi cmxa cmxs INSTALLED_LIB_EXTS = a cma cmx cmi cmxa cmxs
COMPILED_LIB_EXTS = $(INSTALLED_LIB_EXTS) o cmo cmt cmti annot dep conflicts COMPILED_LIB_EXTS = $(INSTALLED_LIB_EXTS) o cmo cmt cmti annot dep conflicts
TARGET_EMACS = share/emacs/why3.elc
TOTARGET = > "$@" || (RV=$$?; rm -f "$@"; exit $${RV}) TOTARGET = > "$@" || (RV=$$?; rm -f "$@"; exit $${RV})
############### ###############
...@@ -290,11 +288,7 @@ clean_old_install:: ...@@ -290,11 +288,7 @@ clean_old_install::
rm -rf $(OCAMLINSTALLLIB)/why3 rm -rf $(OCAMLINSTALLLIB)/why3
ifeq ($(EMACS),no)
install_no_local:: clean_old_install install_no_local:: clean_old_install
else
install_no_local:: clean_old_install $(TARGET_EMACS)
endif
$(MKDIR_P) $(BINDIR) $(MKDIR_P) $(BINDIR)
$(MKDIR_P) $(LIBDIR)/why3 $(MKDIR_P) $(LIBDIR)/why3
$(MKDIR_P) $(TOOLDIR) $(MKDIR_P) $(TOOLDIR)
...@@ -305,7 +299,6 @@ endif ...@@ -305,7 +299,6 @@ endif
$(MKDIR_P) $(DATADIR)/why3/theories $(MKDIR_P) $(DATADIR)/why3/theories
$(MKDIR_P) $(DATADIR)/why3/modules/mach $(MKDIR_P) $(DATADIR)/why3/modules/mach
$(MKDIR_P) $(DATADIR)/why3/drivers $(MKDIR_P) $(DATADIR)/why3/drivers
$(MKDIR_P) $(DATADIR)/emacs/site-lisp/
$(INSTALL_DATA) theories/*.why $(DATADIR)/why3/theories $(INSTALL_DATA) theories/*.why $(DATADIR)/why3/theories
$(INSTALL_DATA) modules/*.mlw $(DATADIR)/why3/modules $(INSTALL_DATA) modules/*.mlw $(DATADIR)/why3/modules
$(INSTALL_DATA) modules/mach/*.mlw $(DATADIR)/why3/modules/mach $(INSTALL_DATA) modules/mach/*.mlw $(DATADIR)/why3/modules/mach
...@@ -355,16 +348,19 @@ uninstall: clean_old_install ...@@ -355,16 +348,19 @@ uninstall: clean_old_install
clean_old_install:: clean_old_install::
rm -f $(DATADIR)/emacs/site-lisp/why3.el rm -f $(DATADIR)/emacs/site-lisp/why3.el
ifneq ($(EMACS),no)
rm -f $(DATADIR)/emacs/site-lisp/why3.elc rm -f $(DATADIR)/emacs/site-lisp/why3.elc
endif
install_no_local:: install_no_local::
$(MKDIR_P) $(DATADIR)/emacs/site-lisp/
$(INSTALL_DATA) share/emacs/why3.el $(DATADIR)/emacs/site-lisp/why3.el $(INSTALL_DATA) share/emacs/why3.el $(DATADIR)/emacs/site-lisp/why3.el
ifneq ($(EMACS),no) ifeq (@enable_emacs_compilation@,yes)
$(INSTALL_DATA) share/emacs/why3.elc $(DATADIR)/emacs/site-lisp/why3.elc $(INSTALL_DATA) share/emacs/why3.elc $(DATADIR)/emacs/site-lisp/why3.elc
endif endif
ifeq (@enable_emacs_compilation@,yes)
all: share/emacs/why3.elc
endif
################## ##################
# Why3 plugins # Why3 plugins
...@@ -584,7 +580,7 @@ CPULIM_O := $(addprefix src/server/, $(addsuffix .o, $(CPULIM_MODULES))) ...@@ -584,7 +580,7 @@ CPULIM_O := $(addprefix src/server/, $(addsuffix .o, $(CPULIM_MODULES)))
TOOLS = lib/why3server$(EXE) lib/why3cpulimit$(EXE) TOOLS = lib/why3server$(EXE) lib/why3cpulimit$(EXE)
byte opt: $(TOOLS) all: $(TOOLS)
lib/why3server$(EXE): $(SERVER_O) lib/why3server$(EXE): $(SERVER_O)
$(CC) -Wall -o $@ $^ $(CC) -Wall -o $@ $^
...@@ -1036,9 +1032,7 @@ COQVD = $(addsuffix .vd, $(COQLIBS_FILES)) ...@@ -1036,9 +1032,7 @@ COQVD = $(addsuffix .vd, $(COQLIBS_FILES))
$(SHOW) 'Coqdep $<' $(SHOW) 'Coqdep $<'
$(HIDE)$(COQDEP) -R lib/coq Why3 $< $(TOTARGET) $(HIDE)$(COQDEP) -R lib/coq Why3 $< $(TOTARGET)
opt byte: $(COQVO) all: $(COQVO) drivers/coq-realizations.aux
install_local:: $(COQVO) drivers/coq-realizations.aux
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean" ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
ifneq "$(MAKECMDGOALS:update-coq%=update-coq)" "update-coq" ifneq "$(MAKECMDGOALS:update-coq%=update-coq)" "update-coq"
...@@ -1064,8 +1058,6 @@ endif ...@@ -1064,8 +1058,6 @@ endif
install_no_local:: install_no_local::
$(INSTALL_DATA) drivers/coq-realizations.aux $(DATADIR)/why3/drivers/ $(INSTALL_DATA) drivers/coq-realizations.aux $(DATADIR)/why3/drivers/
opt byte: drivers/coq-realizations.aux
clean:: clean::
rm -f drivers/coq-realizations.aux rm -f drivers/coq-realizations.aux
...@@ -1123,8 +1115,6 @@ install_no_local:: ...@@ -1123,8 +1115,6 @@ install_no_local::
$(INSTALL_DATA) $(addsuffix .pvs, $(PVSLIBS_FP)) $(LIBDIR)/why3/pvs/floating_point/ $(INSTALL_DATA) $(addsuffix .pvs, $(PVSLIBS_FP)) $(LIBDIR)/why3/pvs/floating_point/
$(INSTALL_DATA) drivers/pvs-realizations.aux $(DATADIR)/why3/drivers/ $(INSTALL_DATA) drivers/pvs-realizations.aux $(DATADIR)/why3/drivers/
install_local:: drivers/pvs-realizations.aux
update-pvs: bin/why3realize.@OCAMLBEST@ drivers/pvs-realizations.aux update-pvs: bin/why3realize.@OCAMLBEST@ drivers/pvs-realizations.aux
for f in $(PVSLIBS_INT_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/pvs-realize.drv -T int.$$f -o lib/pvs/int/; done for f in $(PVSLIBS_INT_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/pvs-realize.drv -T int.$$f -o lib/pvs/int/; done
for f in $(PVSLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/pvs-realize.drv -T real.$$f -o lib/pvs/real/; done for f in $(PVSLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/pvs-realize.drv -T real.$$f -o lib/pvs/real/; done
...@@ -1143,7 +1133,7 @@ install_no_local:: ...@@ -1143,7 +1133,7 @@ install_no_local::
endif endif
opt byte: drivers/pvs-realizations.aux all: drivers/pvs-realizations.aux
clean:: clean::
rm -f drivers/pvs-realizations.aux rm -f drivers/pvs-realizations.aux
...@@ -1292,7 +1282,7 @@ $(ISABELLELIBS_BV): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.au ...@@ -1292,7 +1282,7 @@ $(ISABELLELIBS_BV): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.au
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T bv.$(notdir $(basename $@)) -o lib/isabelle/bv/ WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T bv.$(notdir $(basename $@)) -o lib/isabelle/bv/
# do not update isabelle realizations systematically # do not update isabelle realizations systematically
# opt byte: update-isabelle # all: update-isabelle
clean:: clean::
rm -f lib/isabelle/*/*.xml rm -f lib/isabelle/*/*.xml
...@@ -1308,7 +1298,7 @@ install_no_local:: ...@@ -1308,7 +1298,7 @@ install_no_local::
endif endif
opt byte: drivers/isabelle-realizations.aux all: drivers/isabelle-realizations.aux
clean:: clean::
rm -f drivers/isabelle-realizations.aux rm -f drivers/isabelle-realizations.aux
...@@ -2032,7 +2022,7 @@ doc/version.tex: doc/version.tex.in config.status ...@@ -2032,7 +2022,7 @@ doc/version.tex: doc/version.tex.in config.status
config.status: configure config.status: configure
./config.status --recheck ./config.status --recheck
opt byte: lib/why3/META .merlin all: lib/why3/META .merlin
lib/why3/META: lib/why3/META.in config.status lib/why3/META: lib/why3/META.in config.status
./config.status chmod --file $@ ./config.status chmod --file $@
......
...@@ -127,6 +127,12 @@ AC_ARG_ENABLE(profiling, ...@@ -127,6 +127,12 @@ AC_ARG_ENABLE(profiling,
AS_HELP_STRING([--enable-profiling], [enable profiling]),, AS_HELP_STRING([--enable-profiling], [enable profiling]),,
enable_profiling=no) enable_profiling=no)
# Emacs compilation
AC_ARG_ENABLE(emacs-compilation,
AS_HELP_STRING([--disable-emacs-compilation], [do not compile why3.elc]),,
enable_emacs_compilation=yes)
# either relocation or local, not both # either relocation or local, not both
if test "$enable_relocation" = yes ; then if test "$enable_relocation" = yes ; then
if test "$enable_local" = yes ; then if test "$enable_local" = yes ; then
...@@ -348,7 +354,13 @@ if test "$enable_html_doc" = yes ; then ...@@ -348,7 +354,13 @@ if test "$enable_html_doc" = yes ; then
fi fi
# checking for emacs # checking for emacs
AC_CHECK_PROG(EMACS,emacs,emacs,no) if test "$enable_emacs_compilation" = yes ; then
AC_CHECK_PROG(EMACS,emacs,emacs,no)
if test "$EMACS" = no ; then
enable_emacs_compilation=no
AC_MSG_WARN([Cannot find emacs, compilation of why3.elc disabled.])
fi
fi
# checking for Zarith # checking for Zarith
if test "$enable_zarith" = yes; then if test "$enable_zarith" = yes; then
...@@ -786,6 +798,8 @@ AC_SUBST(enable_html_doc) ...@@ -786,6 +798,8 @@ AC_SUBST(enable_html_doc)
AC_SUBST(RUBBER) AC_SUBST(RUBBER)
AC_SUBST(HEVEA) AC_SUBST(HEVEA)
AC_SUBST(HACHA) AC_SUBST(HACHA)
AC_SUBST(enable_emacs_compilation)
AC_SUBST(EMACS) AC_SUBST(EMACS)
AC_SUBST(enable_frama_c) AC_SUBST(enable_frama_c)
......
...@@ -27,7 +27,7 @@ available: [ ocaml-version >= "4.01.0" ] ...@@ -27,7 +27,7 @@ available: [ ocaml-version >= "4.01.0" ]
build: [ build: [
["./configure" "--prefix" prefix "--disable-frama-c" ["./configure" "--prefix" prefix "--disable-frama-c"
"--disable-ide" { !conf-gtksourceview:installed }] "--disable-ide" { !conf-gtksourceview:installed }]
[make "-j%{jobs}%" "opt" "byte"] [make "-j%{jobs}%" "all" "opt" "byte"]
] ]
install: [make "install" "install-lib"] install: [make "install" "install-lib"]
......
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