]> matita.cs.unibo.it Git - helm.git/blob - daemons/proofChecker/Makefile
Bug fixed: the script Menu was not locked as expected.
[helm.git] / daemons / 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 ifeq ($(origin OCAMLPATH), undefined)
6 OCAMLFIND = OCAMLPATH=../../components/METAS ocamlfind
7 else
8 OCAMLFIND = ocamlfind
9 endif
10 OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLOPTIONS) -g
11 OCAMLOPT = $(OCAMLFIND) ocamlopt $(OCAMLOPTIONS)
12 OCAMLDEP = ocamldep
13
14 LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES))
15 LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES))
16
17 all: $(PROOFCHECKEROBJS) proofChecker
18 opt: $(PROOFCHECKEROBJS:.cmo=.cmx) proofChecker.opt
19
20 DEPOBJS = proofChecker.ml
21
22 PROOFCHECKEROBJS = proofChecker.cmo
23
24 depend:
25         $(OCAMLDEP) $(DEPOBJS) > .depend
26
27 proofChecker: $(PROOFCHECKEROBJS) $(LIBRARIES)
28         $(OCAMLC)  -linkpkg -o proofChecker $(PROOFCHECKEROBJS)
29
30 proofChecker.opt: $(PROOFCHECKEROBJS:.cmo=.cmx) $(LIBRARIES_OPT)
31         $(OCAMLOPT) -linkpkg -o proofChecker.opt $(PROOFCHECKEROBJS:.cmo=.cmx)
32
33 .SUFFIXES: .ml .mli .cmo .cmi .cmx
34 .ml.cmo: $(LIBRARIES)
35         $(OCAMLC) -c $<
36 .mli.cmi: $(LIBRARIES)
37         $(OCAMLC) -c $<
38 .ml.cmx: $(LIBRARIES_OPT)
39         $(OCAMLOPT) -c $<
40
41 clean:
42         rm -f *.cm[iox] *.o proofChecker proofChecker.opt
43
44 install:
45         cp proofChecker proofChecker.opt $(BIN_DIR)
46
47 uninstall:
48         rm -f $(BIN_DIR)/proofChecker $(BIN_DIR)/proofChecker.opt
49
50 .PHONY: install uninstall clean
51
52 include .depend