aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/checker.ml3
-rw-r--r--config/coq_config.mli15
-rw-r--r--configure.ml12
-rw-r--r--ide/coq.ml5
-rw-r--r--ide/preferences.ml19
-rw-r--r--kernel/nativelib.ml7
-rw-r--r--lib/envars.ml51
-rw-r--r--lib/envars.mli9
-rw-r--r--lib/flags.ml21
-rw-r--r--lib/flags.mli11
-rw-r--r--tools/coqdep.ml2
-rw-r--r--toplevel/coqargs.ml3
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" ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:22:02 +0000