aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorfilliatr1999-08-16 13:17:30 +0000
committerfilliatr1999-08-16 13:17:30 +0000
commitb4a932fad873357ebe50bf571858e9fca842b9e5 (patch)
tree830568b3009763e6d9fac0430e258c0d323eefcf /Makefile
parent9380f25b735834a3c9017eeeb0f8795cc474325b (diff)
Initial revision
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile68
1 files changed, 68 insertions, 0 deletions
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000000..cb3d0b2a9f
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,68 @@
+
+# Main Makefile for Coq
+
+include config/Makefile
+
+noargument:
+ @echo Please use either
+ @echo " ./configure"
+ @echo " make world"
+ @echo " make install"
+ @echo " make cleanall"
+ @echo or make archclean
+
+INCLUDES=-I config -I lib
+BYTEFLAGS=$(INCLUDES) $(CAMLDEBUG)
+OPTFLAGS=$(INCLUDES) $(CAMLTIMEPROF)
+OCAMLDEP=ocamldep
+DEPFLAGS=$(INCLUDES)
+
+# Objects files
+
+CONFIG=config/coq_config.cmo
+
+LIB=lib/pp_control.cmo lib/pp.cmo lib/util.cmo lib/hashcons.cmo
+
+KERNEL=kernel/names.cmo
+
+OBJS=$(CONFIG) $(LIB) $(KERNEL)
+
+# Targets
+
+world: $(OBJS)
+
+# Default rules
+
+.SUFFIXES: .ml .mli .cmo .cmi .cmx
+
+.ml.cmo:
+ $(OCAMLC) $(BYTEFLAGS) -c $<
+
+.mli.cmi:
+ $(OCAMLC) $(BYTEFLAGS) -c $<
+
+.ml.cmx:
+ $(OCAMLOPT) $(OPTFLAGS) -c $<
+
+# Cleaning
+
+archclean::
+ rm -f config/*.cmx config/*.[so]
+ rm -f lib/*.cmx lib/*.[so]
+ rm -f kernel/*.cmx kernel/*.[so]
+
+cleanall:: archclean
+ rm -f *~
+ rm -f config/*.cm[io] config/*~
+ rm -f lib/*.cm[io] lib/*~
+ rm -f kernel/*.cm[io] kernel/*~
+
+cleanconfig::
+ rm -f config/Makefile config/coq_config.ml
+
+# Dependencies
+
+depend:
+ $(OCAMLDEP) $(DEPFLAGS) */*.mli */*.ml > .depend
+
+include .depend