diff options
| author | letouzey | 2007-09-15 10:35:59 +0000 |
|---|---|---|
| committer | letouzey | 2007-09-15 10:35:59 +0000 |
| commit | da3edaa7eab2bed17cdfb2c455f2e6b5b0318c4d (patch) | |
| tree | 14b6ae25300dc08c9ca5ff86ad88a78910df7b92 /Makefile.build | |
| parent | 4f39e160d05b0e5501a909b3041589303651670b (diff) | |
* Adding compability with ocaml 3.10 + camlp5 (rework of
the patch by S. Mimram)
* for detecting architecture, also look for /bin/uname
* restore the compatibility of kernel/byterun/coq_interp.c with
ocaml 3.07 (caml_modify vs. modify). There is still an issue
with this 3.07 and 64-bits architecture (see coqdev and a future
bug report).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10122 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/Makefile.build b/Makefile.build index e814699f32..89ebaf6a10 100644 --- a/Makefile.build +++ b/Makefile.build @@ -77,11 +77,9 @@ BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) $(USERFLAGS) OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF) $(USERFLAGS) DEPFLAGS=$(LOCALINCLUDES) -OCAMLC_P4O=$(OCAMLC) -pp $(CAMLP4O) $(BYTEFLAGS) -OCAMLOPT_P4O=$(OCAMLOPT) -pp $(CAMLP4O) $(OPTFLAGS) CAMLP4EXTENDFLAGS=-I . #grammar dependencies are now in camlp4use statements CAMLP4DEPS=sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*\*)@\1@p' -CAMLP4USE=sed -n -e 's@^(\*.*camlp4use: "\(.*\)".*\*)@\1@p' +CAMLP4USE=sed -n -e 's/pa_macro.cmo/pa_macro.cmo -D$(CAMLVERSION)/' -e 's@^(\*.*camlp4use: "\(.*\)".*\*)@\1@p' COQINCLUDES= # coqtop includes itself the needed paths COQ_XML= # is "-xml" when building XML library @@ -707,12 +705,12 @@ toplevel/mltop.cmx: toplevel/mltop.optml | toplevel/mltop.ml4.ml.d toplevel/mlto ## In other words, the Byte-only code doesn't import a new module. toplevel/mltop.byteml: toplevel/mltop.ml4 # no camlp4deps here $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` pr_o.cmo -DByte -impl $< > $@ \ + $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` -DByte -impl $< > $@ \ || ( RV=$$?; rm -f "$@"; exit $${RV} ) toplevel/mltop.optml: toplevel/mltop.ml4 # no camlp4deps here $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` pr_o.cmo -impl $< > $@ \ + $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` -impl $< > $@ \ || ( RV=$$?; rm -f "$@"; exit $${RV} ) # files compiled with -rectypes @@ -804,7 +802,7 @@ endif %.ml4.preprocessed: %.ml4 | %.ml4.d $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ \ + $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ \ || ( RV=$$?; rm -f "$@"; exit $${RV} ) %.vo %.glob: %.v states/initial.coq $(VO_TOOLS_STRICT) | %.v.d $(VO_TOOLS_ORDER_ONLY) @@ -827,7 +825,7 @@ endif #Critical section: # Nobody (in a make -j) should touch the .ml file here. $(SHOW)'OCAMLDEP4 $<' - $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $*.ml \ + $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $*.ml \ || ( RV=$$?; rm -f "$*.ml"; exit $${RV} ) $(HIDE)$(OCAMLDEP) $(DEPFLAGS) $*.ml > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) $(HIDE)echo "let keep_ocamldep_happy Do_not_compile_me = assert false" > $*.ml |