Commit 301e8ad9 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Merge branch 'new_ide'

parents 18e48e16 e193469f
:x: marks a potential source of incompatibility
Version 0.88.2, December 7, 2017
--------------------------------
Bug fixes
* `why3 session html`: improved compliance of generated files
* `why3 doc`: fixed missing anchors for operator definitions
* improved build process when `coqtop.byte` is missing
Version 0.88.1, November 6, 2017
--------------------------------
......@@ -8,7 +16,7 @@ API
Provers
* improved support for Isabelle 2017
* fixed support for Coq 8.7
* fixed support for Coq 8.7 (released Oct 17, 2017)
Miscellaneous
* fixed compilation for OCaml 4.06
......@@ -34,16 +42,16 @@ Standard library
compliant to IEEE-754, mapped to SMT-LIB FP theory.
User features
* proof strategies: why3 config now generates default proof strategies
* proof strategies: `why3 config` now generates default proof strategies
using the installed provers. These are available under name "Auto
level 0", "Auto level 1" and "Auto level 2" in why3 ide.
level 0", "Auto level 1" and "Auto level 2" in `why3 ide`.
More details in the manual, section 10.6 "Proof Strategies".
* counterexamples: better support for array values, support for
floating-point values, support for Z3 in addition to CVC4.
More details in the manual, section 6.3.5 "Displaying Counterexamples".
Provers
* support for Isabelle 2017
* support for Isabelle 2017 (released Oct 2017)
* discarded support for Isabelle 2016 (2016-1 still supported) :x:
* support for Coq 8.6.1 (released Jul 25, 2017)
* tentative support for Coq 8.7
......@@ -89,7 +97,7 @@ Language
Tools
* added a command-line option `--extra-expl-prefix` to specify
additional possible prefixes for VC explanations. Available for
why3 commands `prove` and `ide`.
`why3` commands `prove` and `ide`.
* removed `jstree` style from the `session` command :x:
Transformations
......@@ -158,7 +166,7 @@ Provers
* support for Gappa 1.2 (released May 19, 2015)
Bug fixes
* why3doc: garbled output
* `why3doc`: garbled output
Version 0.86, May 11, 2015
--------------------------
......
......@@ -124,6 +124,10 @@ COMPILED_LIB_EXTS = $(INSTALLED_LIB_EXTS) o cmo cmt cmti annot dep conflicts
TOTARGET = > "$@" || (RV=$$?; rm -f "$@"; exit $${RV})
# Variables added for checking realizations
GENERATED_PREFIX_COQ="lib/coq"
GENERATED_PREFIX_ISABELLE="lib/isabelle"
###############
# main target
###############
......@@ -183,7 +187,7 @@ LIB_MLW = ity expr pdecl eval_match typeinv vc pmodule dexpr \
LIB_PARSER = ptree glob typing parser lexer
LIB_TRANSFORM = simplify_formula inlining split_goal induction \
LIB_TRANSFORM = simplify_formula inlining split_goal \
detect_polymorphism reduction_engine compute \
eliminate_definition eliminate_algebraic \
eliminate_inductive eliminate_let eliminate_if \
......@@ -195,9 +199,10 @@ LIB_TRANSFORM = simplify_formula inlining split_goal induction \
eliminate_epsilon intro_projections_counterexmp \
intro_vc_vars_counterexmp prepare_for_counterexmp \
instantiate_predicate smoke_detector \
induction_pr prop_curry eliminate_literal \
prop_curry eliminate_literal \
args_wrapper generic_arg_trans_utils case apply \
ind_itp destruct cut
ind_itp destruct cut \
induction induction_pr
LIB_PRINTER = cntexmp_printer alt_ergo why3printer smtv1 smtv2 coq\
pvs isabelle \
......@@ -294,10 +299,13 @@ GENERATED += $(LIBGENERATED)
clean_old_install::
rm -rf $(LIBDIR)/why3
rm -rf $(DATADIR)/why3
rm -rf $(OCAMLINSTALLLIB)/why3
clean_old_install-lib::
if test -d $(OCAMLINSTALLLIB) -a -w $(OCAMLINSTALLLIB); then \
rm -f $(OCAMLINSTALLLIB)/why3; \
fi
install_no_local:: clean_old_install
install_no_local::
$(MKDIR_P) $(BINDIR)
$(MKDIR_P) $(LIBDIR)/why3
$(MKDIR_P) $(TOOLDIR)
......@@ -340,7 +348,7 @@ install install-lib:
@echo "To install Why3, run ./configure --disable-local ; make ; make install"
else
install: clean_old_install install_no_local
install-lib: install_no_local_lib
install-lib: clean_old_install-lib install_no_local_lib
endif
install-all: install install-lib
......@@ -349,7 +357,12 @@ install-all: install install-lib
# Uninstallation
##################
uninstall: clean_old_install
ifeq (@enable_local@,yes)
uninstall:
@echo "Why3 is configured in local installation mode."
else
uninstall: clean_old_install clean_old_install-lib
endif
##################
# Why3 emacs mode
......@@ -678,7 +691,7 @@ gallery-subs::
d=`dirname $$x`; \
f=`basename $$d`; \
echo "exporting $$f"; \
rm $$d/*.bak; \
rm -f $$d/*.bak; \
mkdir -p $(GALLERYDIR)/$$f; \
WHY3CONFIG="" bin/why3session.@OCAMLBEST@ html $$d -o $(GALLERYDIR)/$$f; \
if test -f examples/$$f.mlw; then cp examples/$$f.mlw $(GALLERYDIR)/$$f/; fi; \
......@@ -985,11 +998,6 @@ endif
# Coq realizations
####################
ifeq (@enable_coq_support@,yes)
ifeq (@enable_coq_libs@,yes)
COQVERSIONSPECIFIC=
COQVERSIONSPECIFICTARGETS=$(addprefix lib/coq/, $(COQVERSIONSPECIFIC))
......@@ -1085,6 +1093,49 @@ drivers/coq-realizations.aux: Makefile
echo 'theory floating_point.'"$$f"' meta "realized_theory" "floating_point.'"$$f"'", "" end'; done; \
) > $@
update-coq: update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp update-coq-seq update-coq-bv update-coq-ieee_float
update-coq-int: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/int.why
for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T int.$$f -o $(GENERATED_PREFIX_COQ)/int/; done
update-coq-bool: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/bool.why
for f in $(COQLIBS_BOOL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T bool.$$f -o $(GENERATED_PREFIX_COQ)/bool/; done
update-coq-real: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/real.why
for f in $(COQLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T real.$$f -o $(GENERATED_PREFIX_COQ)/real/; done
update-coq-number: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/number.why
for f in $(COQLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T number.$$f -o $(GENERATED_PREFIX_COQ)/number/; done
update-coq-set: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/set.why
for f in $(COQLIBS_SET_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T set.$$f -o $(GENERATED_PREFIX_COQ)/set/; done
update-coq-map: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/map.why
for f in $(COQLIBS_MAP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T map.$$f -o $(GENERATED_PREFIX_COQ)/map/; done
update-coq-list: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/list.why
for f in $(COQLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T list.$$f -o $(GENERATED_PREFIX_COQ)/list/; done
update-coq-option: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/option.why
for f in $(COQLIBS_OPTION_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T option.$$f -o $(GENERATED_PREFIX_COQ)/option/; done
update-coq-seq: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/seq.why
for f in $(COQLIBS_SEQ_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T seq.$$f -o $(GENERATED_PREFIX_COQ)/seq/; done
update-coq-bv: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/bv.why
for f in $(COQLIBS_BV_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T bv.$$f -o $(GENERATED_PREFIX_COQ)/bv/; done
update-coq-ieee_float: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/ieee_float.why
for f in $(COQLIBS_IEEEFLOAT_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T ieee_float.$$f -o $(GENERATED_PREFIX_COQ)/ieee_float/; done
update-coq-fp: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/floating_point.why
for f in $(COQLIBS_FP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T floating_point.$$f -o $(GENERATED_PREFIX_COQ)/floating_point/; done
ifeq (@enable_coq_support@,yes)
ifeq (@enable_coq_libs@,yes)
install_no_local::
$(MKDIR_P) $(LIBDIR)/why3/coq
$(INSTALL_DATA) lib/coq/BuiltIn.vo lib/coq/HighOrd.vo $(LIBDIR)/why3/coq/
......@@ -1115,52 +1166,6 @@ ifeq (@enable_coq_fp_libs@,yes)
$(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_IEEEFLOAT)) $(LIBDIR)/why3/coq/ieee_float/
endif
update-coq: update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp update-coq-seq update-coq-bv update-coq-ieee_float
update-coq-int: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/int.why
for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done
update-coq-bool: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/bool.why
for f in $(COQLIBS_BOOL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T bool.$$f -o lib/coq/bool/; done
update-coq-real: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/real.why
for f in $(COQLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T real.$$f -o lib/coq/real/; done
update-coq-number: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/number.why
for f in $(COQLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T number.$$f -o lib/coq/number/; done
update-coq-set: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/set.why
for f in $(COQLIBS_SET_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T set.$$f -o lib/coq/set/; done
update-coq-map: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/map.why
for f in $(COQLIBS_MAP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T map.$$f -o lib/coq/map/; done
update-coq-list: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/list.why
for f in $(COQLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T list.$$f -o lib/coq/list/; done
update-coq-option: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/option.why
for f in $(COQLIBS_OPTION_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T option.$$f -o lib/coq/option/; done
update-coq-seq: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/seq.why
for f in $(COQLIBS_SEQ_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T seq.$$f -o lib/coq/seq/; done
update-coq-bv: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/bv.why
for f in $(COQLIBS_BV_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T bv.$$f -o lib/coq/bv/; done
update-coq-ieee_float: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/ieee_float.why
for f in $(COQLIBS_IEEEFLOAT_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T ieee_float.$$f -o lib/coq/ieee_float/; done
update-coq-fp: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/floating_point.why
for f in $(COQLIBS_FP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T floating_point.$$f -o lib/coq/floating_point/; done
else
drivers/coq-realizations.aux: Makefile
$(SHOW) 'Generate $@'
$(HIDE)echo "(* generated automatically at compilation time *)" > $@
COQLIBS_FILES = lib/coq/BuiltIn lib/coq/HighOrd
endif
COQV = $(addsuffix .v, $(COQLIBS_FILES))
......@@ -1190,12 +1195,6 @@ clean-coq:
clean:: clean-coq
else
drivers/coq-realizations.aux: Makefile
$(SHOW) 'Generate $@'
$(HIDE)echo "(* generated automatically at compilation time *)" > $@
endif
all: drivers/coq-realizations.aux
......@@ -1287,7 +1286,6 @@ clean::
# Isabelle realizations
#######################
ifeq (@enable_isabelle_libs@,yes)
ISABELLEVERSIONSPECIFIC=ROOT why3.ML Why3_BV.thy Why3_Number.thy Why3_Real.thy Why3_Set.thy
......@@ -1358,98 +1356,111 @@ else
ISABELLE_TARGET_DIR=$(LIBDIR)/why3/isabelle
endif
lib/isabelle/last_build: $(ISABELLEVERSIONSPECIFICTARGETS) $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION) $(ISABELLELIBS_BV)
ifneq (@enable_local@,yes)
cp -r lib/isabelle "$(LIBDIR)/why3"
endif
@(if isabelle components -l | grep -q "$(ISABELLE_TARGET_DIR)$$"; then \
echo "Building the Why3 heap for Isabelle/HOL:"; \
isabelle build -bc Why3; \
touch $@; \
else \
echo "[Warning] Cannot pre-build the Isabelle heap because"; \
echo " the Isabelle component configuration does not contain"; \
echo " [$(ISABELLE_TARGET_DIR)]"; \
fi)
install_no_local::
$(INSTALL_DATA) drivers/isabelle-realizations.aux $(DATADIR)/why3/drivers/
install_no_local:: lib/isabelle/last_build
install_local:: lib/isabelle/last_build
update-isabelle: $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION) $(ISABELLELIBS_BV)
$(ISABELLELIBS_INT): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/int.why
$(SHOW) "Generating Isabelle realization for int.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/int
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T int.$(notdir $(basename $@)) -o lib/isabelle/int/
$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/int
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T int.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/int/
$(ISABELLELIBS_BOOL): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/bool.why
$(SHOW) "Generating Isabelle realization for bool.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/bool
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T bool.$(notdir $(basename $@)) -o lib/isabelle/bool/
$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/bool
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T bool.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/bool/
$(ISABELLELIBS_REAL): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/real.why
$(SHOW) "Generating Isabelle realization for real.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/real
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T real.$(notdir $(basename $@)) -o lib/isabelle/real/
$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/real
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T real.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/real/
$(ISABELLELIBS_NUMBER): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/number.why
$(SHOW) "Generating Isabelle realization for number.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/number
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T number.$(notdir $(basename $@)) -o lib/isabelle/number/
$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/number
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T number.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/number/
$(ISABELLELIBS_SET): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/set.why
$(SHOW) "Generating Isabelle realization for set.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/set
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T set.$(notdir $(basename $@)) -o lib/isabelle/set/
$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/set
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T set.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/set/
$(ISABELLELIBS_MAP): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/map.why
$(SHOW) "Generating Isabelle realization for map.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/map
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T map.$(notdir $(basename $@)) -o lib/isabelle/map/
$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/map
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T map.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/map/
$(ISABELLELIBS_LIST): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/list.why
$(SHOW) "Generating Isabelle realization for list.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/list
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T list.$(notdir $(basename $@)) -o lib/isabelle/list/
$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/list
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T list.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/list/
$(ISABELLELIBS_OPTION): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/option.why
$(SHOW) "Generating Isabelle realization for option.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/option
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T option.$(notdir $(basename $@)) -o lib/isabelle/option/
$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/option
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T option.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/option/
$(ISABELLELIBS_BV): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/bv.why
$(SHOW) "Generating Isabelle realization for bv.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/bv
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T bv.$(notdir $(basename $@)) -o lib/isabelle/bv/
$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/bv
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T bv.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/bv/
$(GENERATED_PREFIX_ISABELLE)/last_build: $(ISABELLEVERSIONSPECIFICTARGETS)
# $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION) $(ISABELLELIBS_BV)
ifeq (@enable_isabelle_libs@,yes)
ifneq (@enable_local@,yes)
cp -r $(GENERATED_PREFIX_ISABELLE) "$(LIBDIR)/why3"
endif
@(if isabelle components -l | grep -q "$(ISABELLE_TARGET_DIR)$$"; then \
echo "Building the Why3 heap for Isabelle/HOL:"; \
isabelle build -bc Why3; \
touch $@; \
else \
echo "[Warning] Cannot pre-build the Isabelle heap because"; \
echo " the Isabelle component configuration does not contain"; \
echo " [$(ISABELLE_TARGET_DIR)]"; \
fi)
install_no_local::
$(INSTALL_DATA) drivers/isabelle-realizations.aux $(DATADIR)/why3/drivers/
install_no_local:: $(GENERATED_PREFIX_ISABELLE)/last_build
install_local:: $(GENERATED_PREFIX_ISABELLE)/last_build
# do not update isabelle realizations systematically
# all: update-isabelle
clean::
rm -f lib/isabelle/*/*.xml
# Removed cleaning of xml
#clean::
# rm -f $(GENERATED_PREFIX_ISABELLE)/*/*.xml
else
drivers/isabelle-realizations.aux: Makefile
$(SHOW) 'Generate $@'
$(HIDE)echo "(* generated automatically at compilation time *)" > $@
install_no_local::
$(INSTALL_DATA) drivers/isabelle-realizations.aux $(DATADIR)/why3/drivers/
install_no_local:: $(GENERATED_PREFIX_ISABELLE)/last_build
install_local:: $(GENERATED_PREFIX_ISABELLE)/last_build
# do not update isabelle realizations systematically
# all: update-isabelle
# Removed cleaning of xml
#clean::
# rm -f $(GENERATED_PREFIX_ISABELLE)/*/*.xml
endif
all: drivers/isabelle-realizations.aux
......@@ -1927,10 +1938,6 @@ doc/apidoc/dg.svg: doc/apidoc/dg.dot
doc/apidoc/dg.png: doc/apidoc/dg.dot
dot -T png $< > $@
# what is this ? api doc is in why3.lri.fr/api instead...
# install_apidoc: apidoc
# rsync -av doc/apidoc/ marche@scm.gforge.inria.fr:/home/groups/why3/htdocs/apidoc/
doc/apidoc.tex: $(FILESTODOC)
$(OCAMLDOC) -o doc/apidoc.tex -latex -noheader -notrailer $(INCLUDES) \
$(LIBINCLUDES) -I lib/why3 $(FILESTODOC)
......@@ -1939,11 +1946,13 @@ clean::
rm -f doc/apidoc/*
##########
# Install rules that require root, and thus appear last in the file!
# Install rules for bash completions
##########
clean_old_install::
if test -d /etc/bash_completion.d -a -w /etc/bash_completion.d; then rm -f /etc/bash_completion.d/why3; fi
if test -d /etc/bash_completion.d -a -w /etc/bash_completion.d; then \
rm -f /etc/bash_completion.d/why3; \
fi
install_no_local::
if test -d /etc/bash_completion.d -a -w /etc/bash_completion.d; then \
......
......@@ -121,7 +121,7 @@
* check/update the content of the About dialog in src/ide/gconfig.ml
around lines 550-600
* check headers
* check the file CHANGES, add the release date
* check the file CHANGES.md, add the release date
* generate documentation
- update the date in doc/manual.tex (near \whyversion{})
......@@ -158,9 +158,6 @@
- make (to check validity)
- make export
* add a new version to the bugtracker:
https://gforge.inria.fr/tracker/admin/?group_id=2990&atid=10293&add_extrafield=1
* The next commit : add +git to the version in file Version
* prepare the OPAM package
......
......@@ -665,15 +665,19 @@ fi
# Isabelle
# Default version used for generation of realization in the case Isabelle is not
# detected or Why3 is compiled with disable-isabelle.
ISABELLEVERSION=2017
if test "$enable_isabelle_libs" = no; then
enable_isabelle_support=no
reason_isabelle_support=" (disabled by user)"
else
AC_CHECK_PROG(ISABELLE,isabelle,isabelle,no)
if test "$ISABELLE" = no ; then
enable_isabelle_support=no
AC_MSG_WARN(Cannot find isabelle.)
reason_isabelle_support=" (isabelle not found)"
enable_isabelle_support=no
AC_MSG_WARN(Cannot find isabelle.)
reason_isabelle_support=" (isabelle not found)"
else
AC_MSG_CHECKING(Isabelle version)
ISABELLEDETECTEDVERSION=`$ISABELLE version | sed -n -e 's|Isabelle\([[^:]]*\).*$|\1|p' `
......
......@@ -108,7 +108,7 @@
%BEGIN LATEX
\begin{LARGE}
%END LATEX
Version \whyversion{}, November 2017
Version \whyversion{}, December 2017
%BEGIN LATEX
\end{LARGE}
%END LATEX
......
......@@ -2,30 +2,36 @@
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require bool.Bool.
Require int.Int.
Require map.Map.
Require list.List.
Require list.Length.
Require list.Mem.
Require list.Append.
(* Why3 assumption *)
Inductive datatype :=
| TYunit : datatype
| TYint : datatype
| TYbool : datatype .
Inductive datatype :=
| TYunit : datatype
| TYint : datatype
| TYbool : datatype.
Axiom datatype_WhyType : WhyType datatype.
Existing Instance datatype_WhyType.
(* Why3 assumption *)
Inductive value :=
| Vvoid : value
| Vint : Z -> value
| Vbool : bool -> value .
Inductive value :=
| Vvoid : value
| Vint : Z -> value
| Vbool : bool -> value.
Axiom value_WhyType : WhyType value.
Existing Instance value_WhyType.
(* Why3 assumption *)
Inductive operator :=
| Oplus : operator
| Ominus : operator
| Omult : operator
| Ole : operator .
Inductive operator :=
| Oplus : operator
| Ominus : operator
| Omult : operator
| Ole : operator.
Axiom operator_WhyType : WhyType operator.
Existing Instance operator_WhyType.
......@@ -43,77 +49,43 @@ Existing Instance ident_WhyType.
Axiom ident_decide : forall (m1:ident) (m2:ident), (m1 = m2) \/ ~ (m1 = m2).
(* Why3 assumption *)
Inductive term :=
| Tvalue : value -> term
| Tvar : ident -> term
| Tderef : mident -> term
| Tbin : term -> operator -> term -> term .
Inductive term :=
| Tvalue : value -> term
| Tvar : ident -> term
| Tderef : mident -> term
| Tbin : term -> operator -> term -> term.
Axiom term_WhyType : WhyType term.
Existing Instance term_WhyType.
(* Why3 assumption *)
Inductive fmla :=
| Fterm : term -> fmla
| Fand : fmla -> fmla -> fmla
| Fnot : fmla -> fmla
| Fimplies : fmla -> fmla -> fmla
| Flet : ident -> term -> fmla -> fmla
| Fforall : ident -> datatype -> fmla -> fmla .
Inductive fmla :=
| Fterm : term -> fmla
| Fand : fmla -> fmla -> fmla
| Fnot : fmla -> fmla
| Fimplies : fmla -> fmla -> fmla
| Flet : ident -> term -> fmla -> fmla
| Fforall : ident -> datatype -> fmla -> fmla.
Axiom fmla_WhyType : WhyType fmla.
Existing Instance fmla_WhyType.
(* Why3 assumption *)
Inductive stmt :=
| Sskip : stmt
| Sassign : mident -> term -> stmt
| Sseq : stmt -> stmt -> stmt
| Sif : term -> stmt -> stmt -> stmt
| Sassert : fmla -> stmt
| Swhile : term -> fmla -> stmt -> stmt .
Inductive stmt :=
| Sskip : stmt
| Sassign : mident -> term -> stmt
| Sseq : stmt -> stmt -> stmt
| Sif : term -> stmt -> stmt -> stmt
| Sassert : fmla -> stmt
| Swhile : term -> fmla -> stmt -> stmt.
Axiom stmt_WhyType : WhyType stmt.
Existing Instance stmt_WhyType.
Axiom decide_is_skip : forall (s:stmt), (s = Sskip) \/ ~ (s = Sskip).
Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type.
Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b}, WhyType (map a b).
Existing Instance map_WhyType.