From ec1e83e85543a793dc248e9d2f47dd146f9a913d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 27 Sep 2018 02:25:16 +0200 Subject: [envars] Defer CAMLP5 location to configure. These functions are unused, and configure should suffice for this purpose. --- lib/envars.ml | 40 ++-------------------------------------- lib/envars.mli | 6 ------ 2 files changed, 2 insertions(+), 44 deletions(-) (limited to 'lib') diff --git a/lib/envars.ml b/lib/envars.ml index 3ee0c7106b..dbd381bb2a 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 @@ -155,29 +140,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 +173,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..93d3cf9d0c 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -58,12 +58,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. -- cgit v1.2.3 From 4de95593380294b3d2c4f10f346aaf9bb5d4d6eb Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 27 Sep 2018 02:28:30 +0200 Subject: [lib] [flags] Move private IDE functions to `ide` --- lib/flags.ml | 17 ----------------- lib/flags.mli | 7 ------- 2 files changed, 24 deletions(-) (limited to 'lib') diff --git a/lib/flags.ml b/lib/flags.ml index 7e0065beba..54f25e209d 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -121,23 +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)" diff --git a/lib/flags.mli b/lib/flags.mli index 02d8a3adc1..0faad1a541 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -118,13 +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 -- cgit v1.2.3 From 9d3a2d042500094befe4b88f3aa73693bc287ed9 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 27 Sep 2018 02:33:10 +0200 Subject: [lib] [flags] Move coqlib handling out of `Flags` The relevant logic is already in `Envars`, so it makes sense to make it private and don't expose the low-level implementation of the logic. --- lib/envars.ml | 14 +++++++++++--- lib/envars.mli | 3 +++ lib/flags.ml | 4 ---- lib/flags.mli | 4 ---- 4 files changed, 14 insertions(+), 11 deletions(-) (limited to 'lib') diff --git a/lib/envars.ml b/lib/envars.ml index dbd381bb2a..12cc9edfe4 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -107,12 +107,20 @@ let guess_coqlib fail = (** coqlib is now computed once during coqtop initialization *) +(* Options for changing coqlib *) +let coqlib_spec = ref false +let coqlib = ref "(not initialized yet)" + +let set_user_coqlib path = + coqlib_spec := true; + coqlib := path + let set_coqlib ~fail = - if not !Flags.coqlib_spec then + if not !coqlib_spec then let lib = if !Flags.boot then coqroot else guess_coqlib fail in - Flags.coqlib := lib + coqlib := lib -let coqlib () = !Flags.coqlib +let coqlib () = !coqlib let docdir () = (* This assumes implicitly that the suffix is non-trivial *) diff --git a/lib/envars.mli b/lib/envars.mli index 93d3cf9d0c..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 diff --git a/lib/flags.ml b/lib/flags.ml index 54f25e209d..4d6c36f55d 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -121,10 +121,6 @@ let warn = ref true let make_warn flag = warn := flag; () let if_warn f x = if !warn then f x -(* 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 0faad1a541..398f22ab4f 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -118,10 +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 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 -- cgit v1.2.3 From 24086d1000db370fcf74077841506f02849d0c44 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 27 Sep 2018 02:41:18 +0200 Subject: [envars] Small implementation cleanup for coqlib internals. --- lib/envars.ml | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) (limited to 'lib') diff --git a/lib/envars.ml b/lib/envars.ml index 12cc9edfe4..cf76b6ebc8 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -105,22 +105,19 @@ let guess_coqlib fail = fail "cannot guess a path for Coq libraries; please use -coqlib option") ) -(** coqlib is now computed once during coqtop initialization *) - -(* Options for changing coqlib *) -let coqlib_spec = ref false -let coqlib = ref "(not initialized yet)" +let coqlib : string option ref = ref None +let set_user_coqlib path = coqlib := Some path -let set_user_coqlib path = - coqlib_spec := true; - coqlib := path +(** coqlib is now computed once during coqtop initialization *) let set_coqlib ~fail = - if not !coqlib_spec then + match !coqlib with + | Some _ -> () + | None -> let lib = if !Flags.boot then coqroot else guess_coqlib fail in - coqlib := lib + coqlib := Some lib -let coqlib () = !coqlib +let coqlib () = Option.default "" !coqlib let docdir () = (* This assumes implicitly that the suffix is non-trivial *) -- cgit v1.2.3