Mentions légales du service

Skip to content
Snippets Groups Projects
Commit efb51e7d authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Merge theories and modules into stdlib (fix issue #62).

parent 26335a9a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 114 additions and 136 deletions
.gitignore
+ 1
− 11
View file @ efb51e7d
...@@ -148,8 +148,7 @@ why3.conf ...@@ -148,8 +148,7 @@ why3.conf
/share/emacs/semantic.cache /share/emacs/semantic.cache
/share/Makefile.config /share/Makefile.config
/share/drivers /share/drivers
/share/modules /share/stdlib
/share/theories
# /src/ # /src/
/src/config.sh /src/config.sh
...@@ -301,15 +300,6 @@ pvsbin/ ...@@ -301,15 +300,6 @@ pvsbin/
/examples/prover/bench1 /examples/prover/bench1
/examples/prover/bench2 /examples/prover/bench2
# modules
/modules/string/
/modules/stack/
/modules/queue/
/modules/pqueue/
/modules/mach/array/
/modules/mach/int/
/modules/python/
# Try Why3 # Try Why3
/src/trywhy3/trywhy3.byte /src/trywhy3/trywhy3.byte
/src/trywhy3/trywhy3.js /src/trywhy3/trywhy3.js
......
Makefile.in
+ 96
− 104
View file @ efb51e7d
...@@ -315,12 +315,11 @@ install_no_local:: ...@@ -315,12 +315,11 @@ install_no_local::
$(MKDIR_P) $(DATADIR)/why3/vim/ftdetect $(MKDIR_P) $(DATADIR)/why3/vim/ftdetect
$(MKDIR_P) $(DATADIR)/why3/vim/syntax $(MKDIR_P) $(DATADIR)/why3/vim/syntax
$(MKDIR_P) $(DATADIR)/why3/lang $(MKDIR_P) $(DATADIR)/why3/lang
$(MKDIR_P) $(DATADIR)/why3/theories $(MKDIR_P) $(DATADIR)/why3/stdlib
$(MKDIR_P) $(DATADIR)/why3/modules/mach $(MKDIR_P) $(DATADIR)/why3/stdlib/mach
$(MKDIR_P) $(DATADIR)/why3/drivers $(MKDIR_P) $(DATADIR)/why3/drivers
$(INSTALL_DATA) theories/*.why $(DATADIR)/why3/theories $(INSTALL_DATA) stdlib/*.why stdlib/*.mlw $(DATADIR)/why3/stdlib
$(INSTALL_DATA) modules/*.mlw $(DATADIR)/why3/modules $(INSTALL_DATA) stdlib/mach/*.mlw $(DATADIR)/why3/stdlib/mach
$(INSTALL_DATA) modules/mach/*.mlw $(DATADIR)/why3/modules/mach
$(INSTALL_DATA) drivers/*.drv drivers/*.gen $(DATADIR)/why3/drivers $(INSTALL_DATA) drivers/*.drv drivers/*.gen $(DATADIR)/why3/drivers
$(INSTALL_DATA) LICENSE $(DATADIR)/why3/ $(INSTALL_DATA) LICENSE $(DATADIR)/why3/
$(INSTALL_DATA) share/provers-detection-data.conf $(DATADIR)/why3/ $(INSTALL_DATA) share/provers-detection-data.conf $(DATADIR)/why3/
...@@ -563,16 +562,13 @@ install_local:: bin/why3 $(addprefix bin/,$(TOOLS_BIN)) ...@@ -563,16 +562,13 @@ install_local:: bin/why3 $(addprefix bin/,$(TOOLS_BIN))
bin/%: bin/%.@OCAMLBEST@ bin/%: bin/%.@OCAMLBEST@
ln -sf $(notdir $<) $@ ln -sf $(notdir $<) $@
install_local:: share/drivers share/modules share/theories install_local:: share/drivers share/stdlib
share/drivers: share/drivers:
ln -snf ../drivers share/drivers ln -snf ../drivers share/drivers
share/modules: share/stdlib:
ln -snf ../modules share/modules ln -snf ../stdlib share/stdlib
share/theories:
ln -snf ../theories share/theories
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean" ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(TOOLSDEP) -include $(TOOLSDEP)
...@@ -677,7 +673,7 @@ gallery-subs:: ...@@ -677,7 +673,7 @@ gallery-subs::
echo "exporting examples/$$d"; \ echo "exporting examples/$$d"; \
mkdir -p $(GALLERYDIR)/$$d; \ mkdir -p $(GALLERYDIR)/$$d; \
cd examples/$$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 ..; \ cd ..; \
rm -f $(GALLERYDIR)/$$d/$$d.zip; \ rm -f $(GALLERYDIR)/$$d/$$d.zip; \
zip -q -r $(GALLERYDIR)/$$d/$$d.zip $$d; \ zip -q -r $(GALLERYDIR)/$$d/$$d.zip $$d; \
...@@ -1095,41 +1091,41 @@ drivers/coq-realizations.aux: Makefile ...@@ -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: 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 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 theories -D drivers/coq-realize.drv -T int.$$f -o $(GENERATED_PREFIX_COQ)/int/; done 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 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 theories -D drivers/coq-realize.drv -T bool.$$f -o $(GENERATED_PREFIX_COQ)/bool/; done 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 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 theories -D drivers/coq-realize.drv -T real.$$f -o $(GENERATED_PREFIX_COQ)/real/; done 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 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 theories -D drivers/coq-realize.drv -T number.$$f -o $(GENERATED_PREFIX_COQ)/number/; done 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 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 theories -D drivers/coq-realize.drv -T set.$$f -o $(GENERATED_PREFIX_COQ)/set/; done 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 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 theories -D drivers/coq-realize.drv -T map.$$f -o $(GENERATED_PREFIX_COQ)/map/; done 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 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 theories -D drivers/coq-realize.drv -T list.$$f -o $(GENERATED_PREFIX_COQ)/list/; done 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 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 theories -D drivers/coq-realize.drv -T option.$$f -o $(GENERATED_PREFIX_COQ)/option/; done 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 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 theories -D drivers/coq-realize.drv -T seq.$$f -o $(GENERATED_PREFIX_COQ)/seq/; done 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 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 theories -D drivers/coq-realize.drv -T bv.$$f -o $(GENERATED_PREFIX_COQ)/bv/; done 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 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 theories -D drivers/coq-realize.drv -T ieee_float.$$f -o $(GENERATED_PREFIX_COQ)/ieee_float/; done 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 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 theories -D drivers/coq-realize.drv -T floating_point.$$f -o $(GENERATED_PREFIX_COQ)/floating_point/; done 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) ifeq (@enable_coq_support@,yes)
...@@ -1260,11 +1256,11 @@ install_no_local:: ...@@ -1260,11 +1256,11 @@ install_no_local::
$(INSTALL_DATA) drivers/pvs-realizations.aux $(DATADIR)/why3/drivers/ $(INSTALL_DATA) drivers/pvs-realizations.aux $(DATADIR)/why3/drivers/
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 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 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 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 theories -D drivers/pvs-realize.drv -T list.$$f -o lib/pvs/list/; 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 theories -D drivers/pvs-realize.drv -T number.$$f -o lib/pvs/number/; 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 theories -D drivers/pvs-realize.drv -T floating_point.$$f -o lib/pvs/floating_point/; 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 else
...@@ -1359,58 +1355,58 @@ endif ...@@ -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) 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 \ $(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 $@))" $(SHOW) "Generating Isabelle realization for int.$(notdir $(basename $@))"
$(HIDE)mkdir -p $(GENERATED_PREFIX_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/ $(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 \ $(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 $@))" $(SHOW) "Generating Isabelle realization for bool.$(notdir $(basename $@))"
$(HIDE)mkdir -p $(GENERATED_PREFIX_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/ $(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 \ $(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 $@))" $(SHOW) "Generating Isabelle realization for real.$(notdir $(basename $@))"
$(HIDE)mkdir -p $(GENERATED_PREFIX_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/ $(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 \ $(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 $@))" $(SHOW) "Generating Isabelle realization for number.$(notdir $(basename $@))"
$(HIDE)mkdir -p $(GENERATED_PREFIX_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/ $(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 \ $(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 $@))" $(SHOW) "Generating Isabelle realization for set.$(notdir $(basename $@))"
$(HIDE)mkdir -p $(GENERATED_PREFIX_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/ $(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 \ $(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 $@))" $(SHOW) "Generating Isabelle realization for map.$(notdir $(basename $@))"
$(HIDE)mkdir -p $(GENERATED_PREFIX_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/ $(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 \ $(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 $@))" $(SHOW) "Generating Isabelle realization for list.$(notdir $(basename $@))"
$(HIDE)mkdir -p $(GENERATED_PREFIX_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/ $(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 \ $(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 $@))" $(SHOW) "Generating Isabelle realization for option.$(notdir $(basename $@))"
$(HIDE)mkdir -p $(GENERATED_PREFIX_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/ $(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 \ $(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 $@))" $(SHOW) "Generating Isabelle realization for bv.$(notdir $(basename $@))"
$(HIDE)mkdir -p $(GENERATED_PREFIX_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/ $(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D $(ISABELLEREALIZEDRV) -T bv.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/bv/
$(GENERATED_PREFIX_ISABELLE)/last_build: $(ISABELLEVERSIONSPECIFICTARGETS) $(GENERATED_PREFIX_ISABELLE)/last_build: $(ISABELLEVERSIONSPECIFICTARGETS)
# $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION) $(ISABELLELIBS_BV) # $(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 ...@@ -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 src/trywhy3/why3_worker.js: src/trywhy3/why3_worker.byte
js_of_ocaml $(JSOO_DEBUG) --extern-fs -I . -I src/trywhy3 --file=trywhy3.conf:/ \ js_of_ocaml $(JSOO_DEBUG) --extern-fs -I . -I src/trywhy3 --file=trywhy3.conf:/ \
--file=try_alt_ergo.drv:/ \ --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 $< +weak.js +nat.js $<
src/trywhy3/why3_worker.byte: $(TRYWHY3CMO) src/trywhy3/worker_proto.cmo src/trywhy3/why3_worker.cmo src/trywhy3/why3_worker.byte: $(TRYWHY3CMO) src/trywhy3/worker_proto.cmo src/trywhy3/why3_worker.cmo
...@@ -1966,59 +1962,55 @@ install_no_local:: ...@@ -1966,59 +1962,55 @@ install_no_local::
.PHONY: stdlibdoc .PHONY: stdlibdoc
STDLIBS = algebra \ STDLIBS = \
bag \ algebra.why \
bintree \ array.mlw \
bool \ bag.why \
bv \ bintree.why \
floating_point \ bool.why \
graph \ bv.why \
int \ floating_point.why \
ieee_float \ graph.why \
list \ hashtbl.mlw \
map \ impset.mlw \
number \ int.why \
option \ ieee_float.why \
pigeon \ list.why \
real \ map.why \
relations \ matrix.mlw \
seq \ number.why \
set \ option.why \
sum 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 ? # function ? tptp ?
STDMODS = array \ STDLIBFILES = $(addprefix stdlib/, $(STDLIBS))
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)))
# TODO: remove the hack about int.why once it has become builtin # 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 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 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" \ -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 rm int.why
cd doc/stdlibdoc; \ cd doc/stdlibdoc; \
for f in theories.*.html; \ for f in stdlib.*.html; \
do mv "$$f" "$${f#theories.}"; done; \ do mv "$$f" "$${f#stdlib.}"; done
for f in modules.*.html; \ sed -i -e "s#stdlib.##g" doc/stdlibdoc/index.html
do mv "$$f" "$${f#modules.}"; done
sed -i -e "s#theories.##g" -e "s#modules.##g" doc/stdlibdoc/index.html
sed -i -e "s#int\.\(<a href=\"int\.html\)#\1#g" doc/stdlibdoc/int.html sed -i -e "s#int\.\(<a href=\"int\.html\)#\1#g" doc/stdlibdoc/int.html
clean:: clean::
......
README.md
+ 1
− 1
View file @ efb51e7d
...@@ -26,7 +26,7 @@ The documentation (a tutorial and a reference manual) is in the file ...@@ -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 [doc/manual.pdf](http://why3.lri.fr/manual.pdf) or online at
http://why3.lri.fr/doc/. 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). and [examples/](examples).
Mailing list (Why3 Club): Mailing list (Why3 Club):
......
bench/bench
+ 8
− 10
View file @ efb51e7d
#!/bin/bash #!/bin/bash
# auto bench for why # auto bench for why
...@@ -10,17 +9,20 @@ ...@@ -10,17 +9,20 @@
suffix=$1 suffix=$1
# TODO: remove the hack about int.why once it has become builtin
goods () { goods () {
pgm="bin/why3prove$suffix" pgm="bin/why3prove$suffix"
ERROR= ERROR=
rm -f bench_errors rm -f bench_errors
for f in $1/*.[wm][hl][yw] ; do for f in $1/*.[wm][hl][yw] ; do
printf " $f... " printf " $f... "
opts="$2"
if test $f = stdlib/int.why; then opts="$2 --type-only"; fi
# running Why # 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 "FAILED!"
# echo "env: WHY3DATA='$WHY3DATA'" # 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 cat bench_error | tee -a bench_errors
ERROR=yes ERROR=yes
elif test -s bench_error; then elif test -s bench_error; then
...@@ -174,13 +176,9 @@ list_stuff () { ...@@ -174,13 +176,9 @@ list_stuff () {
fi fi
} }
echo "=== Checking theories ===" echo "=== Checking stdlib ==="
goods theories --type-only # FIXME remove --type-only goods stdlib
echo "" goods stdlib/mach
echo "=== Checking modules ==="
goods modules
goods modules/mach
echo "" echo ""
echo "=== Checking drivers ===" echo "=== Checking drivers ==="
......
bench/encoding/why.conf
+ 2
− 2
View file @ efb51e7d
[main ] [main]
loadpath = "../../share/theories" loadpath = "../../share/stdlib"
magic = 5 magic = 5
memlimit = 2048 memlimit = 2048
running_provers_max = 7 running_provers_max = 7
......
examples/stdlib/array/why3session.xml
+ 1
− 1
View file @ efb51e7d
...@@ -8,7 +8,7 @@ ...@@ -8,7 +8,7 @@
<prover id="3" name="Coq" version="8.6.1" timelimit="6" steplimit="0" memlimit="1000"/> <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="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"/> <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"> <theory name="Array" proved="true" sum="d12f98c64e888261d80af67de4830724">
<goal name="VC array" expl="VC for array" proved="true"> <goal name="VC array" expl="VC for array" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="1"/></proof> <proof prover="2"><result status="valid" time="0.00" steps="1"/></proof>
......
examples/stdlib/bintree/why3session.xml
+ 1
− 1
View file @ efb51e7d
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/> <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"/> <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"> <theory name="Tree" sum="c05a159c0fca07eac9e3cabdb81061c8">
<goal name="VC is_empty" expl="VC for is_empty"> <goal name="VC is_empty" expl="VC for is_empty">
<transf name="split_goal_wp"> <transf name="split_goal_wp">
......
examples/stdlib/list/why3session.xml
+ 1
− 1
View file @ efb51e7d
...@@ -7,7 +7,7 @@ ...@@ -7,7 +7,7 @@
<prover id="3" name="Spass" version="3.7" timelimit="5" steplimit="0" memlimit="1000"/> <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="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"/> <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"> <theory name="List" sum="0837e0e504ae2d2a2dc07ff388fab3e5">
<goal name="VC is_nil" expl="VC for is_nil"> <goal name="VC is_nil" expl="VC for is_nil">
<proof prover="6"><result status="valid" time="0.00" steps="7"/></proof> <proof prover="6"><result status="valid" time="0.00" steps="7"/></proof>
......
src/driver/whyconf.ml
+ 2
− 3
View file @ efb51e7d
...@@ -42,8 +42,7 @@ let why3_regexp_of_string s = (* define a regexp in why3 *) ...@@ -42,8 +42,7 @@ let why3_regexp_of_string s = (* define a regexp in why3 *)
(* lib and shared dirs *) (* lib and shared dirs *)
let default_loadpath = let default_loadpath =
[ Filename.concat Config.datadir "theories"; [ Filename.concat Config.datadir "stdlib" ]
Filename.concat Config.datadir "modules"; ]
let default_conf_file = let default_conf_file =
match Config.localdir with match Config.localdir with
...@@ -184,7 +183,7 @@ let set_strategies rc strategies = ...@@ -184,7 +183,7 @@ let set_strategies rc strategies =
type main = { type main = {
libdir : string; (* "/usr/local/lib/why/" *) libdir : string; (* "/usr/local/lib/why/" *)
datadir : string; (* "/usr/local/share/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; timelimit : int;
(* default prover time limit in seconds (0 unlimited) *) (* default prover time limit in seconds (0 unlimited) *)
memlimit : int; memlimit : int;
......
src/trywhy3/trywhy3.conf
+ 1
− 2
View file @ efb51e7d
[main] [main]
cntexample = false cntexample = false
loadpath = "/theories" loadpath = "/stdlib"
loadpath = "/modules"
magic = 14 magic = 14
memlimit = 1000 memlimit = 1000
running_provers_max = 2 running_provers_max = 2
......
theories/algebra.why → stdlib/algebra.why
+ 0
− 0
View file @ efb51e7d
File moved
modules/appmap.mlw → stdlib/appmap.mlw
+ 0
− 0
View file @ efb51e7d
File moved
modules/appset.mlw → stdlib/appset.mlw
+ 0
− 0
View file @ efb51e7d
File moved
modules/array.mlw → stdlib/array.mlw
+ 0
− 0
View file @ efb51e7d
File moved
theories/bag.why → stdlib/bag.why
+ 0
− 0
View file @ efb51e7d
File moved
theories/bintree.why → stdlib/bintree.why
+ 0
− 0
View file @ efb51e7d
File moved
theories/bool.why → stdlib/bool.why
+ 0
− 0
View file @ efb51e7d
File moved
theories/bv.why → stdlib/bv.why
+ 0
− 0
View file @ efb51e7d
File moved
modules/cursor.mlw → stdlib/cursor.mlw
+ 0
− 0
View file @ efb51e7d
File moved
modules/exn.mlw → stdlib/exn.mlw
+ 0
− 0
View file @ efb51e7d
File moved
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment