diff options
| author | letouzey | 2012-10-23 18:06:26 +0000 |
|---|---|---|
| committer | letouzey | 2012-10-23 18:06:26 +0000 |
| commit | bdc7217d03a109a9149d7c93bbe2f95b1df480f5 (patch) | |
| tree | e5629f161ca05baa15552fc7cc06539777d9219b | |
| parent | 40b00efff7e47b22c80c677514f9d689c918383c (diff) | |
Coqmktop: missing -I (fix #2851)
The modules used in coqmktop's temporary main file should have
their .cmi in the search path, hence a small set of -I is required:
lib, toplevel. We do not place their the full list to avoid issues
with the win32 command-line length
Btw, coqmktop -boot now also builds its list of -I instead of receiving
them via its command-line, it's simpler this way...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15926 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile.build | 5 | ||||
| -rw-r--r-- | scripts/coqmktop.ml | 16 |
2 files changed, 11 insertions, 10 deletions
diff --git a/Makefile.build b/Makefile.build index 44be3c3d0c..c3768528ed 100644 --- a/Makefile.build +++ b/Makefile.build @@ -102,7 +102,6 @@ HIDE := $(if $(VERBOSE),,@) LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) ) MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) -COREMLINCLUDES=$(addprefix -I , $(CORESRCDIRS)) -I $(MYCAMLP4LIB) OCAMLC := $(TYPEREX) $(OCAMLC) $(CAMLFLAGS) OCAMLOPT := $(TYPEREX) $(OCAMLOPT) $(CAMLFLAGS) @@ -222,7 +221,7 @@ minibyte: $(COQTOPBYTE) pluginsbyte ifeq ($(BEST),opt) $(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -boot -opt $(COREMLINCLUDES) $(OPTFLAGS) -o $@ + $(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) -o $@ $(STRIP) $@ else $(COQTOPEXE): $(COQTOPBYTE) @@ -231,7 +230,7 @@ endif $(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -boot -top $(COREMLINCLUDES) $(BYTEFLAGS) -o $@ + $(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -o $@ LOCALCHKLIBS:=$(addprefix -I , $(CHKSRCDIRS) ) CHKLIBS:=$(LOCALCHKLIBS) -I $(MYCAMLP4LIB) diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index 230ab75928..441926becf 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -63,16 +63,18 @@ let no_start = ref false let is_ocaml4 = Coq_config.caml_version.[0] <> '3' +(* Since the .cma are given with their relative paths (e.g. "lib/clib.cma"), + we only need to include directories mentionned in the temp main ml file + below (for accessing the corresponding .cmi). *) + let src_dirs = - [ []; ["kernel";"byterun"]; [ "config" ]; [ "toplevel" ] ] + [ []; ["lib"]; ["toplevel"]; ["kernel";"byterun"] ] let includes () = - (if !Flags.boot then [] (* the include flags are given on the cmdline *) - else - let coqlib = Envars.coqlib Errors.error in - let mkdir d = "\"" ^ List.fold_left Filename.concat coqlib d ^ "\"" in - let camlp4incl = ["-I"; "\"" ^ Envars.camlp4lib () ^ "\""] in - List.fold_right (fun d l -> "-I" :: mkdir d :: l) src_dirs camlp4incl) + let coqlib = if !Flags.boot then "." else Envars.coqlib Errors.error in + let mkdir d = "\"" ^ List.fold_left Filename.concat coqlib d ^ "\"" in + (List.fold_right (fun d l -> "-I" :: mkdir d :: l) src_dirs []) + @ ["-I"; "\"" ^ Envars.camlp4lib () ^ "\""] @ (if is_ocaml4 then ["-I"; "+compiler-libs"] else []) (* Transform bytecode object file names in native object file names *) |