Merge PR #8572: [config] Miscellaneous cleaning of configuration variables.

12 files changed, 37 insertions, 121 deletions

diff --git a/checker/checker.ml b/checker/checker.ml
index fd2725c859..d3d114d7d7 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -321,8 +321,7 @@ let parse_args argv =
     | "-coqlib" :: s :: rem ->
       if not (exists_dir s) then 
 	fatal_error (str "Directory '" ++ str s ++ str "' does not exist") false;
-      Flags.coqlib := s;
-      Flags.coqlib_spec := true;
+      Envars.set_user_coqlib s;
       parse rem
 
     | ("-I"|"-include") :: d :: "-as" :: p :: rem -> deprecated "-I"; set_include d p; parse rem
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 29065d3ef8..22d8c49fd1 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -23,26 +23,17 @@ val configdirsuffix : string (* config files relative to installation prefix *)
 val datadirsuffix : string   (* data files relative to installation prefix *)
 val docdirsuffix : string    (* doc directory relative to installation prefix *)
 
-val ocaml : string      (* names of ocaml binaries *)
 val ocamlfind : string
-val ocamllex : string
-
-val camlbin : string    (* base directory of OCaml binaries *)
-val camllib : string    (* for Dynlink *)
 
 val camlp5o : string    (* name of the camlp5o executable *)
 val camlp5bin : string  (* base directory for camlp5 binaries *)
 val camlp5lib : string  (* where is the library of camlp5 *)
 val camlp5compat : string (* compatibility argument to camlp5 *)
 
-val coqideincl : string (* arguments for building coqide (e.g. lablgtk) *)
-val cflags : string     (* arguments passed to gcc *)
 val caml_flags : string     (* arguments passed to ocamlc (ie. CAMLFLAGS) *)
 
-val best : string       (* byte/opt *)
 val arch : string       (* architecture *)
 val arch_is_win32 : bool
-val vmbyteflags : string list (* -custom/-dllib -lcoqrun *)
 
 val version : string    (* version number of Coq *)
 val caml_version : string    (* OCaml version used to compile Coq *)
@@ -52,8 +43,6 @@ val compile_date : string (* compile date *)
 val vo_magic_number : int
 val state_magic_number : int
 
-val core_src_dirs : string list
-val plugins_dirs : string list
 val all_src_dirs : string list
 
 val exec_extension : string (* "" under Unix, ".exe" under MS-windows *)
@@ -62,13 +51,9 @@ val browser : string
 (** default web browser to use, may be overridden by environment
     variable COQREMOTEBROWSER *)
 
