1 BIN_DIR = /usr/local/bin
6 helm-cic_transformations \
7 helm-cic_textual_parser2 \
8 helm-mathql_interpreter \
9 helm-mathql_generator \
16 REQUIRES = $(TEST_REQUIRES) #gdome2-xslt helm-hbugs lablgtk2.init lablgtk2.glade
19 -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o -thread
21 OCAMLDEBUGOPTIONS = -g
22 OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) $(OCAMLOPTIONS)
23 OCAMLOPT = $(OCAMLFIND) ocamlopt $(OCAMLOPTIONS)
24 OCAMLDEP = $(OCAMLFIND) ocamldep -pp camlp4o
25 OCAMLDEBUG = wowcamldebug
27 LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES))
28 LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES))
29 TEST_LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(TEST_REQUIRES))
30 TEST_LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(TEST_REQUIRES))
36 $(MAKE) -C ../hbugs/ start
38 $(MAKE) -C ../hbugs/ stop
45 $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) \
48 TOPLEVELOBJS = $(INTERFACE_FILES:%.mli=%.cmo) saturation.cmo
50 # disambiguatingParser.cmo \
52 # REGTESTOBJS = $(TESTOBJS) regtest.cmo
53 # TESTLIBOBJS = $(TESTOBJS) testlibrary.cmo
55 $(INTERFACE_FILES:%.mli=%.cmo): $(LIBRARIES)
56 $(INTERFACE_FILES:%.mli=%.cmx): $(LIBRARIES_OPT)
59 $(OCAMLDEP) $(DEPOBJS) > .depend
61 saturation: $(TOPLEVELOBJS) $(LIBRARIES)
62 $(OCAMLC) -thread -linkpkg -o $@ $(TOPLEVELOBJS)
63 saturation.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT)
64 $(OCAMLOPT) -thread -linkpkg -o $@ $(TOPLEVELOBJS:.cmo=.cmx)
66 .SUFFIXES: .ml .mli .cmo .cmi .cmx
74 $(TOPLEVELOBJS): $(LIBRARIES)
75 $(TOPLEVELOBJS:.cmo=.cmx)): $(LIBRARIES_OPT)
78 rm -f *.cm[iox] *.o gTopLevel{,.opt} regtest{,.opt} testlibrary{,.opt}
80 cp gTopLevel gTopLevel.opt $(BIN_DIR)
82 rm -f $(BIN_DIR)/gTopLevel $(BIN_DIR)/gTopLevel.opt
84 .PHONY: install uninstall clean test
86 INTESTS := $(wildcard tests/*.cic)
87 OUTTESTS := $(patsubst %, %.test, $(INTESTS))
91 tests/%.cic.test: tests/%.cic regtest
92 time ./regtest -gen $<
94 ./regtest $(INTESTS) 2> /dev/null
96 ./regtest.opt $(INTESTS) 2> /dev/null
98 ./regtest -dump $(INTESTS) 2> /dev/null
99 envtest.opt: regtest.opt
100 ./regtest.opt -dump $(INTESTS) 2> /dev/null
101 librarytest: testlibrary
102 ./testlibrary -vars -varsprefix cic:/Coq index.txt 2>/dev/null >LOG
103 librarytest.opt: testlibrary.opt
104 ./testlibrary.opt -vars -varsprefix cic:/Coq index.txt 2>/dev/null >LOG
105 typecheck_uri: typecheck_uri.ml
106 $(OCAMLFIND) ocamlc -thread -package helm-cic_proof_checking -linkpkg -o $@ $<
107 typecheck_uri.opt: typecheck_uri.ml
108 $(OCAMLFIND) opt -thread -package helm-cic_proof_checking -linkpkg -o $@ $<
113 echo "load_printer \"threads.cma\"" > .debug_script
114 $(OCAMLFIND) query -recursive -predicates "mt,byte" -a-format \
115 helm-cic_unification | \
116 sed 's/\(.*\)/load_printer "\1"/' \
118 echo "install_printer CicMetaSubst.fppsubst" >> .debug_script
119 echo "install_printer CicMetaSubst.fppterm" >> .debug_script
120 echo "install_printer CicMetaSubst.fppmetasenv" >> .debug_script
121 ledit $(OCAMLDEBUG) \
122 -source .debug_script \
124 $(shell $(OCAMLFIND) query -recursive -i-format $(REQUIRES)) \
127 ifneq ($(MAKECMDGOALS), depend)