NULL =
H=@
-OCAML_FLAGS = -pp $(CAMLP5O) -rectypes
+ifeq ($(ANNOT),true)
+ ANNOTOPTION = -dtypes
+else
+ ANNOTOPTION =
+endif
+
+OCAML_FLAGS = -pp $(CAMLP5O) -rectypes $(ANNOTOPTION)
OCAMLDEP_FLAGS = -pp $(CAMLP5O)
PKGS = -package "$(MATITA_REQUIRES)"
CPKGS = -package "$(MATITA_CREQUIRES)"
OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS) $(OCAMLOPT_DEBUG_FLAGS)
OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAMLDEP_FLAGS)
INSTALL_PROGRAMS= matita matitac
-INSTALL_PROGRAMS_LINKS_MATITA= cicbrowser
-INSTALL_PROGRAMS_LINKS_MATITAC= matitadep matitamake matitaclean matitaprover matitawiki
+INSTALL_PROGRAMS_LINKS_MATITA=
+INSTALL_PROGRAMS_LINKS_MATITAC= matitadep matitaclean matitawiki
MATITA_FLAGS = -noprofile
NODB=false
lablGraphviz.mli \
matitaTypes.mli \
matitaMisc.mli \
- matitamakeLib.mli \
- matitaExcPp.mli \
- matitaInit.mli \
- matitaEngine.mli \
applyTransformation.mli \
- matitaAutoGui.mli \
+ matitaEngine.mli \
+ matitaExcPp.mli \
matitacLib.mli \
- matitaprover.mli \
+ matitaInit.mli \
matitaGtkMisc.mli \
+ matitaAutoGui.mli \
+ virtuals.mli \
matitaScript.mli \
+ predefined_virtuals.mli \
matitaMathView.mli \
matitaGui.mli \
$(NULL)
CMLI = \
matitaTypes.mli \
matitaMisc.mli \
- matitamakeLib.mli \
- matitaExcPp.mli \
- matitaInit.mli \
- matitaEngine.mli \
applyTransformation.mli \
+ matitaEngine.mli \
+ matitaExcPp.mli \
matitacLib.mli \
+ matitaInit.mli \
matitaWiki.mli \
- matitaprover.mli \
$(NULL)
MAINCMLI = \
matitadep.mli \
matitaclean.mli \
- matitamake.mli \
- gragrep.mli \
$(NULL)
# objects for matita (GTK GUI)
ML = buildTimeConf.ml matitaGeneratedGui.ml $(MLI:%.mli=%.ml)
# objects for matitac (batch compiler)
CML = buildTimeConf.ml $(CMLI:%.mli=%.ml)
MAINCML = $(MAINCMLI:%.mli=%.ml)
-
+
PROGRAMS_BYTE = \
- matita matitac cicbrowser matitadep matitaclean \
- matitamake matitaprover matitawiki
-PROGRAMS = $(PROGRAMS_BYTE) matitatop
+ matita matitac matitadep matitaclean \
+ matitawiki
+PROGRAMS = $(PROGRAMS_BYTE)
PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE))
-NOINST_PROGRAMS = dump_moo gragrep
+NOINST_PROGRAMS = dump_moo
NOINST_PROGRAMS_OPT = $(patsubst %,%.opt,$(EXTRA_PROGRAMS))
.PHONY: all
linkonly:
$(H)echo " OCAMLC matita.ml"
- $(H)$(OCAMLC) $(PKGS) -linkpkg -o matita $(CMOS) matita.ml
+ $(H)$(OCAMLC) $(PKGS) -linkpkg -o matita $(CMOS) $(OCAML_DEBUG_FLAGS) matita.ml
$(H)echo " OCAMLC matitac.ml"
- $(H)$(OCAMLC) $(CPKGS) -linkpkg -o matitac $(CCMOS) $(MAINCMOS) matitac.ml
+ $(H)$(OCAMLC) $(CPKGS) -linkpkg -o matitac $(CCMOS) $(MAINCMOS) $(OCAML_DEBUG_FLAGS) matitac.ml
.PHONY: linkonly
matita: matita.ml $(LIB_DEPS) $(CMOS)
$(H)echo " OCAMLC $<"
$(H)echo " OCAMLOPT $<"
$(H)$(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml
-matitatop: matitatop.ml $(CLIB_DEPS) $(CCMOS)
+rottener: rottener.ml $(CLIB_DEPS) $(CCMOS) $(MAINCMOS)
$(H)echo " OCAMLC $<"
- $(H)$(OCAMLC) $(CPKGS) -linkpkg -o $@ toplevellib.cma $(CCMOS) $<
-
-matitaprover: matitac
- $(H)test -f $@ || ln -s $< $@
-matitaprover.opt: matitac.opt
- $(H)test -f $@ || ln -s $< $@
+ $(H)$(OCAMLC) $(CPKGS) -package lablgtk2 -linkpkg -o $@ $(CCMOS) $(MAINCMOS) rottener.ml
+rottener.opt: rottener.ml $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS)
+ $(H)echo " OCAMLOPT $<"
+ $(H)$(OCAMLOPT) $(CPKGS) -package lablgtk2 -linkpkg -o $@ $(CCMXS) $(MAINCMXS) rottener.ml
+clean-rottened:
+ find . -type f -name "*.ma.*.rottened" -exec rm {} \;
matitadep: matitac
$(H)test -f $@ || ln -s $< $@
matitaclean.opt: matitac.opt
$(H)test -f $@ || ln -s $< $@
-matitamake: matitac
- $(H)test -f $@ || ln -s $< $@
-matitamake.opt: matitac.opt
- $(H)test -f $@ || ln -s $< $@
-
-gragrep: matitac
- $(H)test -f $@ || ln -s $< $@
-gragrep.opt: matitac.opt
- $(H)test -f $@ || ln -s $< $@
-
-cicbrowser: matita
- $(H)test -f $@ || ln -s $< $@
-cicbrowser.opt: matita.opt
- $(H)test -f $@ || ln -s $< $@
-
matitaGeneratedGui.ml: matita.glade
$(H)$(LABLGLADECC) -embed $< > matitaGeneratedGui.ml
clean:
$(H)rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o \
$(PROGRAMS) $(PROGRAMS_OPT) \
+ rottener rottener.opt \
$(NOINST_PROGRAMS) $(NOINST_PROGRAMS_OPT) \
$(PROGRAMS_STATIC) \
$(PROGRAMS_UPX) \
$(H)rm -f matita.conf.xml.sample
$(H)rm -rf .matita
-TEST_DIRS = \
- legacy \
- library \
- tests \
- dama \
- contribs/CoRN \
- contribs/RELATIONAL \
- contribs/LOGIC \
- contribs/LAMBDA-TYPES \
- contribs/PREDICATIVE-TOPOLOGY \
+TEST_DIRS = \
+ legacy \
+ library \
+ contribs/character \
+ tests \
+ contribs/dama/dama \
+ contribs/assembly \
+ contribs/CoRN \
+ contribs/RELATIONAL \
+ contribs/LOGIC \
+ contribs/limits \
$(NULL)
# library_auto
-TEST_DIRS_OPT = \
- $(TEST_DIRS) \
+TEST_DIRS_OPT = \
+ $(TEST_DIRS) \
+# contribs/LAMBDA-TYPES \
$(NULL)
.PHONY: tests tests.opt cleantests cleantests.opt
ifeq ($(DISTRIBUTED),yes)
-MATITA_CFLAGS = #-nodb
-
-dist_library: install_preliminaries dist_library@standard-library
-dist_library@%:
- $(H)echo "MATITAMAKE init $*"
- $(H)(HOME=$(WHERE) USER=builder MATITA_RT_BASE_DIR=$(WHERE) MATITA_FLAGS='$(MATITA_CFLAGS)' $(WHERE)/matitamake init $* $(WHERE)/ma/$*)
- $(H)echo "MATITAMAKE publish $*"
- $(H)(HOME=$(WHERE) USER=builder MATITA_RT_BASE_DIR=$(WHERE) MATITA_FLAGS='$(MATITA_CFLAGS)' $(WHERE)/matitamake publish $*)
- $(H)echo "MATITAMAKE destroy $*"
- $(H)(HOME=$(WHERE) USER=builder MATITA_RT_BASE_DIR=$(WHERE) MATITA_FLAGS='$(MATITA_CFLAGS)' $(WHERE)/matitamake destroy $*)
- # sqlite3 only
+dist_library: install_preliminaries
+ $(H)echo "depend"
+ $(H)cd $(WHERE)/ma/standard-library;(HOME=$(WHERE) USER=builder MATITA_RT_BASE_DIR=$(WHERE) MATITA_FLAGS='$(MATITA_CFLAGS)' $(WHERE)/matitadep)
+ $(H)echo "publish"
+ $(H)cd $(WHERE)/ma/standard-library;(HOME=$(WHERE) USER=builder MATITA_RT_BASE_DIR=$(WHERE) MATITA_FLAGS='$(MATITA_CFLAGS)' $(WHERE)/matitac -system -noinnertypes)
+ $(H)echo "destroy"
+ $(H)cd $(WHERE)/ma/standard-library;(HOME=$(WHERE) USER=builder MATITA_RT_BASE_DIR=$(WHERE) MATITA_FLAGS='$(MATITA_CFLAGS)' $(WHERE)/matitaclean)
+# sqlite3 only
$(H)cp $(WHERE)/.matita/matita.db $(WHERE)/metadata.db || true
- #$(H)rm -rf $(WHERE)/.matita/
+#$(H)rm -rf $(WHERE)/.matita/
touch $@
endif
matita.conf.xml \
closed.xml \
gtkmathview.matita.conf.xml \
- template_makefile.in \
AUTHORS \
LICENSE \
$(NULL)
endif
install-arch: install_preliminaries
-install-indep: dist_library
+install-indep:
install_preliminaries : install_preliminaries.stamp
ln -fs matita $(WHERE)/$$p;\
done
$(H)cp -a library/ $(WHERE)/ma/standard-library
- #$(H)cp -a contribs/ $(WHERE)/ma/
+ $(H)cp -a nlibrary/ $(WHERE)/ma/new-standard-library
+
$(H)touch install_preliminaries.stamp
uninstall:
$(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml \
$(STATIC_EXTRA_CLIBS)
strip $@
-matitaprover.opt.static: $(STATIC_LINK) $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml
- $(STATIC_LINK) $(STATIC_CLIBS_PROVER) -- \
- $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml \
- $(STATIC_EXTRA_CLIBS);
- strip $@
matitadep.opt.static: matitac.opt.static
$(H)test -f $@ || ln -s $< $@
matitaclean.opt.static: matitac.opt.static
$(H)test -f $@ || ln -s $< $@
matitawiki.opt.static: matitac.opt.static
$(H)test -f $@ || ln -s $< $@
-matitamake.opt.static: matitac.opt.static
- $(H)test -f $@ || ln -s $< $@
-cicbrowser.opt.static: matita.opt.static
- $(H)test -f $@ || ln -s $< $@
-cicbrowser.opt.static.upx: matita.opt.static.upx
- $(H)test -f $@ || ln -s $< $@
%.upx: %
cp $< $@
$(H)cd ..; otags -vi -r components/ matita/
.PHONY: depend
-
+
depend:
$(H)echo " OCAMLDEP"
$(H)$(OCAMLDEP) *.ml *.mli > .depend
projects / helm.git / blobdiff