-val has_coqide : string
 val gtk_platform : [`QUARTZ | `WIN32 | `X11]
 
 val has_natdynlink : bool
-val natdynlinkflag : string (* special cases of natdynlink (e.g. MacOS 10.5) *)
-
-val flambda_flags : string list
 
 val wwwcoq : string
 val wwwrefman : string
diff --git a/configure.ml b/configure.ml
index 48e55546d1..a508ac6071 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1183,13 +1183,11 @@ let write_configml f =
   let pr_i = pr "let %s = %d\n" in
   let pr_p s o = pr "let %s = %S\n" s
     (match o with Relative s -> s | Absolute s -> s) in
-  let pr_l  n l = pr "let %s = [%s]\n" n (String.concat ";" (List.map (fun s -> "\"" ^ s ^ "\"") l)) in
   let pr_li n l = pr "let %s = [%s]\n" n (String.concat ";" (List.map string_of_int l)) in
   pr "(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)\n";
   pr "(* Exact command that generated this file: *)\n";
   pr "(* %s *)\n\n" (String.concat " " (Array.to_list Sys.argv));
   pr_b "local" !prefs.local;
-  pr "let vmbyteflags = ["; List.iter (pr "%S;") vmbyteflags; pr "]\n";
   pr_s "coqlib" coqlib;
   pr_s "configdir" configdir;
   pr_s "datadir" datadir;
@@ -1198,18 +1196,12 @@ let write_configml f =
   pr_p "configdirsuffix" configdirsuffix;
   pr_p "datadirsuffix" datadirsuffix;
   pr_p "docdirsuffix" docdirsuffix;
-  pr_s "ocaml" camlexec.top;
   pr_s "ocamlfind" camlexec.find;
-  pr_s "ocamllex" camlexec.lex;
-  pr_s "camlbin" camlbin;
-  pr_s "camllib" camllib;
   pr_s "camlp5o" camlp5o;
   pr_s "camlp5bin" camlp5bindir;
   pr_s "camlp5lib" camlp5libdir;
   pr_s "camlp5compat" camlp5compat;
-  pr_s "cflags" cflags;
   pr_s "caml_flags" caml_flags;
-  pr_s "best" best_compiler;
   pr_s "version" coq_version;
   pr_s "caml_version" caml_version;
   pr_li "caml_version_nums" caml_version_nums;
@@ -1218,12 +1210,8 @@ let write_configml f =
   pr_s "arch" arch;
   pr_b "arch_is_win32" arch_is_win32;
   pr_s "exec_extension" exe;
-  pr_s "coqideincl" !lablgtkincludes;
-  pr_s "has_coqide" coqide;
   pr "let gtk_platform = `%s\n" !idearchdef;
   pr_b "has_natdynlink" hasnatdynlink;
-  pr_s "natdynlinkflag" natdynlinkflag;
-  pr_l "flambda_flags" !prefs.flambda_flags;
   pr_i "vo_magic_number" vo_magic;
   pr_i "state_magic_number" state_magic;
   pr_s "browser" browser;
diff --git a/ide/coq.ml b/ide/coq.ml
index e948360191..88ffb4f0b7 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -42,14 +42,11 @@ let version () =
       "The Coq Proof Assistant, version %s (%s)\
        \nArchitecture %s running %s operating system\
        \nGtk version is %s\
-       \nThis is %s (%s is the best one for this architecture and OS)\
-       \n"
+       \nThis is %s \n"
       ver date
       Coq_config.arch Sys.os_type
       (let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z)
       (Filename.basename Sys.executable_name)
-      Coq_config.best
-
 
 (** * Initial checks by launching test coqtop processes *)
 
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 955ee87840..3f10af04c9 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -345,8 +345,15 @@ let _ = attach_modifiers modifier_for_queries "<Actions>/Queries/"
 let modifiers_valid =
   new preference ~name:["modifiers_valid"] ~init:"<Alt><Control><Shift>" ~repr:Repr.(string)
 
+let browser_cmd_fmt =
+ try
+  let coq_netscape_remote_var = "COQREMOTEBROWSER" in
+  Sys.getenv coq_netscape_remote_var
+ with
+  Not_found -> Coq_config.browser
+
 let cmd_browse =
-  new preference ~name:["cmd_browse"] ~init:Flags.browser_cmd_fmt ~repr:Repr.(string)
+  new preference ~name:["cmd_browse"] ~init:browser_cmd_fmt ~repr:Repr.(string)
 
 let cmd_editor =
   let init = if Sys.os_type = "Win32" then "NOTEPAD %s" else "emacs %s" in
@@ -359,6 +366,14 @@ let text_font =
   in
   new preference ~name:["text_font"] ~init ~repr:Repr.(string)
 
+let is_standard_doc_url url =
+  let wwwcompatprefix = "http://www.lix.polytechnique.fr/coq/" in
+  let n = String.length Coq_config.wwwcoq in
+  let n' = String.length Coq_config.wwwrefman in
+  url = Coq_config.localwwwrefman ||
+  url = Coq_config.wwwrefman ||
+  url = wwwcompatprefix ^ String.sub Coq_config.wwwrefman n (n'-n)
+
 let doc_url =
 object
   inherit [string] preference
@@ -366,7 +381,7 @@ object
     as super
 
   method! set v =
-    if not (Flags.is_standard_doc_url v) &&
+    if not (is_standard_doc_url v) &&
       v <> use_default_doc_url &&
       (* Extra hack to support links to last released doc version *)
       v <> Coq_config.wwwcoq ^ "doc" &&
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 6edb387bb1..d294f2060e 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -11,7 +11,6 @@ open Util
 open Nativevalues
 open Nativecode
 open CErrors
-open Envars
 
 (** This file provides facilities to access OCaml compiler and dynamic linker,
 used by the native compiler. *)
@@ -37,7 +36,7 @@ let ( / ) = Filename.concat
 (* We have to delay evaluation of include_dirs because coqlib cannot be guessed
 until flags have been properly initialized *)
 let include_dirs () =
-  [Filename.get_temp_dir_name (); coqlib () / "kernel"; coqlib () / "library"]
+  [Filename.get_temp_dir_name (); Envars.coqlib () / "kernel"; Envars.coqlib () / "library"]
 
 (* Pointer to the function linking an ML object into coq's toplevel *)
 let load_obj = ref (fun _x -> () : string -> unit)
@@ -99,9 +98,9 @@ let call_compiler ?profile:(profile=false) ml_filename =
        ::"-w"::"a"
        ::include_dirs) @
       ["-impl"; ml_filename] in
-  if !Flags.debug then Feedback.msg_debug (Pp.str (ocamlfind () ^ " " ^ (String.concat " " args)));
+  if !Flags.debug then Feedback.msg_debug (Pp.str (Envars.ocamlfind () ^ " " ^ (String.concat " " args)));
   try
-    let res = CUnix.sys_command (ocamlfind ()) args in
+    let res = CUnix.sys_command (Envars.ocamlfind ()) args in
     let res = match res with
       | Unix.WEXITED 0 -> true
       | Unix.WEXITED _n | Unix.WSIGNALED _n | Unix.WSTOPPED _n ->
diff --git a/lib/envars.ml b/lib/envars.ml
index 3ee0c7106b..cf76b6ebc8 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -36,21 +36,6 @@ let path_to_list p =
   let sep = if String.equal Sys.os_type "Win32" then ';' else ':' in
     String.split sep p
 
-let user_path () =
-  path_to_list (Sys.getenv "PATH") (* may raise Not_found *)
-
-(* Finding a name in path using the equality provided by the file system *)
-(* whether it is case-sensitive or case-insensitive *)
-let rec which l f =
-  match l with
-    | [] ->
-      raise Not_found
-    | p :: tl ->
-      if Sys.file_exists (p / f) then
-	p
-      else
-	which tl f
-
 let expand_path_macros ~warn s =
   let rec expand_atom s i =
     let l = String.length s in
@@ -120,14 +105,19 @@ let guess_coqlib fail =
         fail "cannot guess a path for Coq libraries; please use -coqlib option")
   )
 
