Commit 317d51b8 authored by MARCHE Claude's avatar MARCHE Claude

Prover example: makefile entry for replaying all

parent 7f913f7c
......@@ -20,6 +20,8 @@ ifeq ($(BENCH),yes)
endif
MLWUTIL=Nat
MLWTYPES=BacktrackArray Firstorder_symbol_impl ISet Firstorder_term_impl \
Firstorder_formula_impl Firstorder_formula_list_impl \
Firstorder_tableau_impl Unification FormulaTransformations \
......@@ -28,7 +30,7 @@ MLWTYPES=BacktrackArray Firstorder_symbol_impl ISet Firstorder_term_impl \
MLWIMPL=$(MLWTYPES) ProverMain ProverTest
BD=build
MLUTIL=$(BD)/Nat__Nat
MLUTIL=$(patsubst %,$(BD)/%__Nat,$(MLWUTIL))
MLTYPES=$(patsubst %,$(BD)/%__Types,$(MLWTYPES))
MLIMPL=$(patsubst %,$(BD)/%__Impl,$(MLWIMPL))
MLALL=$(MLUTIL) $(MLTYPES) $(MLIMPL)
......@@ -43,6 +45,8 @@ MLFLAGS=
MLIFLAGS=
MLEXECFLAGS=
.PHONY: clean depend extract replay
$(BD)/prover: $(CMX) run.cmx
$(OCAMLC) $(INCLUDES) $(LIBS) $(MLFLAGS) $(MLEXECFLAGS) \
-o $(BD)/prover $^
......@@ -55,11 +59,6 @@ $(ML):
%.cmx: %.ml
$(OCAMLC) $(INCLUDES) $(MLFLAGS) -c $<
.PHONY: clean depend
depend: .depend
.depend: Makefile $(ML)
ocamldep.opt -I $(BD) $(ML) > .depend
......@@ -69,6 +68,13 @@ include .depend
endif
endif
replay:
for i in $(MLWUTIL) $(MLWIMPL); do \
why3 replay -L . $$i ; \
done
depend: .depend
clean:
rm -f $(BD)/*.o $(BD)/*.cmi $(BD)/*.cmx
rm -f $(BD)/*__*.ml
......
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