diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/envars.ml | 51 | ||||
| -rw-r--r-- | lib/envars.mli | 9 | ||||
| -rw-r--r-- | lib/flags.ml | 31 | ||||
| -rw-r--r-- | lib/flags.mli | 13 |
4 files changed, 19 insertions, 85 deletions
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..c8f19f2f11 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -66,25 +66,25 @@ let we_are_parsing = ref false (* Current means no particular compatibility consideration. For correct comparisons, this constructor should remain the last one. *) -type compat_version = V8_6 | V8_7 | Current +type compat_version = V8_7 | V8_8 | Current let compat_version = ref Current let version_compare v1 v2 = match v1, v2 with - | V8_6, V8_6 -> 0 - | V8_6, _ -> -1 - | _, V8_6 -> 1 | V8_7, V8_7 -> 0 | V8_7, _ -> -1 | _, V8_7 -> 1 + | V8_8, V8_8 -> 0 + | V8_8, _ -> -1 + | _, V8_8 -> 1 | Current, Current -> 0 let version_strictly_greater v = version_compare !compat_version v > 0 let version_less_or_equal v = not (version_strictly_greater v) let pr_version = function - | V8_6 -> "8.6" | V8_7 -> "8.7" + | V8_8 -> "8.8" | Current -> "current" (* Translate *) @@ -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..3d9eafde75 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -58,7 +58,7 @@ val we_are_parsing : bool ref (* Set Printing All flag. For some reason it is a global flag *) val raw_print : bool ref -type compat_version = V8_6 | V8_7 | Current +type compat_version = V8_7 | V8_8 | Current val compat_version : compat_version ref val version_compare : compat_version -> compat_version -> int val version_strictly_greater : compat_version -> bool @@ -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 |