Commit 2c4af0a1 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'split'

parents 4b57ce11 01cafd39
......@@ -51,6 +51,9 @@ why3.conf
/bin/why3.byte
/bin/why3.opt
/bin/why3
/bin/why3contraption.byte
/bin/why3contraption.opt
/bin/why3contraption
/bin/why3ide.byte
/bin/why3ide.opt
/bin/why3ide
......@@ -63,15 +66,21 @@ why3.conf
/bin/why3doc.byte
/bin/why3doc.opt
/bin/why3doc
/bin/why3replayer.byte
/bin/why3replayer.opt
/bin/why3replayer
/bin/why3html.byte
/bin/why3html.opt
/bin/why3html
/bin/why3stats.byte
/bin/why3stats.opt
/bin/why3stats
/bin/why3extract.byte
/bin/why3extract.opt
/bin/why3extract
/bin/why3execute.byte
/bin/why3execute.opt
/bin/why3execute
/bin/why3prove.byte
/bin/why3prove.opt
/bin/why3prove
/bin/why3realize.byte
/bin/why3realize.opt
/bin/why3realize
/bin/why3replay.byte
/bin/why3replay.opt
/bin/why3replay
/bin/why3session.opt
/bin/why3session.byte
/bin/why3session
......
......@@ -28,6 +28,7 @@ BINDIR = $(DESTDIR)@bindir@
LIBDIR = $(DESTDIR)@libdir@
DATADIR = $(DESTDIR)@datarootdir@
MANDIR = $(DESTDIR)@mandir@
TOOLDIR = $(LIBDIR)/why3/commands
# OS specific stuff
EXE = @EXE@
......@@ -240,6 +241,7 @@ install_no_local:: clean_old_install $(TARGET_EMACS)
endif
mkdir -p $(BINDIR)
mkdir -p $(LIBDIR)/why3
mkdir -p $(TOOLDIR)
mkdir -p $(DATADIR)/why3
mkdir -p $(DATADIR)/why3/images
mkdir -p $(DATADIR)/why3/images/boomy
......@@ -421,41 +423,164 @@ install_no_local::
# Why3
######
src/main.cmo: lib/why3/why3.cma
src/main.cmx: lib/why3/why3.cmxa
src/tools/main.cmo: lib/why3/why3.cma
src/tools/main.cmx: lib/why3/why3.cmxa
byte: bin/why3.byte
opt: bin/why3.opt
src/tools/why3contraption.cmo: lib/why3/why3.cma
src/tools/why3contraption.cmx: lib/why3/why3.cmxa
bin/why3.opt: lib/why3/why3.cmxa src/main.cmx
byte: bin/why3.byte bin/why3contraption.byte
opt: bin/why3.opt bin/why3contraption.opt
bin/why3.opt: lib/why3/why3.cmxa src/tools/main.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3.byte: lib/why3/why3.cma src/main.cmo
bin/why3.byte: lib/why3/why3.cma src/tools/main.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
bin/why3: bin/why3.@OCAMLBEST@
ln -sf why3.@OCAMLBEST@ $@
bin/why3contraption.opt: lib/why3/why3.cmxa src/tools/why3contraption.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3contraption.byte: lib/why3/why3.cma src/tools/why3contraption.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
bin/why3contraption: bin/why3contraption.@OCAMLBEST@
ln -sf why3contraption.@OCAMLBEST@ $@
clean_old_install::
rm -f $(BINDIR)/why3$(EXE)
rm -f $(BINDIR)/why3$(EXE) $(BINDIR)/why3contraption$(EXE)
install_no_local::
cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE)
cp -f bin/why3contraption.@OCAMLBEST@ $(BINDIR)/why3contraption$(EXE)
install_local:: bin/why3
install_local:: bin/why3 bin/why3contraption
ifneq "$(MAKECMDGOALS)" "clean"
include src/main.dep
include src/tools/main.dep
include src/tools/why3contraption.dep
include src/tools/why3prove.dep
endif
depend: src/main.dep
depend: src/tools/main.dep src/tools/why3contraption.dep
clean::
rm -f src/main.cm[iox] src/main.annot src/main.o src/main.dep
rm -f src/tools/main.cm[iox] src/tools/main.annot src/tools/main.o src/tools/main.dep
rm -f src/tools/why3contraption.cm[iox] src/tools/why3contraption.annot src/tools/why3contraption.o src/tools/why3contraption.dep
rm -f bin/why3.byte bin/why3.opt bin/why3
rm -f bin/why3ml.byte bin/why3ml.opt bin/why3ml
rm -f bin/why3contraption.byte bin/why3contraption.opt bin/why3contraption
###############
# Why3 commands
###############
TOOLS_BIN = why3execute why3extract why3prove why3realize why3replay
TOOLS_FILES = args $(TOOLS_BIN)
TOOLSMODULES = $(addprefix src/tools/, $(TOOLS_FILES))
TOOLSDEP = $(addsuffix .dep, $(TOOLSMODULES))
TOOLSCMO = $(addsuffix .cmo, $(TOOLSMODULES))
TOOLSCMX = $(addsuffix .cmx, $(TOOLSMODULES))
$(TOOLSDEP): DEPFLAGS += -I src/tools
$(TOOLSCMO) $(TOOLSCMX): INCLUDES += -I src/tools
byte: $(TOOLS_BIN:%=bin/%.byte)
opt: $(TOOLS_BIN:%=bin/%.opt)
bin/why3execute.opt: lib/why3/why3.cmxa src/tools/args.cmx src/tools/why3execute.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3execute.byte: lib/why3/why3.cma src/tools/args.cmo src/tools/why3execute.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
bin/why3execute: bin/why3execute.@OCAMLBEST@
ln -sf why3execute.@OCAMLBEST@ $@
bin/why3extract.opt: lib/why3/why3.cmxa src/tools/args.cmx src/tools/why3extract.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3extract.byte: lib/why3/why3.cma src/tools/args.cmo src/tools/why3extract.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
bin/why3extract: bin/why3extract.@OCAMLBEST@
ln -sf why3extract.@OCAMLBEST@ $@
bin/why3prove.opt: lib/why3/why3.cmxa src/tools/args.cmx src/tools/why3prove.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3prove.byte: lib/why3/why3.cma src/tools/args.cmo src/tools/why3prove.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
bin/why3prove: bin/why3prove.@OCAMLBEST@
ln -sf why3prove.@OCAMLBEST@ $@
bin/why3realize.opt: lib/why3/why3.cmxa src/tools/args.cmx src/tools/why3realize.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3realize.byte: lib/why3/why3.cma src/tools/args.cmo src/tools/why3realize.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
bin/why3realize: bin/why3realize.@OCAMLBEST@
ln -sf why3realize.@OCAMLBEST@ $@
bin/why3replay.opt: lib/why3/why3.cmxa src/tools/args.cmx src/tools/why3replay.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3replay.byte: lib/why3/why3.cma src/tools/args.cmo src/tools/why3replay.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
bin/why3replay: bin/why3replay.@OCAMLBEST@
ln -sf why3replay.@OCAMLBEST@ $@
clean_old_install::
rm -f $(TOOLS_BIN:%=$(TOOLDIR)/%$(EXE))
install_no_local::
cp -f bin/why3execute.@OCAMLBEST@ $(TOOLDIR)/why3execute$(EXE)
cp -f bin/why3extract.@OCAMLBEST@ $(TOOLDIR)/why3extract$(EXE)
cp -f bin/why3prove.@OCAMLBEST@ $(TOOLDIR)/why3prove$(EXE)
cp -f bin/why3realize.@OCAMLBEST@ $(TOOLDIR)/why3realize$(EXE)
cp -f bin/why3replay.@OCAMLBEST@ $(TOOLDIR)/why3replay$(EXE)
install_local:: $(addprefix bin/,$(TOOLS_BIN))
ifneq "$(MAKECMDGOALS)" "clean"
include $(TOOLSDEP)
endif
depend: $(TOOLSDEP)
clean::
rm -f src/tools/args.cm[iox] src/tools/args.annot src/tools/args.o src/tools/args.dep
rm -f src/tools/why3execute.cm[iox] src/tools/why3execute.annot src/tools/why3execute.o src/tools/why3execute.dep
rm -f src/tools/why3extract.cm[iox] src/tools/why3extract.annot src/tools/why3extract.o src/tools/why3extract.dep
rm -f src/tools/why3prove.cm[iox] src/tools/why3prove.annot src/tools/why3prove.o src/tools/why3prove.dep
rm -f src/tools/why3realize.cm[iox] src/tools/why3realize.annot src/tools/why3realize.o src/tools/why3realize.dep
rm -f src/tools/why3replay.cm[iox] src/tools/why3replay.annot src/tools/why3replay.o src/tools/why3replay.dep
rm -f bin/why3execute.byte bin/why3execute.opt bin/why3execute
rm -f bin/why3extract.byte bin/why3extract.opt bin/why3extract
rm -f bin/why3prove.byte bin/why3prove.opt bin/why3prove
rm -f bin/why3realize.byte bin/why3realize.opt bin/why3realize
rm -f bin/why3replay.byte bin/why3replay.opt bin/why3replay
##############
# test targets
......@@ -580,7 +705,7 @@ clean_old_install::
rm -f $(BINDIR)/why3config$(EXE)
install_no_local::
cp -f bin/why3config.@OCAMLBEST@ $(BINDIR)/why3config$(EXE)
cp -f bin/why3config.@OCAMLBEST@ $(TOOLDIR)/why3config$(EXE)
install_local:: bin/why3config
......@@ -641,66 +766,12 @@ clean_old_install::
rm -f $(BINDIR)/why3ide$(EXE)
install_no_local::
cp -f bin/why3ide.@OCAMLBEST@ $(BINDIR)/why3ide$(EXE)
cp -f bin/why3ide.@OCAMLBEST@ $(TOOLDIR)/why3ide$(EXE)
install_local:: bin/why3ide
endif
###############
# Replayer
###############
REPLAYER_FILES = replay
REPLAYERMODULES = $(addprefix src/why3replayer/, $(REPLAYER_FILES))
REPLAYERDEP = $(addsuffix .dep, $(REPLAYERMODULES))
REPLAYERCMO = $(addsuffix .cmo, $(REPLAYERMODULES))
REPLAYERCMX = $(addsuffix .cmx, $(REPLAYERMODULES))
$(REPLAYERDEP): DEPFLAGS += -I src/why3replayer
$(REPLAYERCMO) $(REPLAYERCMX): INCLUDES += -I src/why3replayer
# build targets
byte: bin/why3replayer.byte
opt: bin/why3replayer.opt
bin/why3replayer.opt: lib/why3/why3.cmxa $(REPLAYERCMX)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3replayer.byte: lib/why3/why3.cma $(REPLAYERCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
bin/why3replayer: bin/why3replayer.@OCAMLBEST@
ln -sf why3replayer.@OCAMLBEST@ $@
# depend and clean targets
ifneq "$(MAKECMDGOALS)" "clean"
include $(REPLAYERDEP)
endif
depend: $(REPLAYERDEP)
clean::
rm -f src/why3replayer/*.cm[iox] src/why3replayer/*.o
rm -f src/why3replayer/*.annot src/why3replayer/*.dep src/why3replayer/*~
rm -f bin/why3replayer.byte bin/why3replayer.opt bin/why3replayer
clean_old_install::
rm -f $(BINDIR)/why3replayer$(EXE)
install_no_local::
cp -f bin/why3replayer.@OCAMLBEST@ $(BINDIR)/why3replayer$(EXE)
install_local:: bin/why3replayer
###############
# Session
###############
......@@ -752,7 +823,7 @@ clean_old_install::
rm -f $(BINDIR)/why3session$(EXE)
install_no_local::
cp -f bin/why3session.@OCAMLBEST@ $(BINDIR)/why3session$(EXE)
cp -f bin/why3session.@OCAMLBEST@ $(TOOLDIR)/why3session$(EXE)
install_local:: bin/why3session
......@@ -810,7 +881,7 @@ clean_old_install::
rm -f $(BINDIR)/why3bench$(EXE)
install_no_local::
cp -f bin/why3bench.@OCAMLBEST@ $(BINDIR)/why3bench$(EXE)
cp -f bin/why3bench.@OCAMLBEST@ $(TOOLDIR)/why3bench$(EXE)
install_local:: bin/why3bench
......@@ -1010,31 +1081,31 @@ clean::
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-int: bin/why3 drivers/coq-realizations.aux theories/int.why
for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done
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/why3 drivers/coq-realizations.aux theories/bool.why
for f in $(COQLIBS_BOOL_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T bool.$$f -o lib/coq/bool/; done
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/why3 drivers/coq-realizations.aux theories/real.why
for f in $(COQLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T real.$$f -o lib/coq/real/; done
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/why3 drivers/coq-realizations.aux theories/number.why
for f in $(COQLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T number.$$f -o lib/coq/number/; done
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/why3 drivers/coq-realizations.aux theories/set.why
for f in $(COQLIBS_SET_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T set.$$f -o lib/coq/set/; done
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/why3 drivers/coq-realizations.aux theories/map.why
for f in $(COQLIBS_MAP_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T map.$$f -o lib/coq/map/; done
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/why3 drivers/coq-realizations.aux theories/list.why
for f in $(COQLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T list.$$f -o lib/coq/list/; done
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/why3 drivers/coq-realizations.aux theories/option.why
for f in $(COQLIBS_OPTION_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T option.$$f -o lib/coq/option/; done
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-fp: bin/why3 drivers/coq-realizations.aux theories/floating_point.why
for f in $(COQLIBS_FP_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T floating_point.$$f -o lib/coq/floating_point/; done
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
......@@ -1108,11 +1179,11 @@ install_no_local::
install_local:: drivers/pvs-realizations.aux
update-pvs: bin/why3 drivers/pvs-realizations.aux
for f in $(PVSLIBS_INT_FILES); do bin/why3 --realize -D drivers/pvs-realize.drv -T int.$$f -o lib/pvs/int/; done
for f in $(PVSLIBS_REAL_FILES); do bin/why3 --realize -D drivers/pvs-realize.drv -T real.$$f -o lib/pvs/real/; done
for f in $(PVSLIBS_LIST_FILES); do bin/why3 --realize -D drivers/pvs-realize.drv -T list.$$f -o lib/pvs/list/; done
for f in $(PVSLIBS_NUMBER_FILES); do bin/why3 --realize -D drivers/pvs-realize.drv -T number.$$f -o lib/pvs/number/; done
for f in $(PVSLIBS_FP_FILES); do bin/why3 --realize -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@ -D drivers/pvs-realize.drv -T int.$$f -o lib/pvs/int/; done
for f in $(PVSLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -D drivers/pvs-realize.drv -T real.$$f -o lib/pvs/real/; done
for f in $(PVSLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -D drivers/pvs-realize.drv -T list.$$f -o lib/pvs/list/; done
for f in $(PVSLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -D drivers/pvs-realize.drv -T number.$$f -o lib/pvs/number/; done
for f in $(PVSLIBS_FP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -D drivers/pvs-realize.drv -T floating_point.$$f -o lib/pvs/floating_point/; done
else
......@@ -1204,42 +1275,42 @@ update-isabelle: $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $
$(ISABELLELIBS_INT): bin/why3 drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/int.why
mkdir -p lib/isabelle/int
WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/isabelle-realize.drv -T int.$(notdir $(basename $@)) -o lib/isabelle/int/
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T int.$(notdir $(basename $@)) -o lib/isabelle/int/
$(ISABELLELIBS_BOOL): bin/why3 drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/bool.why
mkdir -p lib/isabelle/bool
WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/isabelle-realize.drv -T bool.$(notdir $(basename $@)) -o lib/isabelle/bool/
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T bool.$(notdir $(basename $@)) -o lib/isabelle/bool/
$(ISABELLELIBS_REAL): bin/why3 drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/real.why
mkdir -p lib/isabelle/real
WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/isabelle-realize.drv -T real.$(notdir $(basename $@)) -o lib/isabelle/real/
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T real.$(notdir $(basename $@)) -o lib/isabelle/real/
$(ISABELLELIBS_NUMBER): bin/why3 drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/number.why
mkdir -p lib/isabelle/number
WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/isabelle-realize.drv -T number.$(notdir $(basename $@)) -o lib/isabelle/number/
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T number.$(notdir $(basename $@)) -o lib/isabelle/number/
$(ISABELLELIBS_SET): bin/why3 drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/set.why
mkdir -p lib/isabelle/set
WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/isabelle-realize.drv -T set.$(notdir $(basename $@)) -o lib/isabelle/set/
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T set.$(notdir $(basename $@)) -o lib/isabelle/set/
$(ISABELLELIBS_MAP): bin/why3 drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/map.why
mkdir -p lib/isabelle/map
WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/isabelle-realize.drv -T map.$(notdir $(basename $@)) -o lib/isabelle/map/
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T map.$(notdir $(basename $@)) -o lib/isabelle/map/
$(ISABELLELIBS_LIST): bin/why3 drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/list.why
mkdir -p lib/isabelle/list
WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/isabelle-realize.drv -T list.$(notdir $(basename $@)) -o lib/isabelle/list/
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T list.$(notdir $(basename $@)) -o lib/isabelle/list/
$(ISABELLELIBS_OPTION): bin/why3 drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/option.why
mkdir -p lib/isabelle/option
WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/isabelle-realize.drv -T option.$(notdir $(basename $@)) -o lib/isabelle/option/
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T option.$(notdir $(basename $@)) -o lib/isabelle/option/
opt byte: update-isabelle
......@@ -1412,7 +1483,7 @@ clean_old_install::
rm -f $(BINDIR)/why3wc$(EXE)
install_no_local::
cp -f bin/why3wc.@OCAMLBEST@ $(BINDIR)/why3wc$(EXE)
cp -f bin/why3wc.@OCAMLBEST@ $(TOOLDIR)/why3wc$(EXE)
install_local:: bin/why3wc
......@@ -1469,7 +1540,7 @@ clean_old_install::
rm -f $(BINDIR)/why3doc$(EXE)
install_no_local::
cp -f bin/why3doc.@OCAMLBEST@ $(BINDIR)/why3doc$(EXE)
cp -f bin/why3doc.@OCAMLBEST@ $(TOOLDIR)/why3doc$(EXE)
install_local:: bin/why3doc
......@@ -1489,7 +1560,7 @@ bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \
# desactivé car requiert findlib
# if test -d examples/runstrat ; then \
# $(MAKE) test-runstrat.@OCAMLBEST@ ; fi
bash bench/bench "bin/why3.@OCAMLBEST@"
bash bench/bench ".@OCAMLBEST@"
@if test "@enable_coq_tactic@" = "yes"; then \
echo "=== checking the Coq tactic ==="; \
$(MAKE) test-coq-tactic.@OCAMLBEST@; fi
......@@ -1610,7 +1681,7 @@ test-runstrat: test-runstrat.$(OCAMLBEST)
test-ocaml-extraction: bin/why3.opt lib/why3/why3extract.cmxa
@echo "driver ocaml32"
@mkdir -p tests/test-extraction
@cd tests ; ../bin/why3.opt -E ocaml32 \
@cd tests ; ../bin/why3extract.opt -D ocaml32 \
test_extraction.mlw -o test-extraction
@cd tests/test-extraction/ ; \
$(OCAMLOPT) @BIGINTINCLUDE@ -I ../../lib/why3 \
......@@ -1618,7 +1689,7 @@ test-ocaml-extraction: bin/why3.opt lib/why3/why3extract.cmxa
ref__Refint.ml test_extraction__TestExtraction.ml main.ml
@tests/test-extraction/a.out
@echo "driver ocaml64"
@cd tests ; ../bin/why3.opt -E ocaml64 \
@cd tests ; ../bin/why3extract.opt -D ocaml64 \
test_extraction.mlw -o test-extraction
@cd tests/test-extraction/ ; \
$(OCAMLOPT) @BIGINTINCLUDE@ -I ../../lib/why3 \
......
......@@ -7,9 +7,10 @@
# export WHY3DATA=.
# export WHY3LOADPATH=theories
pgm=$1
suffix=$1
goods () {
pgm="bin/why3prove$suffix"
for f in $1/*.[wm][hl][yw] ; do
echo -n " $f... "
# running Why
......@@ -26,6 +27,7 @@ goods () {
}
bads () {
pgm="bin/why3prove$suffix"
for f in $1/*.[wm][hl][yw] ; do
echo -n " $f... "
if $pgm $2 $f > /dev/null 2>&1; then
......@@ -39,6 +41,7 @@ bads () {
}
drivers () {
pgm="bin/why3prove$suffix"
for f in $1/*.drv; do
if [[ $f == drivers/ocaml*.drv ]]; then continue; fi
echo -n " $f... "
......@@ -53,6 +56,7 @@ drivers () {
}
valid_goals () {
pgm="bin/why3prove$suffix"
for f in $1/*.mlw; do
echo -n " "$f"... "
if $pgm -t 10 -P alt-ergo $f | grep -q -v Valid; then
......@@ -67,6 +71,7 @@ valid_goals () {
}
invalid_goals () {
pgm="bin/why3prove$suffix"
for f in $1/*.mlw; do
echo -n " "$f"... "
if $pgm -t 3 -P alt-ergo $f | grep -q Valid; then
......@@ -81,13 +86,14 @@ invalid_goals () {
}
execute () {
pgm="bin/why3execute$suffix"
echo -n "$1 $2... "
if $pgm $1 --exec $2 > /dev/null 2>&1; then
if $pgm $1 $2 > /dev/null 2>&1; then
echo "ok"
else
echo "execution test failed!"
echo $pgm $1 --exec $2
$pgm $1 --exec $2
echo $pgm $1 $2
$pgm $1 $2
exit 1
fi
}
......@@ -123,6 +129,7 @@ extract_and_run () {
}
list_stuff () {
pgm="bin/why3$suffix"
echo -n "$1 "
if $pgm $1 > /dev/null 2>&1; then
echo "ok"
......@@ -164,8 +171,8 @@ goods examples/logic
goods examples
goods examples/foveoos11-cm
goods examples/hoare_logic
goods examples/vacid_0_binary_heaps "-I examples/vacid_0_binary_heaps"
goods examples/bitvectors "-I examples/bitvectors"
goods examples/vacid_0_binary_heaps "-L examples/vacid_0_binary_heaps"
goods examples/bitvectors "-L examples/bitvectors"
goods examples/in_progress
echo ""
......
# useful script for git bisect
make || exit 125 ; bin/why3config --detect && bin/why3replayer examples/bellman_ford.mlw
make || exit 125 ; bin/why3config --detect && bin/why3replay examples/bellman_ford.mlw
......@@ -150,7 +150,7 @@ end
\section{Calling External Provers}
To call an external prover, we need to access the Why configuration
To call an external prover, we need to access the \why configuration
file \texttt{why3.conf}, as it was built using the \texttt{why3config}
command line tool or the \textsf{Detect Provers} menu of the graphical
IDE. The following API calls allow to access the content of this
......@@ -360,13 +360,13 @@ be done by a sequence of calls:
\item closing the theory under construction, obtaining something of type \verb|Theory.theory|.
\end{itemize}
Creation of a theory named \verb|My_theory| is done by:
Creation of a theory named \verb|My_theory| is done by
\begin{ocamlcode}
let my_theory : Theory.theory_uc =
Theory.create_theory (Ident.id_fresh "My_theory")
\end{ocamlcode}
First let us add the formula 1 above as a goal:
First let us add formula 1 above as a goal:
\begin{ocamlcode}
let decl_goal1 : Decl.decl =
Decl.create_prop_decl Decl.Pgoal goal_id1 fmla1
......@@ -424,7 +424,7 @@ Finally, we close our theory under construction as follows.
let my_theory : Theory.theory = Theory.close_theory my_theory
\end{ocamlcode}
We can inspect what we did for example by printing that theory:
We can inspect what we did by printing that theory:
\begin{ocamlcode}
let () = printf "@[theory is:@\n%a@]@." Pretty.print_theory my_theory
\end{ocamlcode}
......@@ -472,21 +472,21 @@ let () =
One can run provers on those tasks exactly as we did above.
\section{Applying transformations}
\section{Applying Transformations}
[TO BE COMPLETED]
\section{Writing new functions on term}
\section{Writing New Functions on Terms}
[TO BE COMPLETED]
% pattern-matching on terms, opening a quantifier
\section{Proof sessions}
\section{Proof Sessions}
See the example \verb|examples/use_api/create_session.ml| of the distribution for
an illustration on how to manipulate proof sessions from an OCaml program.
\section{ML programs}
\section{ML Programs}
There are two ways for building \whyml programs from OCaml. The first
is to build untyped syntax trees for such \whyml programs, and then
......
......@@ -14,7 +14,7 @@ The Coq tactic is installed in
where \textit{why3-lib-dir} is \why's library directory, as reported
by \verb+why3 --print-libdir+. This directory
is automatically added to Coq's load path if you are
calling Coq via \why (from \texttt{why3ide}, \texttt{why3replayer},
calling Coq via \why (from \texttt{why3 ide}, \texttt{why3 replay},
etc.). If you are calling Coq by yourself, you need to add
this directory to Coq's load path, either using Coq's command line
option \texttt{-I} or by adding
......@@ -33,6 +33,7 @@ The Coq tactic is called \texttt{why3} and is used as follows: