diff options
| author | filliatr | 1999-09-08 09:46:57 +0000 |
|---|---|---|
| committer | filliatr | 1999-09-08 09:46:57 +0000 |
| commit | 6560ae848fbc6a60e432d48d85fbbf12a8d2e6aa (patch) | |
| tree | 334d3f03e55b561b79b2359cf0a996fbb6202e18 /Makefile | |
| parent | c95679b83d0e69d931018382b68cf9b102a411b8 (diff) | |
- deplacement time stamps dans System (car utilise Unix)
- dependances fichiers camlp4 (quelle merde !)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@56 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 34 |
1 files changed, 25 insertions, 9 deletions
@@ -1,4 +1,3 @@ - # Main Makefile for Coq include config/Makefile @@ -18,7 +17,7 @@ DEPFLAGS=$(INCLUDES) INCLUDES=-I config -I lib -I kernel -I library -I parsing -I $(CAMLP4LIB) -CAMLP4EXTEND=camlp4o pa_extend.cmo +CAMLP4EXTEND=camlp4o $(INCLUDES) pa_extend.cmo OCAMLC_P4O=$(OCAMLC) -pp camlp4o $(BYTEFLAGS) OCAMLOPT_P4O=$(OCAMLOPT) -pp camlp4o $(OPTFLAGS) @@ -30,8 +29,8 @@ CAMLP4OBJS=gramlib.cma CONFIG=config/coq_config.cmo -LIB=lib/pp_control.cmo lib/pp.cmo lib/util.cmo lib/hashcons.cmo \ - lib/dyn.cmo +LIB=lib/pp_control.cmo lib/pp.cmo lib/system.cmo lib/util.cmo \ + lib/hashcons.cmo lib/dyn.cmo KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \ kernel/sign.cmo kernel/evd.cmo kernel/constant.cmo \ @@ -62,9 +61,9 @@ coqtop: $(OBJS) MINICOQOBJS=$(CONFIG) $(LIB) $(KERNEL) \ parsing/lexer.cmo parsing/g_minicoq.cmo toplevel/minicoq.cmo -minicoq: $(OBJS) $(MINICOQOBJS) +minicoq: $(MINICOQOBJS) $(OCAMLC) $(INCLUDES) -o minicoq -custom $(CLIBS) $(CAMLP4OBJS) \ - $(OBJS) $(MINICOQOBJS) $(OSDEPLIBS) + $(MINICOQOBJS) $(OSDEPLIBS) # Literate programming (with ocamlweb) @@ -95,6 +94,20 @@ tags: parsing/lexer.cmo: parsing/lexer.ml $(OCAMLC_P4O) -c $< +# grammar modules with camlp4 + +parsing/q_coqast.cmo: parsing/q_coqast.ml4 + $(OCAMLC) $(BYTEFLAGS) -c -pp "camlp4o q_MLast.cmo -impl" -impl $< + +GRAMMAROBJS=parsing/coqast.cmo parsing/lexer.cmo parsing/pcoq.cmo \ + parsing/q_coqast.cmo parsing/g_prim.cmo + +parsing/grammar.cma: $(GRAMMAROBJS) + $(OCAMLC) $(BYTEFLAGS) -linkall -a -o $@ + +parsing/g_command.cmo: parsing/g_command.ml4 + $(OCAMLC) $(BYTEFLAGS) -c -pp "camlp4o -I parsing pa_extend.cmo grammar.cma -impl" -impl $< + # Default rules .SUFFIXES: .ml .mli .cmo .cmi .cmx .mll .ml4 @@ -141,8 +154,11 @@ cleanconfig:: depend: $(OCAMLDEP) $(DEPFLAGS) */*.mli */*.ml > .depend -# for f in */*.ml4; do \ -# camlp4o pa_extend.cmo pr_o.cmo -impl $$f > >> .depend; \ -# done + for f in */*.ml4; do \ + file=`dirname $$f`/`basename $$f .ml4`; \ + camlp4o $(INCLUDES) pa_extend.cmo pr_o.cmo -impl $$f > $$file.ml; \ + ocamldep $(DEPFLAGS) $$file.ml >> .depend; \ + rm -f $$file.ml; \ + done include .depend |