diff options
author | Stephane Glondu <steph@glondu.net> | 2012-12-29 10:57:43 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-12-29 10:57:43 +0100 |
commit | bf12eb93f3f6a6a824a10878878fadd59745aae0 (patch) | |
tree | 279f64f4b7e4804415ab5731cc7aaa8a4fcfe074 /scripts/coqmktop.ml | |
parent | e0d682ec25282a348d35c5b169abafec48555690 (diff) |
Imported Upstream version 8.4pl1dfsgupstream/8.4pl1dfsg
Diffstat (limited to 'scripts/coqmktop.ml')
-rw-r--r-- | scripts/coqmktop.ml | 25 |
1 files changed, 13 insertions, 12 deletions
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index c8bf689b..5bc77457 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 () 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 () 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 *) @@ -242,8 +244,7 @@ let declare_loading_string () = (* create a temporary main file to link *) let create_tmp_main_file modules = - let main_name = Filename.temp_file "coqmain" ".ml" in - let oc = open_out main_name in + let main_name,oc = Filename.open_temp_file "coqmain" ".ml" in try (* Add the pre-linked modules *) output_string oc "List.iter Mltop.add_known_module [\""; @@ -290,10 +291,10 @@ let main () = [] in (* the list of the loaded modules *) - let main_file = Filename.quote (create_tmp_main_file modules) in + let main_file = create_tmp_main_file modules in try - let args = - options @ (includes ()) @ copts @ tolink @ dynlink @ [ main_file ] in + let args = options @ includes () @ copts @ tolink @ dynlink in + let args = args @ [ Filename.quote main_file ] in (* add topstart.cmo explicitly because we shunted ocamlmktop wrapper *) let args = if !top then args @ [ "topstart.cmo" ] else args in (* Now, with the .cma, we MUST use the -linkall option *) |