diff options
| author | Maxime Dénès | 2017-10-05 18:25:20 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-05 18:25:20 +0200 |
| commit | 5f48abba4280773d89095dce442a33c3ab95011d (patch) | |
| tree | 40f8b9efc3b18aa1cb6b940e532edfeda6220d44 /tools | |
| parent | 85b1deda0348f1fd32f7019fb1e7bfabd297a751 (diff) | |
| parent | ef5aeafb74e33be6ac5b93a9713a3769f5917bd6 (diff) | |
Merge PR #1059: coq_makefile: make sure compile flags for Coq and coq_makefile are in sync (supersed #1039)…
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 15 | ||||
| -rw-r--r-- | tools/coqmktop.ml | 15 |
2 files changed, 21 insertions, 9 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index afe8e62ee3..cfa5526025 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -39,6 +39,7 @@ CAMLP4O := $(COQMF_CAMLP4O) CAMLP4BIN := $(COQMF_CAMLP4BIN) CAMLP4LIB := $(COQMF_CAMLP4LIB) CAMLP4OPTIONS := $(COQMF_CAMLP4OPTIONS) +CAMLFLAGS := $(COQMF_CAMLFLAGS) HASNATDYNLINK := $(COQMF_HASNATDYNLINK) @CONF_FILE@: @PROJECT_FILE@ @@ -100,11 +101,11 @@ AFTER ?= CAMLDONTLINK=camlp5.gramlib,unix,str # OCaml binaries -CAMLC ?= "$(OCAMLFIND)" ocamlc -c -rectypes -thread -CAMLOPTC ?= "$(OCAMLFIND)" opt -c -rectypes -thread -CAMLLINK ?= "$(OCAMLFIND)" ocamlc -rectypes -thread -linkpkg -dontlink $(CAMLDONTLINK) -CAMLOPTLINK ?= "$(OCAMLFIND)" opt -rectypes -thread -linkpkg -dontlink $(CAMLDONTLINK) -CAMLDOC ?= "$(OCAMLFIND)" ocamldoc -rectypes +CAMLC ?= "$(OCAMLFIND)" ocamlc -c +CAMLOPTC ?= "$(OCAMLFIND)" opt -c +CAMLLINK ?= "$(OCAMLFIND)" ocamlc -linkpkg -dontlink $(CAMLDONTLINK) +CAMLOPTLINK ?= "$(OCAMLFIND)" opt -linkpkg -dontlink $(CAMLDONTLINK) +CAMLDOC ?= "$(OCAMLFIND)" ocamldoc CAMLDEP ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack # DESTDIR is prepended to all installation paths @@ -114,8 +115,6 @@ DESTDIR ?= CAMLDEBUG ?= COQDEBUG ?= -# Extra flags to the OCaml compiler -CAMLFLAGS ?= # Extra packages to be linked in (as in findlib -package) CAMLPKGS ?= @@ -749,7 +748,7 @@ printenv:: # file you can extend the merlin-hook target in @LOCAL_FILE@ .merlin: $(SHOW)'FILL .merlin' - $(HIDE)echo 'FLG -rectypes -thread' > .merlin + $(HIDE)echo 'FLG $(COQMF_CAMLFLAGS)' > .merlin $(HIDE)echo 'B $(COQLIB)' >> .merlin $(HIDE)echo 'S $(COQLIB)' >> .merlin $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml index 28a3c791cb..c21db300ad 100644 --- a/tools/coqmktop.ml +++ b/tools/coqmktop.ml @@ -252,6 +252,17 @@ let create_tmp_main_file modules = with reraise -> clean main_name; raise reraise +(* TODO: remove once OCaml 4.04 is adopted *) +let split_on_char sep s = + let r = ref [] in + let j = ref (String.length s) in + for i = String.length s - 1 downto 0 do + if s.[i] = sep then begin + r := String.sub s (i + 1) (!j - i - 1) :: !r; + j := i + end + done; + String.sub s 0 !j :: !r (** {6 Main } *) @@ -271,8 +282,10 @@ let main () = try (* - We add topstart.cmo explicitly because we shunted ocamlmktop wrapper. - With the coq .cma, we MUST use the -linkall option. *) + let coq_camlflags = + List.filter ((<>) "") (split_on_char ' ' Coq_config.caml_flags) in let args = - "-linkall" :: "-rectypes" :: "-w" :: "-31" :: flags @ copts @ options @ + coq_camlflags @ "-linkall" :: "-w" :: "-31" :: flags @ copts @ options @ (std_includes basedir) @ tolink @ [ main_file ] @ topstart in if !echo then begin |