+let coqlib : string option ref = ref None
+let set_user_coqlib path = coqlib := Some path
+
 (** coqlib is now computed once during coqtop initialization *)
 
 let set_coqlib ~fail =
-  if not !Flags.coqlib_spec then
+  match !coqlib with
+  | Some _ -> ()
+  | None ->
     let lib = if !Flags.boot then coqroot else guess_coqlib fail in
-    Flags.coqlib := lib
+    coqlib := Some lib
 
-let coqlib () = !Flags.coqlib
+let coqlib () = Option.default "" !coqlib
 
 let docdir () =
   (* This assumes implicitly that the suffix is non-trivial *)
@@ -155,29 +145,8 @@ let coqpath =
 
 (** {2 Caml paths} *)
 
-let exe s = s ^ Coq_config.exec_extension
-
 let ocamlfind () = Coq_config.ocamlfind
 
-(** {2 Camlp5 paths} *)
-
-let guess_camlp5bin () = which (user_path ()) (exe "camlp5")
-
-let camlp5bin () =
-  if !Flags.boot then Coq_config.camlp5bin else
-    try guess_camlp5bin ()
-    with Not_found ->
-      Coq_config.camlp5bin
-
-let camlp5lib () =
-  if !Flags.boot then
-    Coq_config.camlp5lib
-  else
-    let ex, res = CUnix.run_command (ocamlfind () ^ " query camlp5") in
-    match ex with
-      | Unix.WEXITED 0 -> String.strip res
-      | _ -> "/dev/null"
-
 (** {1 XDG utilities} *)
 
 let xdg_data_home warn =
@@ -209,8 +178,8 @@ let print_config ?(prefix_var_name="") f coq_src_subdirs =
   fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ());
   fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ());
   fprintf f "%sCAMLP5O=%s\n" prefix_var_name Coq_config.camlp5o;
-  fprintf f "%sCAMLP5BIN=%s/\n" prefix_var_name (camlp5bin ());
-  fprintf f "%sCAMLP5LIB=%s\n" prefix_var_name (camlp5lib ());
+  fprintf f "%sCAMLP5BIN=%s/\n" prefix_var_name Coq_config.camlp5bin;
+  fprintf f "%sCAMLP5LIB=%s\n" prefix_var_name Coq_config.camlp5lib;
   fprintf f "%sCAMLP5OPTIONS=%s\n" prefix_var_name Coq_config.camlp5compat;
   fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags;
   fprintf f "%sHASNATDYNLINK=%s\n" prefix_var_name
