aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/cEphemeron.ml4
-rw-r--r--lib/cEphemeron.mli2
-rw-r--r--lib/cErrors.ml8
-rw-r--r--lib/cErrors.mli14
-rw-r--r--lib/cString.ml4
-rw-r--r--lib/cString.mli3
-rw-r--r--lib/cWarnings.ml2
-rw-r--r--lib/coqProject_file.ml410
-rw-r--r--lib/coqProject_file.mli1
-rw-r--r--lib/envars.ml65
-rw-r--r--lib/envars.mli18
-rw-r--r--lib/flags.ml1
-rw-r--r--lib/flags.mli4
-rw-r--r--lib/future.ml6
-rw-r--r--lib/genarg.ml6
-rw-r--r--lib/hashcons.ml4
-rw-r--r--lib/remoteCounter.ml4
-rw-r--r--lib/spawn.ml4
18 files changed, 89 insertions, 71 deletions
diff --git a/lib/cEphemeron.ml b/lib/cEphemeron.ml
index a38ea11e10..890e02dc4e 100644
--- a/lib/cEphemeron.ml
+++ b/lib/cEphemeron.ml
@@ -35,10 +35,10 @@ end)
would make the key always reachable) *)
let values : Obj.t HT.t = HT.create 1001
-(* To avoid a race contidion between the finalization function and
+(* To avoid a race condition between the finalization function and
get/create on the values hashtable, the finalization function just
enqueues in an imperative list the item to be collected. Being the list
- imperative, even if the Gc enqueue an item while run_collection is operating,
+ imperative, even if the Gc enqueues an item while run_collection is operating,
the tail of the list is eventually set to Empty on completion.
Kudos to the authors of Why3 that came up with this solution for their
implementation of weak hash tables! *)
diff --git a/lib/cEphemeron.mli b/lib/cEphemeron.mli
index 1200e4e208..76cd7a5a8a 100644
--- a/lib/cEphemeron.mli
+++ b/lib/cEphemeron.mli
@@ -26,7 +26,7 @@
Proposed solution:
Turn all occurrences of [bad] into [bad key] in your data structure.
- Use [crate bad_val] to obtain a unique key [k] for [bad_val], and store
+ Use [create bad_val] to obtain a unique key [k] for [bad_val], and store
[k] in the data structure. Use [get k] to obtain [bad_val].
An ['a key] can always be marshalled. When marshalled, a key loses its
diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index b55fd80c68..8ef11a2cdd 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -38,7 +38,6 @@ exception UserError of string option * std_ppcmds (* User errors *)
let todo s = prerr_string ("TODO: "^s^"\n")
let user_err ?loc ?hdr strm = Loc.raise ?loc (UserError (hdr, strm))
-let error string = user_err (str string)
let invalid_arg ?loc s = Loc.raise ?loc (Invalid_argument s)
@@ -78,7 +77,7 @@ let where = function
if !Flags.debug then str "in " ++ str s ++ str ":" ++ spc () else mt ()
let raw_anomaly e = match e with
- | Anomaly (s, pps) -> where s ++ pps ++ str "."
+ | Anomaly (s, pps) -> where s ++ pps
| Assert_failure _ | Match_failure _ -> str (Printexc.to_string e) ++ str "."
| _ -> str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "."
@@ -138,3 +137,8 @@ let handled e =
let bottom _ = raise Bottom in
try let _ = print_gen bottom !handle_stack e in true
with Bottom -> false
+
+(* Deprecated functions *)
+let error string = user_err (str string)
+let user_err_loc (loc,hdr,msg) = user_err ~loc ~hdr msg
+let errorlabstrm hdr msg = user_err ~hdr msg
diff --git a/lib/cErrors.mli b/lib/cErrors.mli
index 0665a8ce73..ca0838575e 100644
--- a/lib/cErrors.mli
+++ b/lib/cErrors.mli
@@ -41,9 +41,6 @@ val user_err : ?loc:Loc.t -> ?hdr:string -> std_ppcmds -> 'a
(** Main error raising primitive. [user_err ?loc ?hdr pp] signals an
error [pp] with optional header and location [hdr] [loc] *)
-val error : string -> 'a
-(** [error s] just calls [user_error "_" (str s)] *)
-
exception AlreadyDeclared of std_ppcmds
val alreadydeclared : std_ppcmds -> 'a
@@ -98,3 +95,14 @@ val noncritical : exn -> bool
(** Check whether an exception is handled by some toplevel printer. The
[Anomaly] exception is never handled. *)
val handled : exn -> bool
+
+(** Deprecated functions *)
+val error : string -> 'a
+ [@@ocaml.deprecated "use [user_err] instead"]
+
+val errorlabstrm : string -> std_ppcmds -> 'a
+ [@@ocaml.deprecated "use [user_err ~hdr] instead"]
+
+val user_err_loc : Loc.t * string * std_ppcmds -> 'a
+ [@@ocaml.deprecated "use [user_err ~loc] instead"]
+
diff --git a/lib/cString.ml b/lib/cString.ml
index 61ed03083e..7048dbb81b 100644
--- a/lib/cString.ml
+++ b/lib/cString.ml
@@ -11,7 +11,9 @@ module type S = module type of String
module type ExtS =
sig
include S
+ [@@@ocaml.warning "-3"] (* [@@noalloc] since 4.03.0 GPR#240 *)
external equal : string -> string -> bool = "caml_string_equal" "noalloc"
+ [@@@ocaml.warning "+3"]
val hash : string -> int
val is_empty : string -> bool
val explode : string -> string list
@@ -33,7 +35,9 @@ end
include String
+[@@@ocaml.warning "-3"] (* [@@noalloc] since 4.03.0 GPR#240 *)
external equal : string -> string -> bool = "caml_string_equal" "noalloc"
+[@@@ocaml.warning "+3"]
let rec hash len s i accu =
if i = len then accu
diff --git a/lib/cString.mli b/lib/cString.mli
index 65edfbbe68..b30f26abe7 100644
--- a/lib/cString.mli
+++ b/lib/cString.mli
@@ -14,7 +14,10 @@ sig
include S
(** We include the standard library *)
+ [@@@ocaml.warning "-3"] (* [@@noalloc] since 4.03.0 GPR#240 *)
external equal : string -> string -> bool = "caml_string_equal" "noalloc"
+ [@@@ocaml.warning "+3"]
+
(** Equality on strings *)
val hash : string -> int
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index 2755946abc..d004fd6711 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -86,7 +86,7 @@ let parse_flag s =
| '+' -> (AsError, String.sub s 1 (String.length s - 1))
| '-' -> (Disabled, String.sub s 1 (String.length s - 1))
| _ -> (Enabled, s)
- else CErrors.error "Invalid warnings flag"
+ else CErrors.user_err Pp.(str "Invalid warnings flag")
let string_of_flag (status,name) =
match status with
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
index 7a16605695..97aa90e07d 100644
--- a/lib/coqProject_file.ml4
+++ b/lib/coqProject_file.ml4
@@ -11,6 +11,7 @@ type project = {
makefile : string option;
install_kind : install option;
use_ocamlopt : bool;
+ bypass_API : bool;
v_files : string list;
mli_files : string list;
@@ -42,11 +43,12 @@ and install =
| UserInstall
(* TODO generate with PPX *)
-let mk_project project_file makefile install_kind use_ocamlopt = {
+let mk_project project_file makefile install_kind use_ocamlopt bypass_API = {
project_file;
makefile;
install_kind;
use_ocamlopt;
+ bypass_API;
v_files = [];
mli_files = [];
@@ -166,6 +168,8 @@ let process_cmd_line orig_dir proj args =
aux { proj with defs = proj.defs @ [v,def] } r
| "-arg" :: a :: r ->
aux { proj with extra_args = proj.extra_args @ [a] } r
+ | "-bypass-API" :: r ->
+ aux { proj with bypass_API = true } r
| f :: r ->
let f = CUnix.correct_path f orig_dir in
let proj =
@@ -185,11 +189,11 @@ let process_cmd_line orig_dir proj args =
(******************************* API ************************************)
let cmdline_args_to_project ~curdir args =
- process_cmd_line curdir (mk_project None None None true) args
+ process_cmd_line curdir (mk_project None None None true false) args
let read_project_file f =
process_cmd_line (Filename.dirname f)
- (mk_project (Some f) None (Some NoInstall) true) (parse f)
+ (mk_project (Some f) None (Some NoInstall) true false) (parse f)
let rec find_project_file ~from ~projfile_name =
let fname = Filename.concat from projfile_name in
diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli
index 8c8fc068a3..19fc9227ae 100644
--- a/lib/coqProject_file.mli
+++ b/lib/coqProject_file.mli
@@ -13,6 +13,7 @@ type project = {
makefile : string option;
install_kind : install option;
use_ocamlopt : bool;
+ bypass_API : bool;
v_files : string list;
mli_files : string list;
diff --git a/lib/envars.ml b/lib/envars.ml
index 79516bb1bf..47baf66a69 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -23,8 +23,6 @@ let ( / ) a b =
let coqify d = d / "coq"
-let opt2list = function None -> [] | Some x -> [x]
-
let home ~warn =
getenv_else "HOME" (fun () ->
try (Sys.getenv "HOMEDRIVE")^(Sys.getenv "HOMEPATH") with Not_found ->
@@ -81,9 +79,6 @@ let expand_path_macros ~warn s =
(** {2 Coq paths} *)
-let relative_base =
- Filename.dirname (Filename.dirname Sys.executable_name)
-
let coqbin =
CUnix.canonical_path_name (Filename.dirname Sys.executable_name)
@@ -98,25 +93,26 @@ let _ =
if Coq_config.arch_is_win32 then
Unix.putenv "PATH" (coqbin ^ ";" ^ getenv_else "PATH" (fun () -> ""))
+(** Add a local installation suffix (unless the suffix is itself
+ absolute in which case the prefix does not matter) *)
+let use_suffix prefix suffix =
+ if String.length suffix > 0 && suffix.[0] = '/' then suffix else prefix / suffix
+
(** [check_file_else ~dir ~file oth] checks if [file] exists in
- the installation directory [dir] given relatively to [coqroot].
- If this Coq is only locally built, then [file] must be in [coqroot].
+ the installation directory [dir] given relatively to [coqroot],
+ which maybe has been relocated.
If the check fails, then [oth ()] is evaluated.
Using file system equality seems well enough for this heuristic *)
let check_file_else ~dir ~file oth =
- let path = if Coq_config.local then coqroot else coqroot / dir in
+ let path = use_suffix coqroot dir in
if Sys.file_exists (path / file) then path else oth ()
let guess_coqlib fail =
let prelude = "theories/Init/Prelude.vo" in
- let dir = if Coq_config.arch_is_win32 then "lib" else "lib/coq" in
- check_file_else ~dir ~file:prelude
+ check_file_else ~dir:Coq_config.coqlibsuffix ~file:prelude
(fun () ->
- let coqlib = match Coq_config.coqlib with
- | Some coqlib -> coqlib
- | None -> coqroot
- in
- if Sys.file_exists (coqlib / prelude) then coqlib
+ if not Coq_config.local && Sys.file_exists (Coq_config.coqlib / prelude)
+ then Coq_config.coqlib
else
fail "cannot guess a path for Coq libraries; please use -coqlib option")
@@ -130,8 +126,19 @@ let set_coqlib ~fail =
let coqlib () = !Flags.coqlib
let docdir () =
- let dir = if Coq_config.arch_is_win32 then "doc" else "share/doc/coq" in
- check_file_else ~dir ~file:"html" (fun () -> Coq_config.docdir)
+ (* This assumes implicitly that the suffix is non-trivial *)
+ let path = use_suffix coqroot Coq_config.docdirsuffix in
+ if Sys.file_exists path then path else Coq_config.docdir
+
+let datadir () =
+ (* This assumes implicitly that the suffix is non-trivial *)
+ let path = use_suffix coqroot Coq_config.datadirsuffix in
+ if Sys.file_exists path then path else Coq_config.datadir
+
+let configdir () =
+ (* This assumes implicitly that the suffix is non-trivial *)
+ let path = use_suffix coqroot Coq_config.configdirsuffix in
+ if Sys.file_exists path then path else Coq_config.configdir
let coqpath =
let coqpath = getenv_else "COQPATH" (fun () -> "") in
@@ -186,34 +193,16 @@ let xdg_data_dirs warn =
try
List.map coqify (path_to_list (Sys.getenv "XDG_DATA_DIRS"))
with
- | Not_found when String.equal Sys.os_type "Win32" -> [relative_base / "share"]
- | Not_found -> ["/usr/local/share/coq";"/usr/share/coq"]
- in
- xdg_data_home warn :: sys_dirs @ opt2list Coq_config.datadir
-
-let xdg_config_dirs warn =
- let sys_dirs =
- try
- List.map coqify (path_to_list (Sys.getenv "XDG_CONFIG_DIRS"))
- with
- | Not_found when String.equal Sys.os_type "Win32" -> [relative_base / "config"]
- | Not_found -> ["/etc/xdg/coq"]
+ | Not_found -> [datadir ()]
in
- xdg_config_home warn :: sys_dirs @ opt2list Coq_config.configdir
+ xdg_data_home warn :: sys_dirs
let xdg_dirs ~warn =
List.filter Sys.file_exists (xdg_data_dirs warn)
(* Print the configuration information *)
-let coq_src_subdirs = [
- "config" ; "dev" ; "lib" ; "kernel" ; "library" ;
- "engine" ; "pretyping" ; "interp" ; "parsing" ; "proofs" ;
- "tactics" ; "toplevel" ; "printing" ; "intf" ;
- "grammar" ; "ide" ; "stm"; "vernac" ] @
- Coq_config.plugins_dirs
-
-let print_config ?(prefix_var_name="") f =
+let print_config ?(prefix_var_name="") f coq_src_subdirs =
let open Printf in
fprintf f "%sLOCAL=%s\n" prefix_var_name (if Coq_config.local then "1" else "0");
fprintf f "%sCOQLIB=%s/\n" prefix_var_name (coqlib ());
diff --git a/lib/envars.mli b/lib/envars.mli
index b164e789d2..edd13447fc 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -27,12 +27,18 @@ val home : warn:(string -> unit) -> string
(** [coqlib] is the path to the Coq library. *)
val coqlib : unit -> string
+(** [docdir] is the path to the installed documentation. *)
+val docdir : unit -> string
+
+(** [datadir] is the path to the installed data directory. *)
+val datadir : unit -> string
+
+(** [configdir] is the path to the installed config directory. *)
+val configdir : unit -> string
+
(** [set_coqlib] must be runned once before any access to [coqlib] *)
val set_coqlib : fail:(string -> string) -> unit
-(** [docdir] is the path to the Coq documentation. *)
-val docdir : unit -> string
-
(** [coqbin] is the name of the current executable. *)
val coqbin : string
@@ -66,12 +72,8 @@ val camlp4 : unit -> string
*)
val xdg_config_home : (string -> unit) -> string
val xdg_data_home : (string -> unit) -> string
-val xdg_config_dirs : (string -> unit) -> string list
val xdg_data_dirs : (string -> unit) -> string list
val xdg_dirs : warn : (string -> unit) -> string list
(** {6 Prints the configuration information } *)
-val print_config : ?prefix_var_name:string -> out_channel -> unit
-
-(** Directories in which coq sources are found *)
-val coq_src_subdirs : string list
+val print_config : ?prefix_var_name:string -> out_channel -> string list -> unit
diff --git a/lib/flags.ml b/lib/flags.ml
index b2671e5b60..6a3b7a4261 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -87,7 +87,6 @@ let in_toplevel = ref false
let profile = false
-let print_emacs = ref false
let xml_export = ref false
let ide_slave = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 7ce808041a..e2cf09474e 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -13,7 +13,9 @@
val boot : bool ref
val load_init : bool ref
+(* Will affect STM caching *)
val batch_mode : bool ref
+
type compilation_mode = BuildVo | BuildVio | Vio2Vo
val compilation_mode : compilation_mode ref
val compilation_output_name : string option ref
@@ -56,8 +58,6 @@ val profile : bool
(* Legacy flags *)
-(* -emacs option: printing includes emacs tags, will affect stm caching. *)
-val print_emacs : bool ref
(* -xml option: xml hooks will be called *)
val xml_export : bool ref
diff --git a/lib/future.ml b/lib/future.ml
index 1360b7ac4a..8bef1e58e1 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -157,7 +157,7 @@ let chain ~pure ck f =
| Val (v, None) ->
match !ck with
| Finished _ -> CErrors.anomaly(Pp.str
- "Future.chain ~pure:false call on an already joined computation")
+ "Future.chain ~pure:false call on an already joined computation.")
| Ongoing _ -> CErrors.anomaly(Pp.strbrk(
"Future.chain ~pure:false call on a pure computation. "^
"This can happen if the computation was initial created with "^
@@ -171,7 +171,7 @@ let replace kx y =
match !x with
| Exn _ -> x := Closure (fun () -> force ~pure:false y)
| _ -> CErrors.anomaly
- (Pp.str "A computation can be replaced only if is_exn holds")
+ (Pp.str "A computation can be replaced only if is_exn holds.")
let purify f x =
let state = !freeze () in
@@ -213,7 +213,7 @@ let map2 f x l =
let xi = chain ~pure:true x (fun x ->
try List.nth x i
with Failure _ | Invalid_argument _ ->
- CErrors.anomaly (Pp.str "Future.map2 length mismatch")) in
+ CErrors.anomaly (Pp.str "Future.map2 length mismatch.")) in
f xi y) 0 l
let print f kx =
diff --git a/lib/genarg.ml b/lib/genarg.ml
index 05c828d5f9..377ff81827 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -159,7 +159,7 @@ let create_arg name =
match ArgT.name name with
| None -> ExtraArg (ArgT.create name)
| Some _ ->
- CErrors.anomaly (str "generic argument already declared: " ++ str name)
+ CErrors.anomaly (str "generic argument already declared: " ++ str name ++ str ".")
let make0 = create_arg
@@ -180,7 +180,7 @@ struct
let register0 arg f = match arg with
| ExtraArg s ->
if GenMap.mem s !arg0_map then
- let msg = str M.name ++ str " function already registered: " ++ str (ArgT.repr s) in
+ let msg = str M.name ++ str " function already registered: " ++ str (ArgT.repr s) ++ str "." in
CErrors.anomaly msg
else
arg0_map := GenMap.add s (GenMap.Pack f) !arg0_map
@@ -192,7 +192,7 @@ struct
with Not_found ->
match M.default (ExtraArg name) with
| None ->
- CErrors.anomaly (str M.name ++ str " function not found: " ++ str (ArgT.repr name))
+ CErrors.anomaly (str M.name ++ str " function not found: " ++ str (ArgT.repr name) ++ str ".")
| Some obj -> obj
(** For now, the following function is quite dummy and should only be applied
diff --git a/lib/hashcons.ml b/lib/hashcons.ml
index 4eaacf9145..0ee3ec6277 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -130,7 +130,11 @@ module Hstring = Make(
type t = string
type u = unit
let hashcons () s =(* incr accesstr;*) s
+
+ [@@@ocaml.warning "-3"] (* [@@noalloc] since 4.03.0 GPR#240 *)
external eq : string -> string -> bool = "caml_string_equal" "noalloc"
+ [@@@ocaml.warning "+3"]
+
(** Copy from CString *)
let rec hash len s i accu =
if i = len then accu
diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml
index e7646fb796..11f151a609 100644
--- a/lib/remoteCounter.ml
+++ b/lib/remoteCounter.ml
@@ -25,7 +25,7 @@ let new_counter ~name a ~incr ~build =
(* - in the main process there is a race condition between slave
managers (that are threads) and the main thread, hence the mutex *)
if Flags.async_proofs_is_worker () then
- CErrors.anomaly(Pp.str"Slave processes must install remote counters");
+ CErrors.anomaly(Pp.str"Slave processes must install remote counters.");
Mutex.lock m; let x = f () in Mutex.unlock m;
build x in
let mk_thsafe_remote_getter f () =
@@ -33,7 +33,7 @@ let new_counter ~name a ~incr ~build =
let getter = ref(mk_thsafe_local_getter (fun () -> !data := incr !!data; !!data)) in
let installer f =
if not (Flags.async_proofs_is_worker ()) then
- CErrors.anomaly(Pp.str"Only slave processes can install a remote counter");
+ CErrors.anomaly(Pp.str"Only slave processes can install a remote counter.");
getter := mk_thsafe_remote_getter f in
(fun () -> !getter ()), installer
diff --git a/lib/spawn.ml b/lib/spawn.ml
index 4791769735..4d7e78d861 100644
--- a/lib/spawn.ml
+++ b/lib/spawn.ml
@@ -200,7 +200,7 @@ let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ())
p, cout
let stats { oob_req; oob_resp; alive } =
- assert_ alive "This process is dead";
+ assert_ alive "This process is dead.";
output_value oob_req ReqStats;
flush oob_req;
input_value oob_resp
@@ -251,7 +251,7 @@ let kill ({ pid = unixpid; oob_req; oob_resp; cin; cout; alive } as p) =
with e -> prerr_endline ("kill: "^Printexc.to_string e) end
let stats { oob_req; oob_resp; alive } =
- assert_ alive "This process is dead";
+ assert_ alive "This process is dead.";
output_value oob_req ReqStats;
flush oob_req;
let RespStats g = input_value oob_resp in g
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 07:34:21 +0000