Commit 7f913f7c authored by MARCHE Claude's avatar MARCHE Claude

Doc, extraction: add something about Makefiles

parent 43728447
......@@ -92,6 +92,19 @@ For instance, it could be
-I `why3 --print-libdir`/why3 why3extract.cmxa \
...
\end{verbatim}
To make the compilation process easier, one can write a
\texttt{Makefile} which can include informations about Why3
configuration as follows.
\begin{whycode}
WHY3SHARE=$(shell why3 --print-datadir)
include $(WHY3SHARE)/Makefile.config
maxsum:
ocamlopt $(INCLUDE) $(BIGINTLIB).cmxa why3extract.cmxa \
-o maxsum maxsum__MaxAndSum.ml main.ml
\end{whycode}
%%% Local Variables:
......
......@@ -20,18 +20,20 @@ ifeq ($(BENCH),yes)
endif
MLW=BacktrackArray Firstorder_symbol_impl ISet Firstorder_term_impl \
MLWTYPES=BacktrackArray Firstorder_symbol_impl ISet Firstorder_term_impl \
Firstorder_formula_impl Firstorder_formula_list_impl \
Firstorder_tableau_impl Unification FormulaTransformations \
Prover ProverMain ProverTest
Prover
MLWIMPL=$(MLWTYPES) ProverMain ProverTest
BD=build
MLUTIL=$(BD)/Nat__Nat
MLTYPES=$(patsubst %,$(BD)/%__Types,$(MLW))
MLIMPL=$(patsubst %,$(BD)/%__Impl,$(MLW))
ML=$(MLUTIL) $(MLTYPES) $(MLIMPL)
CMX=$(patsubst %,%.cmx,$(ML))
CMI=$(patsubst %,%.cmi,$(ML))
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) $(INCLUDE)
LIBS=unix.cmxa $(BIGINTLIB).cmxa why3extract.cmxa
......@@ -45,30 +47,29 @@ $(BD)/prover: $(CMX) run.cmx
$(OCAMLC) $(INCLUDES) $(LIBS) $(MLFLAGS) $(MLEXECFLAGS) \
-o $(BD)/prover $^
%.cmx: %.ml
$(OCAMLC) $(INCLUDES) $(MLFLAGS) -c $<
$(BD)/Nat__Nat.ml: Nat.mlw
why3 $(WHY3FLAGS) extract -D ocaml64 -o $(BD) $< -T Nat
extract: $(ML)
$(BD)/%__Types.ml: %.mlw
why3 $(WHY3FLAGS) extract -D ocaml64 -o $(BD) $< -T Types
$(ML):
why3 $(WHY3FLAGS) extract -D ocaml64 -o $(BD) ProverTest.mlw
$(BD)/%__Impl.ml: %.mlw
why3 $(WHY3FLAGS) extract -D ocaml64 -o $(BD) $< -T Impl
%.cmx: %.ml
$(OCAMLC) $(INCLUDES) $(MLFLAGS) -c $<
.PHONY: clean depend
depend: .depend
.depend: Makefile $(patsubst %,%.ml,$(ML))
ocamldep.opt -I $(BD) $(patsubst %,%.ml,$(ML)) > .depend
.depend: Makefile $(ML)
ocamldep.opt -I $(BD) $(ML) > .depend
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
ifneq "$(MAKECMDGOALS:extract%=extract)" "extract"
include .depend
endif
endif
clean:
rm -f $(BD)/*.o $(BD)/*.cmi $(BD)/*.cmx
rm -f $(BD)/*__*.ml
rm -f *~ *.o *.cmi *.cmx build/prover
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