diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/envars.ml | 51 | ||||
| -rw-r--r-- | lib/envars.mli | 9 | ||||
| -rw-r--r-- | lib/feedback.ml | 2 | ||||
| -rw-r--r-- | lib/feedback.mli | 5 | ||||
| -rw-r--r-- | lib/flags.ml | 31 | ||||
| -rw-r--r-- | lib/flags.mli | 13 | ||||
| -rw-r--r-- | lib/pp.ml | 3 | ||||
| -rw-r--r-- | lib/pp.mli | 3 | ||||
| -rw-r--r-- | lib/system.ml | 4 | ||||
| -rw-r--r-- | lib/system.mli | 2 |
10 files changed, 23 insertions, 100 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/feedback.ml b/lib/feedback.ml index cb8f8aad1e..9654711ebb 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -84,7 +84,7 @@ let feedback_logger ?loc lvl msg = let msg_info ?loc x = feedback_logger ?loc Info x let msg_notice ?loc x = feedback_logger ?loc Notice x let msg_warning ?loc x = feedback_logger ?loc Warning x -let msg_error ?loc x = feedback_logger ?loc Error x +(* let msg_error ?loc x = feedback_logger ?loc Error x *) let msg_debug ?loc x = feedback_logger ?loc Debug x (* Helper for tools willing to understand only the messages *) diff --git a/lib/feedback.mli b/lib/feedback.mli index 64fdf3724d..f407e2fd5b 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -95,11 +95,6 @@ val msg_warning : ?loc:Loc.t -> Pp.t -> unit (** Message indicating that something went wrong, but without serious consequences. *) -val msg_error : ?loc:Loc.t -> Pp.t -> unit -[@@ocaml.deprecated "msg_error is an internal function and should not be \ - used unless you know what you are doing. Use \ - [CErrors.user_err] instead."] - val msg_debug : ?loc:Loc.t -> Pp.t -> unit (** For debugging purposes *) 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 @@ -42,9 +42,6 @@ type doc_view = internal representation opaque here. *) type t = doc_view -type std_ppcmds = t -[@@ocaml.deprecated "alias of Pp.t"] - let repr x = x let unrepr x = x diff --git a/lib/pp.mli b/lib/pp.mli index ed31daa561..4ce6a535c8 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -42,9 +42,6 @@ type pp_tag = string internal representation opaque here. *) type t -type std_ppcmds = t -[@@ocaml.deprecated "alias of Pp.t"] - type block_type = | Pp_hbox of int | Pp_vbox of int diff --git a/lib/system.ml b/lib/system.ml index 902a4f2506..eec007dcab 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -302,10 +302,10 @@ let with_time ~batch f x = raise e (* We use argv.[0] as we don't want to resolve symlinks *) -let get_toplevel_path top = +let get_toplevel_path ?(byte=not Dynlink.is_native) top = let open Filename in let dir = if String.equal (basename Sys.argv.(0)) Sys.argv.(0) then "" else dirname Sys.argv.(0) ^ dir_sep in let exe = if Sys.(os_type = "Win32" || os_type = "Cygwin") then ".exe" else "" in - let eff = if Dynlink.is_native then ".opt" else ".byte" in + let eff = if byte then ".byte" else ".opt" in dir ^ top ^ eff ^ exe diff --git a/lib/system.mli b/lib/system.mli index a34280037c..f13fd30923 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -122,4 +122,4 @@ val with_time : batch:bool -> ('a -> 'b) -> 'a -> 'b the right name you want you execution to fail rather than fall into choosing some random binary from the system-wide installation of Coq. *) -val get_toplevel_path : string -> string +val get_toplevel_path : ?byte:bool -> string -> string |