Commit 15c3c97f authored by Martin Clochard's avatar Martin Clochard
parents 8ab8e6d9 c26dfb9c
......@@ -51,9 +51,6 @@ 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
......
......@@ -222,7 +222,7 @@ lib/why3/why3.cmx: $(LIBCMX)
# clean and depend
ifneq "$(MAKECMDGOALS)" "clean"
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
include $(LIBDEP)
endif
......@@ -421,7 +421,7 @@ PLUGCLEAN = $(addsuffix /*.cm[iox], $(PLUGSDIRS)) \
# depend and clean targets
ifneq "$(MAKECMDGOALS)" "clean"
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
include $(PLUGDEP)
endif
......@@ -435,42 +435,6 @@ install_no_local::
mkdir -p $(LIBDIR)/why3/plugins
cp -f $(foreach f,$(LIBPLUGCMO) $(LIBPLUGCMXS),$(wildcard $(f))) $(LIBDIR)/why3/plugins
#################################
# Old Why3 command, to be removed
#################################
src/tools/why3contraption.cmo: lib/why3/why3.cma
src/tools/why3contraption.cmx: lib/why3/why3.cmxa
byte: bin/why3contraption.byte
opt: bin/why3contraption.opt
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) $^
clean_old_install::
rm -f $(BINDIR)/why3contraption$(EXE)
install_no_local::
cp -f bin/why3contraption.@OCAMLBEST@ $(BINDIR)/why3contraption$(EXE)
install_local:: bin/why3 bin/why3contraption
ifneq "$(MAKECMDGOALS)" "clean"
include src/tools/why3contraption.dep
endif
depend: src/tools/why3contraption.dep
clean::
rm -f src/tools/why3contraption.cm[iox] src/tools/why3contraption.annot src/tools/why3contraption.o src/tools/why3contraption.dep
rm -f bin/why3contraption.byte bin/why3contraption.opt bin/why3contraption
###############
# Why3 commands
###############
......@@ -564,7 +528,7 @@ install_local:: bin/why3 $(addprefix bin/,$(TOOLS_BIN))
bin/%: bin/%.@OCAMLBEST@
ln -sf $(notdir $<) $@
ifneq "$(MAKECMDGOALS)" "clean"
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
include $(TOOLSDEP)
endif
......@@ -694,7 +658,7 @@ src/ide/resetgc.o: src/ide/resetgc.c
# depend and clean targets
ifneq "$(MAKECMDGOALS)" "clean"
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
include $(IDEDEP)
endif
......@@ -749,7 +713,7 @@ bin/why3session.byte: lib/why3/why3.cma $(SESSIONCMO)
# depend and clean targets
ifneq "$(MAKECMDGOALS)" "clean"
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
include $(SESSIONDEP)
endif
......@@ -825,7 +789,7 @@ src/coq-tactic/.why3-vo-opt: lib/coq-tactic/Why3.v lib/coq-tactic/why3tac.cmxs
# depend and clean targets
ifneq "$(MAKECMDGOALS)" "clean"
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
include $(COQPDEP)
endif
......@@ -949,7 +913,7 @@ endif
install_local:: $(COQVO) drivers/coq-realizations.aux
ifneq "$(MAKECMDGOALS)" "clean"
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
ifneq "$(MAKECMDGOALS:update-coq%=update-coq)" "update-coq"
include $(COQVD)
endif
......@@ -957,9 +921,11 @@ endif
depend: $(COQVD)
clean::
clean-coq:
rm -f $(COQVO) $(COQVD) $(addsuffix .glob, $(COQLIBS_FILES))
clean:: clean-coq
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
......@@ -1230,7 +1196,7 @@ $(OCAMLLIBS_DEP): DEPFLAGS += -I src/util -I lib/ocaml @BIGINTINCLUDE@
$(OCAMLLIBS_CMO) $(OCAMLLIBS_CMX): INCLUDES += -I src/util -I lib/ocaml @BIGINTINCLUDE@
$(OCAMLLIBS_CMX): OFLAGS += -for-pack Why3extract
ifneq "$(MAKECMDGOALS)" "clean"
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
include $(OCAMLLIBS_DEP)
endif
......@@ -1342,7 +1308,7 @@ bin/why3wc.byte: $(WHY3WCCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
ifneq "$(MAKECMDGOALS)" "clean"
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
include $(WHY3WCDEP)
endif
......@@ -1396,7 +1362,7 @@ bin/why3doc.byte: lib/why3/why3.cma $(WHY3DOCCMO)
# depend and clean targets
ifneq "$(MAKECMDGOALS)" "clean"
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
include $(WHY3DOCDEP)
endif
......
......@@ -140,21 +140,19 @@ type config_strategy = {
(* a default set of strategies *)
let default_strategies =
List.map
(fun (name,desc,shortcut,instrs) ->
(fun (name,desc,shortcut,code) ->
let s = ref Rc.empty_section in
s := Rc.set_string !s "name" name;
s := Rc.set_string !s "desc" desc;
s := Rc.set_string !s "shortcut" shortcut;
for i = 0 to Array.length instrs - 1 do
s := Rc.set_string !s ("l" ^ (string_of_int i)) instrs.(i);
done;
s := Rc.set_string !s "code" code;
!s)
[ "Split", "Split@ conjunctions@ in@ goal", "s",
[|"t split_goal_wp 1"|];
"t split_goal_wp exit";
"Inline", "Inline@ function@ symbols@ once", "i",
[|"t inline_goal 1"|];
"t inline_goal exit";
"Compute", "Compute@ in@ goal", "c",
[|"t compute_in_goal 1"|];
"t compute_in_goal exit";
]
let get_strategies ?(default=[]) rc =
......
......@@ -89,7 +89,7 @@
let integer msg s =
try int_of_string s
with Failure _ -> error "unabel to parse %s argument '%s'" msg s
with Failure _ -> error "unable to parse %s argument '%s'" msg s
let transform code t =
try
......
This diff is collapsed.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment