diff options
| -rw-r--r-- | Makefile.build | 12 | ||||
| -rw-r--r-- | Makefile.common | 4 | ||||
| -rw-r--r-- | configure.ml | 29 |
3 files changed, 27 insertions, 18 deletions
diff --git a/Makefile.build b/Makefile.build index 7cc4351be..147f7e315 100644 --- a/Makefile.build +++ b/Makefile.build @@ -321,7 +321,7 @@ ifeq ($(HASCOQIDE),opt) $(COQIDE): $(LINKIDEOPT) $(SHOW)'OCAMLOPT -o $@' $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa lablgtk.cmxa \ - lablgtksourceview2.cmxa str.cmxa $(IDEFLAGS:.cma=.cmxa) $^ + lablgtksourceview2.cmxa str.cmxa $(IDEFLAGS:.cma=.cmxa) $(IDECDEPSFLAGS) $^ $(STRIP) $@ else $(COQIDE): $(COQIDEBYTE) @@ -656,9 +656,9 @@ bin/votour: lib/cObj$(BESTOBJ) checker/values$(BESTOBJ) checker/votour.ml ifeq ($(CAMLP4),camlp4) tools/compat5.cmo: tools/compat5.mlp - $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -impl' -impl $< + $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -I $(MYCAMLP4LIB) -impl' -impl $< tools/compat5b.cmo: tools/compat5b.mlp - $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -impl' -impl $< + $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -I $(MYCAMLP4LIB) -impl' -impl $< else tools/compat5.cmo: tools/compat5.ml $(OCAMLC) -c $< @@ -877,7 +877,7 @@ dev/printers.cma: | dev/printers.mllib.d grammar/grammar.cma: | grammar/grammar.mllib.d $(SHOW)'Testing $@' @touch test.ml4 - $(HIDE)$(CAMLP4O) -I $(CAMLLIB) $^ -impl test.ml4 -o test.ml + $(HIDE)$(CAMLP4O) -I $(CAMLLIB) -I $(MYCAMLP4LIB) $^ -impl test.ml4 -o test.ml $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) test.ml -o test-grammar @rm -f test-grammar test.* $(SHOW)'OCAMLC -a $@' @@ -885,7 +885,7 @@ grammar/grammar.cma: | grammar/grammar.mllib.d ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -D$(IDEINT) -impl $< -o $@ + $(HIDE)$(CAMLP4O) -I $(MYCAMLP4LIB) $(PR_O) $(CAMLP4USE) -D$(IDEINT) -impl $< -o $@ # pretty printing of the revision number when compiling a checked out # source tree @@ -1019,7 +1019,7 @@ plugins/%_mod.ml: plugins/%.mllib %.ml: %.ml4 | %.ml4.d tools/compat5.cmo tools/compat5b.cmo $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(PR_O) -I $(CAMLLIB) tools/compat5.cmo \ + $(HIDE)$(CAMLP4O) -I $(MYCAMLP4LIB) $(PR_O) -I $(CAMLLIB) tools/compat5.cmo \ $(call CAMLP4DEPS,$<) $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@ %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) | %.v.d diff --git a/Makefile.common b/Makefile.common index 44cdc0baf..8e7cebdcb 100644 --- a/Makefile.common +++ b/Makefile.common @@ -222,8 +222,8 @@ IDEDEPS:=lib/clib.cma lib/xml_lexer.cmo lib/xml_parser.cmo lib/xml_printer.cmo l IDECMA:=ide/ide.cma IDETOPLOOPCMA=ide/coqidetop.cma -LINKIDE:=$(IDEDEPS) $(IDECMA) ide/coqide_main.ml -LINKIDEOPT:=$(IDEOPTDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.ml +LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_main.ml +LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.ml # modules known by the toplevel of Coq diff --git a/configure.ml b/configure.ml index ae8c8c328..e816bc6a2 100644 --- a/configure.ml +++ b/configure.ml @@ -538,15 +538,20 @@ let check_camlp5 testcma = match !Prefs.camlp5dir with in die msg | None -> let dir,_ = tryrun "camlp5" ["-where"] in - if dir <> "" then dir - else if Sys.file_exists (camllib/"camlp5"/testcma) then - camllib/"camlp5" - else if Sys.file_exists (camllib/"site-lib"/"camlp5"/testcma) then - camllib/"site-lib"/"camlp5" - else - let () = printf "No Camlp5 installation found." in - let () = printf "Looking for Camlp4 instead...\n" in - raise NoCamlp5 + let dir2 = + if Sys.file_exists (camllib/"camlp5"/testcma) then + camllib/"camlp5" + else if Sys.file_exists (camllib/"site-lib"/"camlp5"/testcma) then + camllib/"site-lib"/"camlp5" + else + let () = printf "No Camlp5 installation found." in + let () = printf "Looking for Camlp4 instead...\n" in + raise NoCamlp5 + in + (* if the two values are different than camlp5 has been relocated + * and will not be able to find its own files, so we prefer the + * path where the files actually do exist *) + if dir = "" then dir2 else if dir <> dir2 then dir2 else dir let check_camlp5_version () = let s = camlexec.p4 in @@ -744,6 +749,7 @@ let coqide = let lablgtkincludes = ref "" let idearchflags = ref "" let idearchfile = ref "" +let idecdepsflags = ref "" let idearchdef = ref "X11" let coqide_flags () = @@ -758,6 +764,7 @@ let coqide_flags () = end | "opt", "win32" -> idearchfile := "ide/ide_win32_stubs.o"; + idecdepsflags := "-custom"; idearchdef := "WIN32" | _, "win32" -> idearchdef := "WIN32" @@ -1140,7 +1147,9 @@ let write_makefile f = pr "# CoqIde (no/byte/opt)\n"; pr "HASCOQIDE=%s\n" coqide; pr "IDEFLAGS=%s\n" !idearchflags; - pr "IDEOPTDEPS=%s\n" !idearchfile; + pr "IDEOPTCDEPS=%s\n" !idearchfile; + pr "IDECDEPS=%s\n" !idearchfile; + pr "IDECDEPSFLAGS=%s\n" !idecdepsflags; pr "IDEINT=%s\n\n" !idearchdef; pr "# Defining REVISION\n"; pr "CHECKEDOUT=%s\n\n" vcs; |