MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

Commit b8420ce8 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files

Merge branch 'master' into mp

parents 927e4802 2f5afda0
......@@ -148,8 +148,7 @@ why3.conf
/share/emacs/semantic.cache
/share/Makefile.config
/share/drivers
/share/modules
/share/theories
/share/stdlib
# /src/
/src/config.sh
......@@ -301,15 +300,6 @@ pvsbin/
/examples/prover/bench1
/examples/prover/bench2
# modules
/modules/string/
/modules/stack/
/modules/queue/
/modules/pqueue/
/modules/mach/array/
/modules/mach/int/
/modules/python/
# Try Why3
/src/trywhy3/trywhy3.byte
/src/trywhy3/trywhy3.js
......
......@@ -315,12 +315,11 @@ install_no_local::
$(MKDIR_P) $(DATADIR)/why3/vim/ftdetect
$(MKDIR_P) $(DATADIR)/why3/vim/syntax
$(MKDIR_P) $(DATADIR)/why3/lang
$(MKDIR_P) $(DATADIR)/why3/theories
$(MKDIR_P) $(DATADIR)/why3/modules/mach
$(MKDIR_P) $(DATADIR)/why3/stdlib
$(MKDIR_P) $(DATADIR)/why3/stdlib/mach
$(MKDIR_P) $(DATADIR)/why3/drivers
$(INSTALL_DATA) theories/*.why $(DATADIR)/why3/theories
$(INSTALL_DATA) modules/*.mlw $(DATADIR)/why3/modules
$(INSTALL_DATA) modules/mach/*.mlw $(DATADIR)/why3/modules/mach
$(INSTALL_DATA) stdlib/*.why stdlib/*.mlw $(DATADIR)/why3/stdlib
$(INSTALL_DATA) stdlib/mach/*.mlw $(DATADIR)/why3/stdlib/mach
$(INSTALL_DATA) drivers/*.drv drivers/*.gen $(DATADIR)/why3/drivers
$(INSTALL_DATA) LICENSE $(DATADIR)/why3/
$(INSTALL_DATA) share/provers-detection-data.conf $(DATADIR)/why3/
......@@ -563,16 +562,13 @@ install_local:: bin/why3 $(addprefix bin/,$(TOOLS_BIN))
bin/%: bin/%.@OCAMLBEST@
ln -sf $(notdir $<) $@
install_local:: share/drivers share/modules share/theories
install_local:: share/drivers share/stdlib
share/drivers:
ln -snf ../drivers share/drivers
share/modules:
ln -snf ../modules share/modules
share/theories:
ln -snf ../theories share/theories
share/stdlib:
ln -snf ../stdlib share/stdlib
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(TOOLSDEP)
......@@ -677,7 +673,7 @@ gallery-subs::
echo "exporting examples/$$d"; \
mkdir -p $(GALLERYDIR)/$$d; \
cd examples/$$d; \
WHY3CONFIG="" ../../bin/why3doc.@OCAMLBEST@ -L ../../theories -L ../../modules -L . --stdlib-url http://why3.lri.fr/stdlib/ *.mlw -o $(GALLERYDIR)/$$d; \
WHY3CONFIG="" ../../bin/why3doc.@OCAMLBEST@ -L ../../stdlib -L . --stdlib-url http://why3.lri.fr/stdlib/ *.mlw -o $(GALLERYDIR)/$$d; \
cd ..; \
rm -f $(GALLERYDIR)/$$d/$$d.zip; \
zip -q -r $(GALLERYDIR)/$$d/$$d.zip $$d; \
......@@ -1095,41 +1091,41 @@ drivers/coq-realizations.aux: Makefile
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-int: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/int.why
for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -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-bool: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/bool.why
for f in $(COQLIBS_BOOL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -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-real: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/real.why
for f in $(COQLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -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-number: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/number.why
for f in $(COQLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -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-set: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/set.why
for f in $(COQLIBS_SET_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -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-map: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/map.why
for f in $(COQLIBS_MAP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -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-list: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/list.why
for f in $(COQLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -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-option: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/option.why
for f in $(COQLIBS_OPTION_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -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-seq: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/seq.why
for f in $(COQLIBS_SEQ_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -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-bv: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/bv.why
for f in $(COQLIBS_BV_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -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-ieee_float: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/ieee_float.why
for f in $(COQLIBS_IEEEFLOAT_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -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
update-coq-fp: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/floating_point.why
for f in $(COQLIBS_FP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T floating_point.$$f -o $(GENERATED_PREFIX_COQ)/floating_point/; done
ifeq (@enable_coq_support@,yes)
......@@ -1260,11 +1256,11 @@ install_no_local::
$(INSTALL_DATA) drivers/pvs-realizations.aux $(DATADIR)/why3/drivers/
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_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_LIST_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/pvs-realize.drv -T list.$$f -o lib/pvs/list/; done
for f in $(PVSLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/pvs-realize.drv -T number.$$f -o lib/pvs/number/; done
for f in $(PVSLIBS_FP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/pvs-realize.drv -T floating_point.$$f -o lib/pvs/floating_point/; done
for f in $(PVSLIBS_INT_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -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 stdlib -D drivers/pvs-realize.drv -T real.$$f -o lib/pvs/real/; done
for f in $(PVSLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/pvs-realize.drv -T list.$$f -o lib/pvs/list/; done
for f in $(PVSLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/pvs-realize.drv -T number.$$f -o lib/pvs/number/; done
for f in $(PVSLIBS_FP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/pvs-realize.drv -T floating_point.$$f -o lib/pvs/floating_point/; done
else
......@@ -1359,58 +1355,58 @@ endif
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
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/int.why
$(SHOW) "Generating Isabelle realization for int.$(notdir $(basename $@))"
$(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/
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -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
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/bool.why
$(SHOW) "Generating Isabelle realization for bool.$(notdir $(basename $@))"
$(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/
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -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
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/real.why
$(SHOW) "Generating Isabelle realization for real.$(notdir $(basename $@))"
$(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/
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -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
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/number.why
$(SHOW) "Generating Isabelle realization for number.$(notdir $(basename $@))"
$(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/
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -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
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/set.why
$(SHOW) "Generating Isabelle realization for set.$(notdir $(basename $@))"
$(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/
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -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
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/map.why
$(SHOW) "Generating Isabelle realization for map.$(notdir $(basename $@))"
$(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/
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -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
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/list.why
$(SHOW) "Generating Isabelle realization for list.$(notdir $(basename $@))"
$(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/
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -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
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/option.why
$(SHOW) "Generating Isabelle realization for option.$(notdir $(basename $@))"
$(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/
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -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
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/bv.why
$(SHOW) "Generating Isabelle realization for bv.$(notdir $(basename $@))"
$(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/
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -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)
......@@ -1668,7 +1664,7 @@ src/trywhy3/trywhy3.byte: src/trywhy3/worker_proto.cmo src/trywhy3/trywhy3.cmo
src/trywhy3/why3_worker.js: src/trywhy3/why3_worker.byte
js_of_ocaml $(JSOO_DEBUG) --extern-fs -I . -I src/trywhy3 --file=trywhy3.conf:/ \
--file=try_alt_ergo.drv:/ \
`find theories modules \( -name "*.mlw" -o -name "*.why" \) -printf " --file=%p:/%p"` \
`find stdlib \( -name "*.mlw" -o -name "*.why" \) -printf " --file=%p:/%p"` \
+weak.js +nat.js $<
src/trywhy3/why3_worker.byte: $(TRYWHY3CMO) src/trywhy3/worker_proto.cmo src/trywhy3/why3_worker.cmo
......@@ -1966,59 +1962,55 @@ install_no_local::
.PHONY: stdlibdoc
STDLIBS = algebra \
bag \
bintree \
bool \
bv \
floating_point \
graph \
int \
ieee_float \
list \
map \
number \
option \
pigeon \
real \
relations \
seq \
set \
sum
STDLIBS = \
algebra.why \
array.mlw \
bag.why \
bintree.why \
bool.why \
bv.why \
floating_point.why \
graph.why \
hashtbl.mlw \
ieee_float.why \
impset.mlw \
int.why \
list.why \
map.why \
matrix.mlw \
number.why \
option.why \
pigeon.why \
pqueue.mlw \
queue.mlw \
random.mlw \
real.why \
ref.mlw \
relations.why \
seq.why \
set.why \
stack.mlw \
string.mlw \
sum.why \
mach/array.mlw \
mach/int.mlw
# function ? tptp ?
STDMODS = array \
hashtbl \
impset \
matrix \
pqueue \
queue \
random \
ref \
stack \
string
STDMACS = array int
STDLIBFILES = $(addsuffix .why, $(addprefix theories/, $(STDLIBS)))
STDMODFILES = $(addsuffix .mlw, $(addprefix modules/, $(STDMODS)))
STDMACFILES = $(addsuffix .mlw, $(addprefix modules/mach/, $(STDMACS)))
STDLIBFILES = $(addprefix stdlib/, $(STDLIBS))
# TODO: remove the hack about int.why once it has become builtin
stdlibdoc: $(STDLIBFILES) $(STDMODFILES) bin/why3doc.@OCAMLBEST@
stdlibdoc: $(STDLIBFILES) bin/why3doc.@OCAMLBEST@
mkdir -p doc/stdlibdoc
sed -e "s/use import Int/use import int.Int/" theories/int.why > int.why
sed -e "s/use import Int/use import int.Int/" stdlib/int.why > int.why
rm -f doc/stdlibdoc/style.css
WHY3CONFIG="" bin/why3doc.@OCAMLBEST@ -L theories -L modules \
WHY3CONFIG="" bin/why3doc.@OCAMLBEST@ -L stdlib \
-o doc/stdlibdoc --title "Why3 Standard Library" \
$(subst theories/int.why,int.why,$(STDLIBFILES)) $(STDMODFILES) $(STDMACFILES)
$(subst stdlib/int.why,int.why,$(STDLIBFILES))
rm int.why
cd doc/stdlibdoc; \
for f in theories.*.html; \
do mv "$$f" "$${f#theories.}"; done; \
for f in modules.*.html; \
do mv "$$f" "$${f#modules.}"; done
sed -i -e "s#theories.##g" -e "s#modules.##g" doc/stdlibdoc/index.html
for f in stdlib.*.html; \
do mv "$$f" "$${f#stdlib.}"; done
sed -i -e "s#stdlib.##g" doc/stdlibdoc/index.html
sed -i -e "s#int\.\(<a href=\"int\.html\)#\1#g" doc/stdlibdoc/int.html
clean::
......
......@@ -26,7 +26,7 @@ The documentation (a tutorial and a reference manual) is in the file
[doc/manual.pdf](http://why3.lri.fr/manual.pdf) or online at
http://why3.lri.fr/doc/.
Various examples can be found in the subdirectories [theories/](theories)
Various examples can be found in the subdirectories [stdlib/](stdlib)
and [examples/](examples).
Mailing list (Why3 Club):
......
#!/bin/bash
# auto bench for why
......@@ -10,17 +9,20 @@
suffix=$1
# TODO: remove the hack about int.why once it has become builtin
goods () {
pgm="bin/why3prove$suffix"
ERROR=
rm -f bench_errors
for f in $1/*.[wm][hl][yw] ; do
printf " $f... "
opts="$2"
if test $f = stdlib/int.why; then opts="$2 --type-only"; fi
# running Why
if ! $pgm $2 $f > /dev/null 2> bench_error; then
if ! $pgm $opts $f > /dev/null 2> bench_error; then
echo "FAILED!"
# echo "env: WHY3DATA='$WHY3DATA'"
echo "invocation: $pgm $2 $f" | tee -a bench_errors
echo "invocation: $pgm $opts $f" | tee -a bench_errors
cat bench_error | tee -a bench_errors
ERROR=yes
elif test -s bench_error; then
......@@ -174,13 +176,9 @@ list_stuff () {
fi
}
echo "=== Checking theories ==="
goods theories --type-only # FIXME remove --type-only
echo ""
echo "=== Checking modules ==="
goods modules
goods modules/mach
echo "=== Checking stdlib ==="
goods stdlib
goods stdlib/mach
echo ""
echo "=== Checking drivers ==="
......
[main ]
loadpath = "../../share/theories"
[main]
loadpath = "../../share/stdlib"
magic = 5
memlimit = 2048
running_provers_max = 7
......
......@@ -8,7 +8,7 @@
<prover id="3" name="Coq" version="8.6.1" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../../../modules/array.mlw" proved="true">
<file name="../../../stdlib/array.mlw" proved="true">
<theory name="Array" proved="true" sum="d12f98c64e888261d80af67de4830724">
<goal name="VC array" expl="VC for array" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="1"/></proof>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../../../theories/bintree.why" expanded="true">
<file name="../../../stdlib/bintree.why" expanded="true">
<theory name="Tree" sum="c05a159c0fca07eac9e3cabdb81061c8">
<goal name="VC is_empty" expl="VC for is_empty">
<transf name="split_goal_wp">
......
......@@ -7,7 +7,7 @@
<prover id="3" name="Spass" version="3.7" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../../../theories/list.why" expanded="true">
<file name="../../../stdlib/list.why" expanded="true">
<theory name="List" sum="0837e0e504ae2d2a2dc07ff388fab3e5">
<goal name="VC is_nil" expl="VC for is_nil">
<proof prover="6"><result status="valid" time="0.00" steps="7"/></proof>
......
......@@ -26,7 +26,7 @@
(defconst why3-font-lock-keywords-1
(list
;; Note: comment font-lock is guaranteed by suitable syntax entries
'("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . font-lock-comment-face)
'("([*][^)]\\([^*]\\|[*][^)]\\)*[*])" . font-lock-comment-face)
; '("{}\\|{[^|]\\([^}]*\\)}" . font-lock-type-face)
`(,(why3-regexp-opt '("invariant" "variant" "diverges" "requires" "ensures" "pure" "returns" "raises" "reads" "writes" "alias" "assert" "assume" "check")) . font-lock-type-face)
`(,(why3-regexp-opt '("use" "clone" "scope" "import" "export" "coinductive" "inductive" "external" "constant" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "abstract" "private" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "for" "to" "downto" "do" "done" "loop" "absurd" "ghost" "raise" "return" "break" "continue" "try" "with" "theory" "uses" "module" "converter" "fun" "at" "old" "true" "false" "forall" "exists" "label" "by" "so" "meta")) . font-lock-keyword-face)
......
......@@ -42,8 +42,7 @@ let why3_regexp_of_string s = (* define a regexp in why3 *)
(* lib and shared dirs *)
let default_loadpath =
[ Filename.concat Config.datadir "theories";
Filename.concat Config.datadir "modules"; ]
[ Filename.concat Config.datadir "stdlib" ]
let default_conf_file =
match Config.localdir with
......@@ -184,7 +183,7 @@ let set_strategies rc strategies =
type main = {
libdir : string; (* "/usr/local/lib/why/" *)
datadir : string; (* "/usr/local/share/why/" *)
loadpath : string list; (* "/usr/local/lib/why/theories" *)
loadpath : string list; (* "/usr/local/lib/why/stdlib" *)
timelimit : int;
(* default prover time limit in seconds (0 unlimited) *)
memlimit : int;
......
......@@ -284,23 +284,11 @@ module Print = struct
Loc.errorm ?loc "Function %a cannot be extracted" Expr.print_rs rs
| _ -> ()
(* a range type that fits in 31-bit sign integers is mapped to type "int" *)
let min_int31 = BigInt.of_string "-1073741824"
let max_int31 = BigInt.of_string "1073741823"
let is_small_range r =
BigInt.le min_int31 r.Number.ir_lower &&
BigInt.le r.Number.ir_upper max_int31
let is_small_range_ity ity = match ity.ity_node with
| Ityapp ({ Ity.its_def = Range r }, _, _) -> is_small_range r
| _ -> false
let is_small_range_type = function
| I ity -> is_small_range_ity ity | C _ -> false
let driver_type_int info ity = match ity.ity_node with
let is_mapped_to_int info ity =
match ity.ity_node with
| Ityapp ({ its_ts = ts }, _, _) ->
query_syntax info.info_syn ts.ts_name = Some "int"
| _ -> false
let is_mapped_to_int info ity =
is_small_range_ity ity || driver_type_int info ity
let print_constant fmt e = begin match e.e_node with
| Econst c ->
......@@ -444,7 +432,6 @@ module Print = struct
| _ -> assert false in
(match query_syntax info.info_literal id with
| Some s -> syntax_arguments s print_constant fmt [e]
| None when is_small_range_type e.e_ity -> pp_print_string fmt n
| None -> fprintf fmt (protect_on paren "Z.of_string \"%s\"") n)
| Evar pvs ->
(print_lident info) fmt (pv_name pvs)
......@@ -602,8 +589,6 @@ module Print = struct
(print_list newline print_field) fl
| Some (Dalias ty) ->
fprintf fmt " =@ %a" (print_ty ~paren:false info) ty
| Some (Drange r) when is_small_range r ->
fprintf fmt " =@ int"
| Some (Drange _) ->
fprintf fmt " =@ Z.t"
| Some (Dfloat _) ->
......
[main]
cntexample = false
loadpath = "/theories"
loadpath = "/modules"
loadpath = "/stdlib"
magic = 14
memlimit = 1000
running_provers_max = 2
......
......@@ -28,33 +28,32 @@ let print_footer fmt () =
let style_css fname =
let c = open_out fname in
output_string c
"\
.why3doc a:visited {color : #416DFF; text-decoration : none; }\
.why3doc a:link {color : #416DFF; text-decoration : none;}\
.why3doc a:hover {color : Red; text-decoration : none; background-color: #5FFF88}\
.why3doc a:active {color : Red; text-decoration : underline; }\
.why3doc .comment { color : #990000 }\
.why3doc .keyword1 { color : purple; font-weight : bold }\
.why3doc .keyword2 { color : blue; font-weight : bold }\
.why3doc .superscript { font-size : 4 }\
.why3doc .subscript { font-size : 4 }\
.why3doc .warning { color : Red ; font-weight : bold }\
.why3doc .info { margin-left : 3em; margin-right : 3em }\
.why3doc .code { color : #465F91 ; }\
.why3doc h1 { font-size : 20pt ; border: 1px solid #000000; margin-top: 10px; margin-bottom: 10px;text-align: center; background-color: #90BDFF ;padding: 10px; }\
.why3doc h2 { font-size : 18pt ; border: 1px solid #000000; margin-top: 8px; margin-bottom: 8px;text-align: left; background-color: #90DDFF ;padding: 8px; }\
.why3doc h3 { font-size : 16pt ; border: 1px solid #000000; margin-top: 6px; margin-bottom: 6px;text-align: left; background-color: #90EDFF ;padding: 6px; }\
.why3doc h4 { font-size : 14pt ; border: 1px solid #000000; margin-top: 4px; margin-bottom: 4px;text-align: left; background-color: #90FDFF ;padding: 4px; }\
.why3doc h5 { font-size : 12pt ; border: 1px solid #000000; margin-top: 2px; margin-bottom: 2px;text-align: left; background-color: #90BDFF ; padding: 2px; }\
.why3doc h6 { font-size : 10pt ; border: 1px solid #000000; margin-top: 0px; margin-bottom: 0px;text-align: left; background-color: #90BDFF ; padding: 0px; }\
.why3doc .typetable { border-style : hidden }\
.why3doc .indextable { border-style : hidden }\
.why3doc .paramstable { border-style : hidden ; padding: 5pt 5pt}\
.why3doc body { background-color : White }\
.why3doc tr { background-color : White }\
.why3doc td.typefieldcomment { background-color : #FFFFFF }\
.why3doc pre { margin-top: 1px ; margin-bottom: 2px; }\
.why3doc div.sig_block {margin-left: 2em}\
";
".why3doc a:visited { color: #416DFF; text-decoration: none }\
\n.why3doc a:link { color: #416DFF; text-decoration: none }\
\n.why3doc a:hover { color: red; text-decoration: none; background-color: #5FFF88 }\
\n.why3doc a:active { color: red; text-decoration: underline }\
\n.why3doc .comment { color: #990000 }\
\n.why3doc .keyword1 { color: purple; font-weight: bold }\
\n.why3doc .keyword2 { color: blue; font-weight: bold }\
\n.why3doc .superscript { font-size: smaller }\
\n.why3doc .subscript { font-size: smaller }\
\n.why3doc .warning { color: red; font-weight: bold }\
\n.why3doc .info { margin-left: 3em; margin-right: 3em }\
\n.why3doc .info > p:first-child { margin-top: 0 }\
\n.why3doc code { color: #465F91 }\
\n.why3doc h1 { font-size: 20pt; border: 1px solid #000000; margin: 10pt 0; text-align: center; background-color: #90BDFF; padding: 10pt }\
\n.why3doc h2 { font-size: 18pt; border: 1px solid #000000; margin: 8pt 0; text-align: left; background-color: #90DDFF; padding: 8pt }\
\n.why3doc h3 { font-size: 15pt; border: 1px solid #000000; margin: 6pt 0; text-align: left; background-color: #90EDFF; padding: 6pt }\
\n.why3doc h4 { font-size: 12pt; border: 1px solid #000000; margin: 4pt 0; text-align: left; background-color: #90FDFF; padding: 4pt }\
\n.why3doc h5 { font-size: 11pt; border: 1px solid #000000; margin: 2pt 0; text-align: left; background-color: #90FEFF; padding: 2pt }\
\n.why3doc h6 { font-size: 10pt; border: 1px solid #000000; margin: 0pt 0; text-align: left; background-color: #90FFFF; padding: 0pt }\
\n.why3doc .typetable { border-style: hidden }\
\n.why3doc .indextable { border-style: hidden }\
\n.why3doc .paramstable { border-style: hidden; padding: 5pt 5pt }\
\n.why3doc body { background-color: white }\
\n.why3doc tr { background-color: white }\
\n.why3doc td.typefieldcomment { background-color: #FFFFFF }\
\n.why3doc pre { margin-top: 0; margin-bottom: 0.5ex }\
\n.why3doc div.sig_block { margin-left: 2em }\
\n";
close_out c
......@@ -226,7 +226,7 @@ module ArrayPermut
M.permut a1.elts a2.elts l u
(** [permut a1 a2 l u] is true when the segment
[a1(l..u-1)] is a permutation of the segment [a2(l..u-1)].
Values outside of the interval (l..u-1) are ignored. *)
Values outside of the interval [(l..u-1)] are ignored. *)
predicate permut_sub (a1 a2: array 'a) (l u: int) =
map_eq_sub a1.elts a2.elts 0 l /\
......@@ -234,7 +234,7 @@ module ArrayPermut
map_eq_sub a1.elts a2.elts u (length a1)
(** [permut_sub a1 a2 l u] is true when the segment
[a1(l..u-1)] is a permutation of the segment [a2(l..u-1)]
and values outside of the interval (l..u-1) are equal. *)
and values outside of the interval [(l..u-1)] are equal. *)
predicate permut_all (a1 a2: array 'a) =
a1.length = a2.length /\ M.permut a1.elts a2.elts 0 a1.length
......@@ -247,14 +247,11 @@ module ArrayPermut
0 <= l -> u <= length a1 -> permut_sub a1 a2 l u
(** we can always enlarge the interval *)
lemma permut_sub_weakening:
forall a1 a2: array 'a, l1 u1 l2 u2: int.
permut_sub a1 a2 l1 u1 -> 0 <= l2 <= l1 -> u1 <= u2 <= length a1 ->
permut_sub a1 a2 l2 u2