diff --git a/lib/envars.mli b/lib/envars.mli
index 66b86252c7..ebf86d0650 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -41,6 +41,9 @@ val configdir : unit -> string
 (** [set_coqlib] must be runned once before any access to [coqlib] *)
 val set_coqlib : fail:(string -> string) -> unit
 
+(** [set_user_coqlib path] sets the coqlib directory explicitedly. *)
+val set_user_coqlib : string -> unit
+
 (** [coqbin] is the name of the current executable. *)
 val coqbin : string
 
@@ -58,12 +61,6 @@ val coqpath : string list
 (** [camlfind ()] is the path to the ocamlfind binary. *)
 val ocamlfind : unit -> string
 
-(** [camlp5bin ()] is the path to the camlp5 binary. *)
-val camlp5bin : unit -> string
-
-(** [camlp5lib ()] is the path to the camlp5 library. *)
-val camlp5lib : unit -> string
-
 (** Coq tries to honor the XDG Base Directory Specification to access
     the user's configuration files.
 
diff --git a/lib/flags.ml b/lib/flags.ml
index 7e0065beba..4d6c36f55d 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -121,27 +121,6 @@ let warn = ref true
 let make_warn flag = warn := flag;  ()
 let if_warn f x = if !warn then f x
 
-(* Flags for external tools *)
-
-let browser_cmd_fmt =
- try
-  let coq_netscape_remote_var = "COQREMOTEBROWSER" in
-  Sys.getenv coq_netscape_remote_var
- with
-  Not_found -> Coq_config.browser
-
-let is_standard_doc_url url =
-  let wwwcompatprefix = "http://www.lix.polytechnique.fr/coq/" in
-  let n = String.length Coq_config.wwwcoq in
-  let n' = String.length Coq_config.wwwrefman in
-  url = Coq_config.localwwwrefman ||
-  url = Coq_config.wwwrefman ||
-  url = wwwcompatprefix ^ String.sub Coq_config.wwwrefman n (n'-n)
-
-(* Options for changing coqlib *)
-let coqlib_spec = ref false
-let coqlib = ref "(not initialized yet)"
-
 (* Level of inlining during a functor application *)
 
 let default_inline_level = 100
diff --git a/lib/flags.mli b/lib/flags.mli
index 02d8a3adc1..398f22ab4f 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -118,17 +118,6 @@ val without_option : bool ref -> ('a -> 'b) -> 'a -> 'b
 (** Temporarily extends the reference to a list *)
 val with_extra_values : 'c list ref -> 'c list -> ('a -> 'b) -> 'a -> 'b
 
-(** Options for external tools *)
-
-(** Returns string format for default browser to use from Coq or CoqIDE *)
-val browser_cmd_fmt : string
-
-val is_standard_doc_url : string -> bool
-
-(** Options for specifying where coq librairies reside *)
-val coqlib_spec : bool ref
-val coqlib : string ref
-
 (** Level of inlining during a functor application *)
 val set_inline_level : int -> unit
 val get_inline_level : unit -> int
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 7db0b28908..ba88069be9 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -496,7 +496,7 @@ let rec parse = function
   | "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll
   | "-exclude-dir" :: r :: ll -> System.exclude_directory r; parse ll
   | "-exclude-dir" :: [] -> usage ()
-  | "-coqlib" :: r :: ll -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll
+  | "-coqlib" :: r :: ll -> Envars.set_user_coqlib r; parse ll
   | "-coqlib" :: [] -> usage ()
   | "-suffix" :: s :: ll -> suffixe := s ; parse ll
   | "-suffix" :: [] -> usage ()
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 98a28bb2b6..1baaa8a45f 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -376,8 +376,7 @@ let parse_args arglist : coq_cmdopts * string list =
 
     (* Options with one arg *)
     |"-coqlib" ->
-      Flags.coqlib_spec := true;
-      Flags.coqlib := (next ());
+      Envars.set_user_coqlib (next ());
       oval
 
     |"-async-proofs" ->