]> matita.cs.unibo.it Git - helm.git/blob - helm/proofChecker/Makefile
...
[helm.git] / helm / proofChecker / Makefile
1 BIN_DIR = /usr/local/bin
2 REQUIRES = helm-cic_proof_checking http
3 PREDICATES =
4 OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread
5 OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) -g
6 OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS)
7 OCAMLDEP = ocamldep
8
9 LIBRARIES = $(shell ocamlfind query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES))
10 LIBRARIES_OPT = $(shell ocamlfind query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES))
11
12 all: $(PROOFCHECKEROBJS) proofChecker
13 opt: $(PROOFCHECKEROBJS:.cmo=.cmx) proofChecker.opt
14
15 DEPOBJS = proofChecker.ml
16
17 PROOFCHECKEROBJS = proofChecker.cmo
18
19 depend:
20         $(OCAMLDEP) $(DEPOBJS) > .depend
21
22 proofChecker: $(PROOFCHECKEROBJS) $(LIBRARIES)
23         $(OCAMLC)  -linkpkg -o proofChecker $(PROOFCHECKEROBJS)
24
25 proofChecker.opt: $(PROOFCHECKEROBJS:.cmo=.cmx) $(LIBRARIES_OPT)
26         $(OCAMLOPT) -linkpkg -o proofChecker.opt $(PROOFCHECKEROBJS:.cmo=.cmx)
27
28 .SUFFIXES: .ml .mli .cmo .cmi .cmx
29 .ml.cmo: $(LIBRARIES)
30         $(OCAMLC) -c $<
31 .mli.cmi: $(LIBRARIES)
32         $(OCAMLC) -c $<
33 .ml.cmx: $(LIBRARIES_OPT)
34         $(OCAMLOPT) -c $<
35
36 clean:
37         rm -f *.cm[iox] *.o proofChecker proofChecker.opt
38
39 install:
40         cp proofChecker proofChecker.opt $(BIN_DIR)
41
42 uninstall:
43         rm -f $(BIN_DIR)/proofChecker $(BIN_DIR)/proofChecker.opt
44
45 .PHONY: install uninstall clean
46
47 include .depend