Commit acef5992 authored by MARCHE Claude's avatar MARCHE Claude

extraction examples/prover: fixed makefile target

parent 43fd0330
......@@ -29,13 +29,13 @@ MLWTYPES=BacktrackArray Firstorder_symbol_impl ISet Firstorder_term_impl \
MLWIMPL=$(MLWTYPES) ProverMain ProverTest
BD=build
MLUTIL=$(patsubst %,$(BD)/%__Nat,$(MLWUTIL))
MLTYPES=$(patsubst %,$(BD)/%__Types,$(MLWTYPES))
MLIMPL=$(patsubst %,$(BD)/%__Impl,$(MLWIMPL))
MLALL=$(MLUTIL) $(MLTYPES) $(MLIMPL)
ML=$(patsubst %,%.ml,$(MLALL))
CMX=$(patsubst %,%.cmx,$(MLALL))
BD=prover
#MLUTIL=$(patsubst %,$(BD)/%__Nat,$(MLWUTIL))
#MLTYPES=$(patsubst %,$(BD)/%__Types,$(MLWTYPES))
#MLIMPL=$(patsubst %,$(BD)/%__Impl,$(MLWIMPL))
#MLALL=$(MLUTIL) $(MLTYPES) $(MLIMPL)
#ML=$(patsubst %,%.ml,$(MLALL))
#CMX=$(patsubst %,%.cmx,$(MLALL))
OCAMLC=ocamlopt.opt
INCLUDES=-I $(BD) $(INCLUDEALL) -I ../../plugins/tptp
LIBS=unix.cmxa nums.cmxa $(BIGINTLIB).cmxa dynlink.cmxa str.cmxa menhirLib.cmx zip.cmxa why3.cmxa why3extract.cmxa tptp_ast.cmx tptp_typing.cmx tptp_parser.cmx tptp_lexer.cmx
......@@ -47,15 +47,15 @@ MLEXECFLAGS=
.PHONY: clean depend extract replay
$(BD)/prover: $(CMX) run.cmx
$(BD): $(BD).cmx run.cmx
echo "WHY3SHARE="$(WHY3SHARE)
$(OCAMLC) $(INCLUDES) $(LIBS) $(MLFLAGS) $(MLEXECFLAGS) \
-o $(BD)/prover $^
-o $(BD) $^
extract: $(ML)
$(ML):
why3 $(WHY3FLAGS) extract -D ocaml64 -o $(BD) ProverTest.mlw
$(BD).ml:
why3 $(WHY3FLAGS) extract -D ocaml64 -o $(BD).ml ProverTest.mlw
%.cmx: %.ml
$(OCAMLC) $(INCLUDES) $(MLFLAGS) -c $<
......
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