aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--INSTALL5
-rw-r--r--Makefile6
-rw-r--r--Makefile.build30
-rw-r--r--config/coq_config.mli7
-rw-r--r--configure.ml158
-rw-r--r--kernel/nativelib.ml11
-rw-r--r--lib/envars.ml29
-rw-r--r--lib/envars.mli13
-rw-r--r--lib/flags.ml6
-rw-r--r--lib/flags.mli4
-rw-r--r--tools/coq_makefile.ml23
-rw-r--r--tools/coqmktop.ml13
-rw-r--r--toplevel/usage.ml7
13 files changed, 109 insertions, 203 deletions
diff --git a/INSTALL b/INSTALL
index 955e605c3..d004ea404 100644
--- a/INSTALL
+++ b/INSTALL
@@ -32,6 +32,11 @@ WHAT DO YOU NEED ?
- Objective Caml version 3.12.1 or later
(available at http://caml.inria.fr/)
+ - Findlib (included in OCaml binary distribution under windows and
+ probably available in your distribution and at
+ http://projects.camlcity.org/projects/findlib.html)
+
+
- Camlp5 (version >= 6.02) (Coq compiles with Camlp4 but might be less
well supported)
diff --git a/Makefile b/Makefile
index 554718bc7..e794f05c8 100644
--- a/Makefile
+++ b/Makefile
@@ -69,7 +69,6 @@ USEGRAMMAR := '(\*.*camlp4deps.*grammar'
## Files in the source tree
-YACCFILES:=$(call find, '*.mly')
LEXFILES := $(call find, '*.mll')
export MLLIBFILES := $(call find, '*.mllib')
export ML4BASEFILES := $(call findx, '*.ml4', grep -L -e $(USEGRAMMAR))
@@ -86,10 +85,9 @@ EXISTINGMLI := $(call find, '*.mli')
## Files that will be generated
GENML4FILES:= $(ML4FILES:.ml4=.ml)
-GENMLIFILES:=$(YACCFILES:.mly=.mli)
GENPLUGINSMOD:=$(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml))
-export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \
- tools/tolink.ml kernel/copcodes.ml $(GENPLUGINSMOD)
+export GENMLFILES:=$(LEXFILES:.mll=.ml) $(GENPLUGINSMOD) \
+ tools/tolink.ml kernel/copcodes.ml
export GENHFILES:=kernel/byterun/coq_jumptbl.h
export GENVFILES:=theories/Numbers/Natural/BigN/NMake_gen.v
export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES)
diff --git a/Makefile.build b/Makefile.build
index a790b92b2..9f087cb55 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -94,8 +94,8 @@ HIDE := $(if $(VERBOSE),,@)
LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) )
MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
-OCAMLC := $(OCAMLC) $(CAMLFLAGS)
-OCAMLOPT := $(OCAMLOPT) $(CAMLFLAGS)
+OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS)
+OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS)
BYTEFLAGS=-thread $(CAMLDEBUG) $(USERFLAGS)
OPTFLAGS=-thread $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
@@ -179,7 +179,7 @@ endif
TOTARGET = > "$@" || (RV=$$?; rm -f "$@"; exit $${RV})
###########################################################################
-# Compilation option for .c files
+# Compilation option for .c files
###########################################################################
CINCLUDES= -I $(CAMLHLIB)
@@ -189,9 +189,9 @@ CINCLUDES= -I $(CAMLHLIB)
# NB: We used to do a ranlib after ocamlmklib, but it seems that
# ocamlmklib is already doing it
-$(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN)
+$(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN)
cd $(dir $(LIBCOQRUN)) && \
- $(OCAMLMKLIB) -oc $(COQRUN) $(foreach u,$(BYTERUN),$(notdir $(u)))
+ $(OCAMLFIND) ocamlmklib -oc $(COQRUN) $(foreach u,$(BYTERUN),$(notdir $(u)))
#coq_jumptbl.h is required only if you have GCC 2.0 or later
kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h
@@ -823,34 +823,34 @@ install-latex:
source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf
$(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi)
- $(OCAMLDOC) -latex -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\
+ $(OCAMLFIND) ocamldoc -latex -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\
$(DOCMLIS) -t "Coq mlis documentation" \
-intro $(OCAMLDOCDIR)/docintro -o $@
mli-doc: $(DOCMLIS:.mli=.cmi)
- $(OCAMLDOC) -html -rectypes -I +threads -I $(MYCAMLP4LIB) $(MLINCLUDES) \
+ $(OCAMLFIND) ocamldoc -html -rectypes -I +threads -I $(MYCAMLP4LIB) $(MLINCLUDES) \
$(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \
-t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \
-css-style style.css
ml-dot: $(MLFILES)
- $(OCAMLDOC) -dot -dot-reduce -rectypes -I +threads -I $(CAMLLIB) -I $(MYCAMLP4LIB) $(MLINCLUDES) \
+ $(OCAMLFIND) ocamldoc -dot -dot-reduce -rectypes -I +threads -I $(CAMLLIB) -I $(MYCAMLP4LIB) $(MLINCLUDES) \
$(filter $(addsuffix /%.ml,$(CORESRCDIRS)),$(MLFILES)) -o $(OCAMLDOCDIR)/coq.dot
%_dep.png: %.dot
$(DOT) -Tpng $< -o $@
%_types.dot: %.mli
- $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $<
+ $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $<
-OCAMLDOC_MLLIBD = $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \
+OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \
$(foreach lib,$(|:.mllib.d=_MLLIB_DEPENDENCIES),$(addsuffix .ml,$($(lib))))
%.dot: | %.mllib.d
$(OCAMLDOC_MLLIBD)
ml-doc:
- $(OCAMLDOC) -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(MLSTATICFILES)
+ $(OCAMLFIND) ocamldoc -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(MLSTATICFILES)
parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d
$(OCAMLDOC_MLLIBD)
@@ -862,7 +862,7 @@ tactics/tactics.dot: | tactics/tactics.mllib.d tactics/hightactics.mllib.d
$(OCAMLDOC_MLLIBD)
%.dot: %.mli
- $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $<
+ $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $<
$(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex
(cd $(OCAMLDOCDIR) ; pdflatex $*.tex && pdflatex $*.tex)
@@ -1011,10 +1011,6 @@ endif
$(SHOW)'OCAMLLEX $<'
$(HIDE)$(OCAMLLEX) -o $@ "$*.mll"
-%.ml %.mli: %.mly
- $(SHOW)'OCAMLYACC $<'
- $(HIDE)$(OCAMLYACC) $<
-
plugins/%_mod.ml: plugins/%.mllib
$(SHOW)'ECHO... > $@'
$(HIDE)sed -e "s/\([^ ]\{1,\}\)/let _=Mltop.add_known_module\"\1\" /g" $< > $@
@@ -1054,7 +1050,7 @@ endif
# Since OCaml 3.12.1, we could use again ocamldep directly, thanks to
# the option -ml-synonym
-OCAMLDEP_NG = $(OCAMLDEP) -slash -ml-synonym .ml4
+OCAMLDEP_NG = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4
checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) $(GENFILES)
$(SHOW)'OCAMLDEP $<'
diff --git a/config/coq_config.mli b/config/coq_config.mli
index c63ba65d4..26f4a148c 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -14,12 +14,7 @@ val datadir : string option (* where extra data files are installed *)
val docdir : string (* where the doc is installed *)
val ocaml : string (* names of ocaml binaries *)
-val ocamlc : string
-val ocamlopt : string
-val ocamlmklib : string
-val ocamldoc : string
-val ocamldep : string
-val ocamlyacc : string
+val ocamlfind : string
val ocamllex : string
val camlbin : string (* base directory of OCaml binaries *)
diff --git a/configure.ml b/configure.ml
index e21088584..a1c172cf4 100644
--- a/configure.ml
+++ b/configure.ml
@@ -236,7 +236,7 @@ module Prefs = struct
let docdir = ref (None : string option)
let emacslib = ref (None : string option)
let coqdocdir = ref (None : string option)
- let camldir = ref (None : string option)
+ let ocamlfindcmd = ref (None : string option)
let lablgtkdir = ref (None : string option)
let usecamlp5 = ref true
let camlp5dir = ref (None : string option)
@@ -290,8 +290,8 @@ let args_options = Arg.align [
"<dir> Obsolete: same as -emacslib";
"-coqdocdir", arg_string_option Prefs.coqdocdir,
"<dir> Where to install Coqdoc style files";
- "-camldir", arg_string_option Prefs.camldir,
- "<dir> Specifies the path to the OCaml binaries";
+ "-ocamlfind", arg_string_option Prefs.ocamlfindcmd,
+ "<dir> Specifies the ocamlfind command to use";
"-lablgtkdir", arg_string_option Prefs.lablgtkdir,
"<dir> Specifies the path to the Lablgtk library";
"-usecamlp5", Arg.Set Prefs.usecamlp5,
@@ -352,42 +352,18 @@ let _ = parse_args ()
(** Default OCaml binaries *)
type camlexec =
- { mutable byte : string;
- mutable opt : string;
+ { mutable find : string;
mutable top : string;
- mutable mklib : string;
- mutable dep : string;
- mutable doc : string;
- mutable lex : string;
- mutable yacc : string }
-
-(* TODO: autodetect .opt binaries ? *)
+ mutable lex : string; }
let camlexec =
- { byte = "ocamlc";
- opt = "ocamlopt";
+ { find = "ocamlfind";
top = "ocaml";
- mklib = "ocamlmklib";
- dep = "ocamldep";
- doc = "ocamldoc";
- lex = "ocamllex";
- yacc = "ocamlyacc" }
-
-let reset_caml_byte c o = c.byte <- o
-let reset_caml_opt c o = c.opt <- o
-let reset_caml_doc c o = c.doc <- o
+ lex = "ocamllex"; }
+
let reset_caml_lex c o = c.lex <- o
-let reset_caml_dep c o = c.dep <- o
-
-let rebase_camlexec dir c =
- c.byte <- Filename.concat dir c.byte;
- c.opt <- Filename.concat dir c.opt;
- c.top <- Filename.concat dir c.top;
- c.mklib <- Filename.concat dir c.mklib;
- c.dep <- Filename.concat dir c.dep;
- c.doc <- Filename.concat dir c.doc;
- c.lex <- Filename.concat dir c.lex;
- c.yacc <- Filename.concat dir c.yacc
+let reset_caml_top c o = c.top <- o
+let reset_caml_find c o = c.find <- o
let coq_debug_flag = if !Prefs.debug then "-g" else ""
let coq_profile_flag = if !Prefs.profile then "-p" else ""
@@ -471,29 +447,28 @@ let browser =
(** * OCaml programs *)
let camlbin, caml_version, camllib =
- let camlbin, camlc = match !Prefs.camldir with
- | Some dir ->
- rebase_camlexec dir camlexec;
- Filename.dirname camlexec.byte, camlexec.byte
- | None ->
- try let camlc = which camlexec.byte in Filename.dirname camlc, camlc
- with Not_found ->
- die (sprintf "Error: cannot find '%s' in your path!\n" camlexec.byte ^
- "Please adjust your path or use the -camldir option of ./configure")
+ let () = match !Prefs.ocamlfindcmd with
+ | Some cmd -> reset_caml_find camlexec cmd
+ | None ->
+ try reset_caml_find camlexec (which camlexec.find)
+ with Not_found ->
+ die (sprintf "Error: cannot find '%s' in your path!\n" camlexec.find ^
+ "Please adjust your path or use the -ocamlfind option of ./configure")
in
- let camlcopt = camlc ^ ".opt" in
- let camlc =
- if is_executable camlcopt then begin
- reset_caml_byte camlexec (camlexec.byte ^ ".opt");
- camlcopt
- end
- else if is_executable camlc then
- camlc
- else
- die ("Error: cannot find the executable '"^camlc^"'.") in
- let caml_version, _ = run camlc ["-version"] in
- let camllib, _ = run camlc ["-where"] in
- camlbin, caml_version, camllib
+ if not (is_executable camlexec.find)
+ then die ("Error: cannot find the executable '"^camlexec.find^"'.")
+ else
+ let caml_version, _ = run camlexec.find ["ocamlc";"-version"] in
+ let camllib, _ = run camlexec.find ["printconf";"stdlib"] in
+ let camlbin = (* TODO beurk beurk beurk *)
+ Filename.dirname (Filename.dirname camllib) / "bin/" in
+ let () =
+ if is_executable (camlbin / "ocamllex")
+ then reset_caml_lex camlexec (camlbin / "ocamllex") in
+ let () =
+ if is_executable (camlbin / "ocaml")
+ then reset_caml_top camlexec (camlbin / "ocaml") in
+ camlbin, caml_version, camllib
let camlp4compat = "-loc loc"
@@ -536,12 +511,8 @@ let camltag = match caml_version_list with
(* Convention: we use camldir as a prioritary location for camlpX, if given *)
let which_camlpX base =
- match !Prefs.camldir with
- | Some dir ->
- let file = Filename.concat dir base in
- if is_executable file then file else which base
- | None ->
- which base
+ let file = Filename.concat camlbin base in
+ if is_executable file then file else which base
(* TODO: camlp5dir should rather be the *binary* location, just as camldir *)
(* TODO: remove the late attempts at finding gramlib.cma *)
@@ -638,40 +609,23 @@ let msg_no_dynlink_cmxa () =
printf "and then run ./configure -natdynlink no\n"
let check_native () =
- if !Prefs.byteonly then raise Not_found;
- let camloptopt = camlexec.opt ^ ".opt" in
- if (is_executable camloptopt || program_in_path camloptopt) then
- reset_caml_opt camlexec camloptopt
- else if not (is_executable camlexec.opt || program_in_path camlexec.opt) then
- (msg_no_ocamlopt (); raise Not_found);
- if not (Sys.file_exists (fullcamlpXlibdir/camlpXmod^".cmxa")) then
- (msg_no_camlpX_cmxa (); raise Not_found);
- if not (Sys.file_exists (camllib/"dynlink.cmxa")) then
- (msg_no_dynlink_cmxa (); raise Not_found);
- let version, _ = run camlexec.opt ["-version"] in
- if version <> caml_version then
- printf
- "Warning: Native and bytecode compilers do not have the same version!\n";
- printf "You have native-code compilation. Good!\n"
+ let () = if !Prefs.byteonly then raise Not_found in
+ let version, _ = tryrun camlexec.find ["opt";"-version"] in
+ if version = "" then let () = msg_no_ocamlopt () in raise Not_found
+ else if not (Sys.file_exists (fullcamlpXlibdir/camlpXmod^".cmxa"))
+ then let () = msg_no_camlpX_cmxa () in raise Not_found
+ else if fst (tryrun camlexec.find ["query";"dynlink"]) = ""
+ then let () = msg_no_dynlink_cmxa () in raise Not_found
+ else
+ let () =
+ if version <> caml_version then
+ printf
+ "Warning: Native and bytecode compilers do not have the same version!\n"
+ in printf "You have native-code compilation. Good!\n"
let best_compiler =
try check_native (); "opt" with Not_found -> "byte"
-let _ =
- let camllexopt = camlexec.lex ^ ".opt" in
- if is_executable camllexopt || program_in_path camllexopt then
- reset_caml_lex camlexec camllexopt
-
-let _ =
- let camldepopt = camlexec.dep ^ ".opt" in
- if is_executable camldepopt || program_in_path camldepopt then
- reset_caml_dep camlexec camldepopt
-
-let _ =
- let camldocopt = camlexec.doc ^ ".opt" in
- if is_executable camldocopt || program_in_path camldocopt then
- reset_caml_doc camlexec camldocopt
-
(** * Native dynlink *)
let hasnatdynlink = !Prefs.natdynlink && best_compiler = "opt"
@@ -822,14 +776,14 @@ let strip =
if hasnatdynlink then "true" else "strip"
else
if !Prefs.profile || !Prefs.debug then "true" else begin
- let _, all = run camlexec.byte ["-config"] in
+ let _, all = run camlexec.find ["ocamlc";"-config"] in
let strip = String.concat "" (List.map (fun l ->
match string_split ' ' l with
| "ranlib:" :: cc :: _ -> (* on windows, we greb the right strip *)
Str.replace_first (Str.regexp "ranlib") "strip" cc
| _ -> ""
) all) in
- if strip = "" then "stip" else strip
+ if strip = "" then "strip" else strip
end
(** * md5sum command *)
@@ -1042,12 +996,7 @@ let write_configml f =
pr_o "datadir" datadir;
pr_s "docdir" docdir;
pr_s "ocaml" camlexec.top;
- pr_s "ocamlc" camlexec.byte;
- pr_s "ocamlopt" camlexec.opt;
- pr_s "ocamlmklib" camlexec.mklib;
- pr_s "ocamldep" camlexec.dep;
- pr_s "ocamldoc" camlexec.doc;
- pr_s "ocamlyacc" camlexec.yacc;
+ pr_s "ocamlfind" camlexec.find;
pr_s "ocamllex" camlexec.lex;
pr_s "camlbin" camlbin;
pr_s "camllib" camllib;
@@ -1131,13 +1080,8 @@ let write_makefile f =
pr "VERSION4MACOS=%s\n\n" coq_macos_version;
pr "# Objective-Caml compile command\n";
pr "OCAML=%S\n" camlexec.top;
- pr "OCAMLC=%S\n" camlexec.byte;
- pr "OCAMLMKLIB=%S\n" camlexec.mklib;
- pr "OCAMLOPT=%S\n" camlexec.opt;
- pr "OCAMLDEP=%S\n" camlexec.dep;
- pr "OCAMLDOC=%S\n" camlexec.doc;
+ pr "OCAMLFIND=%S\n" camlexec.find;
pr "OCAMLLEX=%S\n" camlexec.lex;
- pr "OCAMLYACC=%S\n\n" camlexec.yacc;
pr "# The best compiler: native (=opt) or bytecode (=byte)\n";
pr "BEST=%s\n\n" best_compiler;
pr "# Ocaml version number\n";
@@ -1147,8 +1091,6 @@ let write_makefile f =
pr "# Ocaml .h directory\n";
pr "CAMLHLIB=%S\n\n" camllib;
pr "# Caml link command and Caml make top command\n";
- pr "CAMLLINK=%S\n" camlexec.byte;
- pr "CAMLOPTLINK=%S\n\n" camlexec.opt;
pr "# Caml flags\n";
pr "CAMLFLAGS=-rectypes %s\n" coq_annotate_flag;
pr "# User compilation flag\n";
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 29b6bf6de..4be8ced54 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -30,10 +30,6 @@ let output_dir = ".coq-native"
(* Extension of genereted ml files, stored for debugging purposes *)
let source_ext = ".native"
-(* Global settings and utilies for interface with OCaml *)
-let compiler_name =
- if Dynlink.is_native then ocamlopt () else ocamlc ()
-
let ( / ) = Filename.concat
(* We have to delay evaluation of include_dirs because coqlib cannot be guessed
@@ -70,14 +66,15 @@ let call_compiler ml_filename =
remove link_filename;
remove (f ^ ".cmi");
let args =
- (if Dynlink.is_native then "-shared" else "-c")
+ (if Dynlink.is_native then "opt" else "ocamlc")
+ ::(if Dynlink.is_native then "-shared" else "-c")
::"-o"::link_filename
::"-rectypes"
::"-w"::"a"
::include_dirs
@ ["-impl"; ml_filename] in
- if !Flags.debug then Pp.msg_debug (Pp.str (compiler_name ^ " " ^ (String.concat " " args)));
- try CUnix.sys_command compiler_name args = Unix.WEXITED 0, link_filename
+ if !Flags.debug then Pp.msg_debug (Pp.str (ocamlfind () ^ " " ^ (String.concat " " args)));
+ try CUnix.sys_command (ocamlfind ()) args = Unix.WEXITED 0, link_filename
with Unix.Unix_error (e,_,_) ->
Pp.(msg_warning (str (Unix.error_message e)));
false, link_filename
diff --git a/lib/envars.ml b/lib/envars.ml
index ac0b6f722..1cb140b94 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -156,36 +156,23 @@ let coqpath =
let exe s = s ^ Coq_config.exec_extension
-let guess_camlbin () = which (user_path ()) (exe "ocamlc")
+let guess_ocamlfind () = fst (which (user_path ()) (exe "ocamlfind"))
-let camlbin () =
- if !Flags.camlbin_spec then !Flags.camlbin else
- if !Flags.boot then Coq_config.camlbin else
- try guess_camlbin () with Not_found -> Coq_config.camlbin
-
-let ocamlc () = camlbin () / Coq_config.ocamlc
-
-let ocamlopt () = camlbin () / Coq_config.ocamlopt
-
-let camllib () =
- if !Flags.boot then
- Coq_config.camllib
- else
- let _, res = CUnix.run_command (ocamlc () ^ " -where") in
- String.strip res
+let ocamlfind () =
+ if !Flags.ocamlfind_spec then !Flags.ocamlfind else
+ if !Flags.boot then Coq_config.ocamlfind else
+ try guess_ocamlfind () with Not_found -> Coq_config.ocamlfind
(** {2 Camlp4 paths} *)
-let guess_camlp4bin () = which (user_path ()) (exe Coq_config.camlp4)
+let guess_camlp4bin () = snd (which (user_path ()) (exe Coq_config.camlp4))
let camlp4bin () =
if !Flags.camlp4bin_spec then !Flags.camlp4bin else
if !Flags.boot then Coq_config.camlp4bin else
try guess_camlp4bin ()
with Not_found ->
- let cb = camlbin () in
- if Sys.file_exists (cb / exe Coq_config.camlp4) then cb
- else Coq_config.camlp4bin
+ Coq_config.camlp4bin
let camlp4 () = camlp4bin () / exe Coq_config.camlp4
@@ -193,7 +180,7 @@ let camlp4lib () =
if !Flags.boot then
Coq_config.camlp4lib
else
- let ex, res = CUnix.run_command (camlp4 () ^ " -where") in
+ let ex, res = CUnix.run_command (ocamlfind () ^ " query " ^ Coq_config.camlp4) in
match ex with
| Unix.WEXITED 0 -> String.strip res
| _ -> "/dev/null"
diff --git a/lib/envars.mli b/lib/envars.mli
index b62b9f28a..7c20c035a 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -47,17 +47,8 @@ val coqroot : string
the order it gets added to the search path. *)
val coqpath : string list
-(** [camlbin ()] is the path to the ocaml binaries. *)
-val camlbin : unit -> string
-
-(** [camllib ()] is the path to the ocaml standard library. *)
-val camllib : unit -> string
-
-(** [ocamlc ()] is the ocaml bytecode compiler that compiled this Coq. *)
-val ocamlc : unit -> string
-
-(** [ocamlc ()] is the ocaml native compiler that compiled this Coq. *)
-val ocamlopt : unit -> string
+(** [camlbin ()] is the path to the ocamlfind binary. *)
+val ocamlfind : unit -> string
(** [camlp4bin ()] is the path to the camlp4 binary. *)
val camlp4bin : unit -> string
diff --git a/lib/flags.ml b/lib/flags.ml
index 009caa9de..fe580b7ff 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -193,9 +193,9 @@ let is_standard_doc_url url =
let coqlib_spec = ref false
let coqlib = ref "(not initialized yet)"
-(* Options for changing camlbin (used by coqmktop) *)
-let camlbin_spec = ref false
-let camlbin = ref Coq_config.camlbin
+(* Options for changing ocamlfind (used by coqmktop) *)
+let ocamlfind_spec = ref false
+let ocamlfind = ref Coq_config.camlbin
(* Options for changing camlp4bin (used by coqmktop) *)
let camlp4bin_spec = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 544e2a72a..bdb8159ad 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -120,8 +120,8 @@ val coqlib_spec : bool ref
val coqlib : string ref
(** Options for specifying where OCaml binaries reside *)
-val camlbin_spec : bool ref
-val camlbin : string ref
+val ocamlfind_spec : bool ref
+val ocamlfind : string ref
val camlp4bin_spec : bool ref
val camlp4bin : string ref
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 36d29a1e8..954c21d58 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -355,7 +355,7 @@ let clean sds sps =
sds;
print "\n";
print "printenv:\n\t@\"$(COQBIN)coqtop\" -config\n";
- print "\t@echo 'CAMLC =\t$(CAMLC)'\n\t@echo 'CAMLOPTC =\t$(CAMLOPTC)'\n\t@echo 'PP =\t$(PP)'\n\t@echo 'COQFLAGS =\t$(COQFLAGS)'\n";
+ print "\t@echo 'OCAMLFIND =\t$(OCAMLFIND)'\n\t@echo 'PP =\t$(PP)'\n\t@echo 'COQFLAGS =\t$(COQFLAGS)'\n";
print "\t@echo 'COQLIBINSTALL =\t$(COQLIBINSTALL)'\n\t@echo 'COQDOCINSTALL =\t$(COQDOCINSTALL)'\n\n"
let header_includes () = ()
@@ -365,19 +365,19 @@ let implicit () =
let mli_rules () =
print "$(MLIFILES:.mli=.cmi): %.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
print "$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli\n";
- print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
+ print "\t$(OCAMLFIND) ocamldep -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
let ml4_rules () =
print "$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ML4FILES:.ml4=.cmx)): %.cmx: %.ml4\n";
print "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
print "$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4\n";
- print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
+ print "\t$(OCAMLFIND) ocamldep -slash $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
let ml_rules () =
print "$(MLFILES:.ml=.cmo): %.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(MLFILES:.ml=.cmx)): %.cmx: %.ml\n";
print "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
print "$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml\n";
- print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
+ print "\t$(OCAMLFIND) ocamldep -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
let cmxs_rules () = (* order is important here when there is foo.ml and foo.mllib *)
print "$(filter-out $(MLLIBFILES:.mllib=.cmxs),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLPACKFILES:.mlpack=.cmxs)): %.cmxs: %.cmx
\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n";
@@ -455,17 +455,18 @@ let variables is_install opt (args,defs) =
List.iter (fun c -> print " \\
-I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n";
print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n";
- print "CAMLC?=$(OCAMLC) -c -rectypes -thread\n";
- print "CAMLOPTC?=$(OCAMLOPT) -c -rectypes -thread\n";
- print "CAMLLINK?=$(OCAMLC) -rectypes -thread\n";
- print "CAMLOPTLINK?=$(OCAMLOPT) -rectypes -thread\n";
+ print "CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread\n";
+ print "CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread\n";
+ print "CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread\n";
+ print "CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread\n";
+ print "CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib)\n";
print "GRAMMARS?=grammar.cma\n";
print "ifeq ($(CAMLP4),camlp5)
CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma
else
CAMLP4EXTEND=threads.cma
endif\n";
- print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(CAMLLIB)threads/ $(COQSRCLIBS) compat5.cmo \\
+ print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(CAMLLIB)/threads/ $(COQSRCLIBS) compat5.cmo \\
$(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n";
end;
match is_install with
@@ -682,9 +683,9 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
begin
print "mlihtml: $(MLIFILES:.mli=.cmi)\n";
print "\t mkdir $@ || rm -rf $@/*\n";
- print "\t$(OCAMLDOC) -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
+ print "\t$(OCAMLFIND) ocamldoc -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
print "all-mli.tex: $(MLIFILES:.mli=.cmi)\n";
- print "\t$(OCAMLDOC) -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
+ print "\t$(OCAMLFIND) ocamldoc -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
end;
if !some_vfile then
begin
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index be796e695..a6254b2a4 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -149,7 +149,7 @@ let usage () =
prerr_endline "Usage: coqmktop <options> <ocaml options> files\
\nFlags are:\
\n -coqlib dir Specify where the Coq object files are\
-\n -camlbin dir Specify where the OCaml binaries are\
+\n -ocamlfind dir Specify where the ocamlfind binary is\
\n -camlp4bin dir Specify where the Camlp4/5 binaries are\
\n -o exec-file Specify the name of the resulting toplevel\
\n -boot Run in boot mode\
@@ -167,8 +167,8 @@ let parse_args () =
(* Directories *)
| "-coqlib" :: d :: rem ->
Flags.coqlib_spec := true; Flags.coqlib := d ; parse (op,fl) rem
- | "-camlbin" :: d :: rem ->
- Flags.camlbin_spec := true; Flags.camlbin := d ; parse (op,fl) rem
+ | "-ocamlfind" :: d :: rem ->
+ Flags.ocamlfind_spec := true; Flags.ocamlfind := d ; parse (op,fl) rem
| "-camlp4bin" :: d :: rem ->
Flags.camlp4bin_spec := true; Flags.camlp4bin := d ; parse (op,fl) rem
| "-R" :: d :: rem -> parse (incl_all_subdirs d op,fl) rem
@@ -266,10 +266,9 @@ let main () =
let (options, userfiles) = parse_args () in
(* Directories: *)
let () = Envars.set_coqlib ~fail:Errors.error in
- let camlbin = Envars.camlbin () in
let basedir = if !Flags.boot then None else Some (Envars.coqlib ()) in
(* Which ocaml compiler to invoke *)
- let prog = camlbin/(if !opt then "ocamlopt" else "ocamlc") in
+ let prog = if !opt then "opt" else "ocamlc" in
(* Which arguments ? *)
if !opt && !top then failwith "no custom toplevel in native code !";
let flags = if !opt then [] else Coq_config.vmbyteflags in
@@ -284,14 +283,14 @@ let main () =
(std_includes basedir) @ tolink @ [ main_file ] @ topstart
in
if !echo then begin
- let command = String.concat " " (prog::args) in
+ let command = String.concat " " (Envars.ocamlfind ()::prog::args) in
print_endline command;
print_endline
("(command length is " ^
(string_of_int (String.length command)) ^ " characters)");
flush Pervasives.stdout
end;
- let exitcode = run_command prog args in
+ let exitcode = run_command (Envars.ocamlfind ()) (prog::args) in
clean main_file;
exitcode
with reraise -> clean main_file; raise reraise
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 36ecc9fa5..c7d77de8c 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -110,12 +110,7 @@ let print_config () =
if Coq_config.local then Printf.printf "LOCAL=1\n" else Printf.printf "LOCAL=0\n";
Printf.printf "COQLIB=%s/\n" (Envars.coqlib ());
Printf.printf "DOCDIR=%s/\n" (Envars.docdir ());
- Printf.printf "OCAMLDEP=%s\n" Coq_config.ocamldep;
- Printf.printf "OCAMLC=%s\n" Coq_config.ocamlc;
- Printf.printf "OCAMLOPT=%s\n" Coq_config.ocamlopt;
- Printf.printf "OCAMLDOC=%s\n" Coq_config.ocamldoc;
- Printf.printf "CAMLBIN=%s/\n" (Envars.camlbin ());
- Printf.printf "CAMLLIB=%s/\n" (Envars.camllib ());
+ Printf.printf "OCAMLFIND=%s\n" (Envars.ocamlfind ());
Printf.printf "CAMLP4=%s\n" Coq_config.camlp4;
Printf.printf "CAMLP4O=%s\n" Coq_config.camlp4o;
Printf.printf "CAMLP4BIN=%s/\n" (Envars.camlp4bin ());
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 11:49:54 +0000