diff options
Diffstat (limited to 'lib')
-rw-r--r-- | lib/envars.ml | 19 | ||||
-rw-r--r-- | lib/errors.ml | 9 | ||||
-rw-r--r-- | lib/errors.mli | 4 | ||||
-rw-r--r-- | lib/flags.ml | 2 | ||||
-rw-r--r-- | lib/flags.mli | 2 | ||||
-rw-r--r-- | lib/pp_control.ml | 11 | ||||
-rw-r--r-- | lib/system.ml | 16 | ||||
-rw-r--r-- | lib/system.mli | 2 |
8 files changed, 57 insertions, 8 deletions
diff --git a/lib/envars.ml b/lib/envars.ml index b0eed8386..ac0b6f722 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -39,12 +39,25 @@ let path_to_list p = let user_path () = path_to_list (Sys.getenv "PATH") (* may raise Not_found *) + (* Duplicated from system.ml to minimize dependencies *) +let file_exists_respecting_case f = + if Coq_config.arch = "Darwin" then + (* ensure that the file exists with expected case on the + case-insensitive but case-preserving default MacOS file system *) + let rec aux f = + let bf = Filename.basename f in + let df = Filename.dirname f in + String.equal df "." || String.equal df "/" || + aux df && Array.exists (String.equal bf) (Sys.readdir df) + in aux f + else Sys.file_exists f + let rec which l f = match l with | [] -> raise Not_found | p :: tl -> - if Sys.file_exists (p / f) then + if file_exists_respecting_case (p / f) then p else which tl f @@ -102,7 +115,7 @@ let _ = If the check fails, then [oth ()] is evaluated. *) let check_file_else ~dir ~file oth = let path = if Coq_config.local then coqroot else coqroot / dir in - if Sys.file_exists (path / file) then path else oth () + if file_exists_respecting_case (path / file) then path else oth () let guess_coqlib fail = let prelude = "theories/Init/Prelude.vo" in @@ -134,7 +147,7 @@ let coqpath = let coqpath = getenv_else "COQPATH" (fun () -> "") in let make_search_path path = let paths = path_to_list path in - let valid_paths = List.filter Sys.file_exists paths in + let valid_paths = List.filter file_exists_respecting_case paths in List.rev valid_paths in make_search_path coqpath diff --git a/lib/errors.ml b/lib/errors.ml index 999d99ee0..c60442654 100644 --- a/lib/errors.ml +++ b/lib/errors.ml @@ -120,3 +120,12 @@ let noncritical = function | Timeout | Drop | Quit -> false | Invalid_argument "equal: functional value" -> false | _ -> true + +(** Check whether an exception is handled *) + +exception Bottom + +let handled e = + let bottom _ = raise Bottom in + try let _ = print_gen bottom !handle_stack e in true + with Bottom -> false diff --git a/lib/errors.mli b/lib/errors.mli index 5bd572474..8320ce409 100644 --- a/lib/errors.mli +++ b/lib/errors.mli @@ -88,3 +88,7 @@ val iprint_no_report : Exninfo.iexn -> Pp.std_ppcmds Typical example: [Sys.Break], [Assert_failure], [Anomaly] ... *) val noncritical : exn -> bool + +(** Check whether an exception is handled by some toplevel printer. The + [Anomaly] exception is never handled. *) +val handled : exn -> bool diff --git a/lib/flags.ml b/lib/flags.ml index 313da0c5b..009caa9de 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -48,6 +48,8 @@ let batch_mode = ref false type compilation_mode = BuildVo | BuildVio | Vio2Vo let compilation_mode = ref BuildVo +let test_mode = ref false + type async_proofs = APoff | APonLazy | APon let async_proofs_mode = ref APoff type cache = Force diff --git a/lib/flags.mli b/lib/flags.mli index 1f68a88f3..544e2a72a 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -15,6 +15,8 @@ val batch_mode : bool ref type compilation_mode = BuildVo | BuildVio | Vio2Vo val compilation_mode : compilation_mode ref +val test_mode : bool ref + type async_proofs = APoff | APonLazy | APon val async_proofs_mode : async_proofs ref type cache = Force diff --git a/lib/pp_control.ml b/lib/pp_control.ml index 0d224c035..969c1550e 100644 --- a/lib/pp_control.ml +++ b/lib/pp_control.ml @@ -20,7 +20,7 @@ let dflt_gp = { margin = 78; max_indent = 50; max_depth = 50; - ellipsis = ".." } + ellipsis = "..." } (* A deeper pretty-printer to print proof scripts *) @@ -84,5 +84,10 @@ let set_margin v = let v = match v with None -> default_margin | Some v -> v in Format.pp_set_margin Format.str_formatter v; Format.pp_set_margin !std_ft v; - Format.pp_set_margin !deep_ft v - + Format.pp_set_margin !deep_ft v; + (* Heuristic, based on usage: the column on the right of max_indent + column is 20% of width, capped to 30 characters *) + let m = max (64 * v / 100) (v-30) in + Format.pp_set_max_indent Format.str_formatter m; + Format.pp_set_max_indent !std_ft m; + Format.pp_set_max_indent !deep_ft m diff --git a/lib/system.ml b/lib/system.ml index e4a60eccb..26bf78010 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -94,6 +94,18 @@ let all_subdirs ~unix_path:root = else msg_warning (str ("Cannot open " ^ root)); List.rev !l +let file_exists_respecting_case f = + if Coq_config.arch = "Darwin" then + (* ensure that the file exists with expected case on the + case-insensitive but case-preserving default MacOS file system *) + let rec aux f = + let bf = Filename.basename f in + let df = Filename.dirname f in + (String.equal df "." || String.equal df "/" || aux df) + && Array.exists (String.equal bf) (Sys.readdir df) + in aux f + else Sys.file_exists f + let rec search paths test = match paths with | [] -> [] @@ -118,7 +130,7 @@ let where_in_path ?(warn=true) path filename = in check_and_warn (search path (fun lpe -> let f = Filename.concat lpe filename in - if Sys.file_exists f then [lpe,f] else [])) + if file_exists_respecting_case f then [lpe,f] else [])) let where_in_path_rex path rex = search path (fun lpe -> @@ -134,7 +146,7 @@ let where_in_path_rex path rex = let find_file_in_path ?(warn=true) paths filename = if not (Filename.is_implicit filename) then - if Sys.file_exists filename then + if file_exists_respecting_case filename then let root = Filename.dirname filename in root, filename else diff --git a/lib/system.mli b/lib/system.mli index 6ed450326..eb29b6970 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -59,6 +59,8 @@ val where_in_path_rex : val find_file_in_path : ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string +val file_exists_respecting_case : string -> bool + (** {6 I/O functions } *) (** Generic input and output functions, parameterized by a magic number and a suffix. The intern functions raise the exception [Bad_magic_number] |