diff options
| -rw-r--r-- | Makefile.build | 7 | ||||
| -rw-r--r-- | Makefile.common | 23 | ||||
| -rwxr-xr-x | configure | 14 | ||||
| -rw-r--r-- | myocamlbuild.ml | 4 | ||||
| -rw-r--r-- | scripts/coqmktop.ml | 36 |
5 files changed, 48 insertions, 36 deletions
diff --git a/Makefile.build b/Makefile.build index 4fa0438fa..907ce47c6 100644 --- a/Makefile.build +++ b/Makefile.build @@ -84,12 +84,15 @@ 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) BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) $(USERFLAGS) OPTFLAGS=$(MLINCLUDES) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) +COREBYTEFLAGS=$(COREMLINCLUDES) $(CAMLDEBUG) $(USERFLAGS) +COREOPTFLAGS=$(COREMLINCLUDES) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) DEPFLAGS= -slash $(LOCALINCLUDES) define bestocaml @@ -203,12 +206,12 @@ states:: states/initial.coq $(COQTOPOPT): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) -o $@ + $(HIDE)$(COQMKTOP) -boot -opt $(COREOPTFLAGS) -o $@ $(STRIP) $@ $(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -o $@ + $(HIDE)$(COQMKTOP) -boot -top $(COREBYTEFLAGS) -o $@ $(COQTOPEXE): $(ORDER_ONLY_SEP) $(BESTCOQTOP) cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE) diff --git a/Makefile.common b/Makefile.common index 91498c5df..4f0aa4195 100644 --- a/Makefile.common +++ b/Makefile.common @@ -68,16 +68,21 @@ COQBINARIES:= $(COQMKTOP) $(COQC) \ CSDPCERT:=plugins/micromega/csdpcert$(EXE) +CORESRCDIRS:=\ + config lib kernel kernel/byterun library \ + proofs tactics pretyping interp toplevel \ + parsing printing grammar intf + +PLUGINS:=\ + omega romega micromega quote \ + setoid_ring xml extraction fourier \ + cc funind firstorder \ + rtauto nsatz syntax decl_mode btauto + SRCDIRS:=\ - config tools tools/coqdoc scripts lib \ - kernel kernel/byterun library proofs tactics \ - pretyping interp toplevel parsing printing \ - grammar intf ide/utils ide \ - $(addprefix plugins/, \ - omega romega micromega quote \ - setoid_ring xml extraction fourier \ - cc funind firstorder \ - rtauto nsatz syntax decl_mode btauto) + $(CORESRCDIRS) \ + tools tools/coqdoc scripts ide/utils ide \ + $(addprefix plugins/, $(PLUGINS)) # Order is relevent here because kernel and checker contain files # with the same name @@ -741,13 +741,15 @@ fi ########################################### # bindir, libdir, mandir, docdir, etc. -case $src_spec in - no) COQTOP=${COQSRC} -esac - # OCaml only understand Windows filenames (C:\...) case $ARCH in - win32) COQTOP=`mk_win_path "$COQTOP"` + win32) COQSRC=`mk_win_path "$COQSRC"` + CAMLBIN=`mk_win_path "$CAMLBIN"` + CAMLP4BIN=`mk_win_path "$CAMLP4BIN"` +esac + +case $src_spec in + no) COQTOP=${COQSRC} esac case $ARCH$CYGWIN in @@ -1011,8 +1013,6 @@ BROWSER=`escape_string "$BROWSER"` case $ARCH in win32) - COQSRC=`mk_win_path "$COQSRC"` - COQTOP=`escape_string "$COQTOP"` BINDIR=`escape_string "$BINDIR"` COQSRC=`escape_string "$COQSRC"` diff --git a/myocamlbuild.ml b/myocamlbuild.ml index 966eb6c1c..29514b9eb 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -422,9 +422,9 @@ let extra_rules () = begin if not w32 then N else S ([A"-camlbin";A w32bin;A "-ccopt";P w32ico]) in if opt then rule fo ~prod:fo ~deps:(depsall@depso) ~insert:`top - (cmd [P coqmktop_boot;w32flag;A"-boot";A"-opt";incl fo;A"-o";Px fo]); + (cmd [P coqmktop_boot;w32flag;A"-boot";A"-opt";incl fo;camlp4incl;A"-o";Px fo]); rule fb ~prod:fb ~deps:(depsall@depsb) ~insert:`top - (cmd [P coqmktop_boot;w32flag;A"-boot";A"-top";incl fb;A"-o";Px fb]); + (cmd [P coqmktop_boot;w32flag;A"-boot";A"-top";incl fb;camlp4incl;A"-o";Px fb]); in (** Coq files dependencies *) diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index 6028bb7c8..60dfeb28d 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -12,6 +12,15 @@ open Unix +(* In Win32 outside cygwin, Sys.command calls cmd.exe. When it executes + a command that may contains many double-quote, we should double-quote + the whole ! *) + +let safe_sys_command = + if Sys.os_type = "Win32" then + fun cmd -> Sys.command ("\""^cmd^"\"") + else Sys.command + (* Objects to link *) (* 1. Core objects *) @@ -52,20 +61,19 @@ let top = ref false let echo = ref false let no_start = ref false -let is_ocaml4 = String.sub Coq_config.caml_version 0 2 = "4." +let is_ocaml4 = Coq_config.caml_version.[0] <> '3' -let src_dirs () = +let src_dirs = [ []; ["kernel";"byterun"]; [ "config" ]; [ "toplevel" ] ] let includes () = - let coqlib = Envars.coqlib Errors.error in - let camlp4lib = Envars.camlp4lib () in - List.fold_right - (fun d l -> "-I" :: ("\"" ^ List.fold_left Filename.concat coqlib d ^ "\"") :: l) - (src_dirs ()) - (["-I"; "\"" ^ camlp4lib ^ "\""] @ - ["-I"; "\"" ^ coqlib ^ "\""] @ - if is_ocaml4 then ["-I"; "+compiler-libs"] else []) + (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) + @ (if is_ocaml4 then ["-I"; "+compiler-libs"] else []) (* Transform bytecode object file names in native object file names *) let native_suffix f = @@ -282,7 +290,7 @@ let main () = [] in (* the list of the loaded modules *) - let main_file = create_tmp_main_file modules in + let main_file = Filename.quote (create_tmp_main_file modules) in try let args = options @ (includes ()) @ copts @ tolink @ dynlink @ [ main_file ] in @@ -290,10 +298,6 @@ let main () = let args = if !top then args @ [ "topstart.cmo" ] else args in (* Now, with the .cma, we MUST use the -linkall option *) let command = String.concat " " (prog::"-rectypes"::args) in - (* In Win32, when Sys.command (and hence cmd.exe) executes a command - that may contains many double-quote, we should double-quote the whole ! *) - let command = if Sys.os_type = "Win32" then "\""^command^"\"" else command - in if !echo then begin print_endline command; @@ -302,7 +306,7 @@ let main () = (string_of_int (String.length command)) ^ " characters)"); flush Pervasives.stdout end; - let retcode = Sys.command command in + let retcode = safe_sys_command command in clean main_file; (* command gives the exit code in HSB, and signal in LSB !!! *) if retcode > 255 then retcode lsr 8 else retcode |