BIN_DIR = /usr/local/bin
TEST_REQUIRES = \
+ helm-registry \
helm-mathql_interpreter \
helm-mathql_generator \
helm-tactics \
helm-cic_textual_parser \
helm-tex_cic_textual_parser \
mathml-editor \
- lablgtkmathview \
- helm-cic_cache
+ lablgtkmathview
REQUIRES = \
$(TEST_REQUIRES) \
gdome2-xslt \
- hbugs-client \
- helm-cic_cache
+ hbugs-client
PREDICATES = "gnome,init,glade"
-OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o
+OCAMLOPTIONS = \
+ -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o -thread
OCAMLFIND = ocamlfind
OCAMLDEBUGOPTIONS = -g
OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) $(OCAMLOPTIONS)
-OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS)
+OCAMLOPT = $(OCAMLFIND) ocamlopt $(OCAMLOPTIONS)
OCAMLDEP = $(OCAMLFIND) ocamldep -pp camlp4o
OCAMLDEBUG = wowcamldebug
termViewer.mli \
invokeTactics.mli \
hbugs.mli \
- chosenTermEditor.mli
+ chosenTermEditor.mli \
+ helmGtkLogger.mli
DEPOBJS = \
$(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) \
$(OCAMLOPT) -thread -linkpkg -o $@ $(TOPLEVELOBJS:.cmo=.cmx)
testlibrary: $(TESTLIBOBJS) $(TEST_LIBRARIES)
- $(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) -linkpkg \
+ $(OCAMLFIND) ocamlc -thread $(OCAMLDEBUGOPTIONS) -linkpkg \
-package "$(TEST_REQUIRES)" -o $@ $(TESTLIBOBJS)
testlibrary.opt: $(TESTLIBOBJS:.cmo=.cmx) $(TEST_LIBRARIES_OPT)
- $(OCAMLFIND) opt -linkpkg -package "$(TEST_REQUIRES)" -o $@ \
+ $(OCAMLFIND) ocamlopt -thread -linkpkg -package "$(TEST_REQUIRES)" -o $@ \
$(TESTLIBOBJS:.cmo=.cmx)
regtest: $(REGTESTOBJS) $(TEST_LIBRARIES)
- $(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) -linkpkg \
+ $(OCAMLFIND) ocamlc -thread $(OCAMLDEBUGOPTIONS) -linkpkg \
-package "$(TEST_REQUIRES)" -o $@ $(REGTESTOBJS)
regtest.opt: $(REGTESTOBJS:.cmo=.cmx) $(TEST_LIBRARIES_OPT)
- $(OCAMLOPT) opt -linkpkg -package "$(TEST_REQUIRES)" -o $@ \
+ $(OCAMLFIND) ocamlopt -thread -linkpkg -package "$(TEST_REQUIRES)" -o $@ \
$(REGTESTOBJS:.cmo=.cmx)
.SUFFIXES: .ml .mli .cmo .cmi .cmx
time ./regtest -gen $<
test: regtest
./regtest $(INTESTS) 2> /dev/null
+test.opt: regtest.opt
+ ./regtest.opt $(INTESTS) 2> /dev/null
envtest: regtest
./regtest -dump $(INTESTS) 2> /dev/null
-librarytest: testlibrary.opt
- ./testlibrary.opt index.txt 2>/dev/null >LOG &
+envtest.opt: regtest.opt
+ ./regtest.opt -dump $(INTESTS) 2> /dev/null
+librarytest: testlibrary
+ ./testlibrary -vars -varsprefix cic:/Coq index.txt 2>/dev/null >LOG
+librarytest.opt: testlibrary.opt
+ ./testlibrary.opt -vars -varsprefix cic:/Coq index.txt 2>/dev/null >LOG
MAIN = ./gTopLevel
ARGS =
debug:
- $(OCAMLFIND) query -recursive -predicates byte -a-format \
+ echo "load_printer \"threads.cma\"" > .debug_script
+ $(OCAMLFIND) query -recursive -predicates "mt,byte" -a-format \
helm-cic_unification | \
sed 's/\(.*\)/load_printer "\1"/' \
- > .debug_script
+ >> .debug_script
echo "install_printer CicMetaSubst.fppsubst" >> .debug_script
echo "install_printer CicMetaSubst.fppterm" >> .debug_script
echo "install_printer CicMetaSubst.fppmetasenv" >> .debug_script
ledit $(OCAMLDEBUG) \
-source .debug_script \
+ -I +threads \
$(shell $(OCAMLFIND) query -recursive -i-format $(REQUIRES)) \
$(MAIN) $(ARGS)