1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(** Some excerpt of Util and similar files to avoid loading the whole
module and its dependencies (and hence Compat and Camlp4) *)
module Stringmap = Map.Make(String)
let list_fold_left_i f =
let rec it_list_f i a = function
| [] -> a
| b::l -> it_list_f (i+1) (f i a b) l
in
it_list_f
(* [list_chop i l] splits [l] into two lists [(l1,l2)] such that
[l1++l2=l] and [l1] has length [i].
It raises [Failure] when [i] is negative or greater than the length of [l] *)
let list_chop n l =
let rec chop_aux i acc = function
| tl when i=0 -> (List.rev acc, tl)
| h::t -> chop_aux (pred i) (h::acc) t
| [] -> failwith "list_chop"
in
chop_aux n [] l
let list_map_i f =
let rec map_i_rec i = function
| [] -> []
| x::l -> let v = f i x in v :: map_i_rec (i+1) l
in
map_i_rec
let list_index x =
let rec index_x n = function
| y::l -> if x = y then n else index_x (succ n) l
| [] -> raise Not_found
in
index_x 1
let list_index0 x l = list_index x l - 1
let list_filter_i p =
let rec filter_i_rec i = function
| [] -> []
| x::l -> let l' = filter_i_rec (succ i) l in if p i x then x::l' else l'
in
filter_i_rec 0
let string_map f s =
let l = String.length s in
let r = String.create l in
for i= 0 to (l - 1) do r.[i] <- f (s.[i]) done;
r
let subst_command_placeholder s t =
Str.global_replace (Str.regexp_string "%s") t s
(* Split the content of a variable such as $PATH in a list of directories.
The separators are either ":" in unix or ";" in win32 *)
let path_to_list = Str.split (Str.regexp "[:;]")
(* On win32, the home directory is probably not in $HOME, but in
some other environment variable *)
let home =
try Sys.getenv "HOME" with Not_found ->
try (Sys.getenv "HOMEDRIVE")^(Sys.getenv "HOMEPATH") with Not_found ->
try Sys.getenv "USERPROFILE" with Not_found -> Filename.current_dir_name
let opt2list = function None -> [] | Some x -> [x]
let (/) = Filename.concat
let coqify d = d / "coq"
let xdg_config_home =
coqify (try Sys.getenv "XDG_CONFIG_HOME" with Not_found -> home / ".config")
let relative_base =
Filename.dirname (Filename.dirname Sys.executable_name)
let xdg_config_dirs =
let sys_dirs =
try List.map coqify (path_to_list (Sys.getenv "XDG_CONFIG_DIRS"))
with
| Not_found when Sys.os_type = "Win32" -> [relative_base / "config"]
| Not_found -> ["/etc/xdg/coq"]
in
xdg_config_home :: sys_dirs @ opt2list Coq_config.configdir
let xdg_data_home =
coqify
(try Sys.getenv "XDG_DATA_HOME" with Not_found -> home / ".local" / "share")
let xdg_data_dirs =
let sys_dirs =
try List.map coqify (path_to_list (Sys.getenv "XDG_DATA_DIRS"))
with
| Not_found when Sys.os_type = "Win32" -> [relative_base / "share"]
| Not_found -> ["/usr/local/share/coq";"/usr/share/coq"]
in
xdg_data_home :: sys_dirs @ opt2list Coq_config.datadir
let coqtop_path = ref ""
(* On a Win32 application with no console, writing to stderr raise
a Sys_error "bad file descriptor", hence the "try" below.
Ideally, we should re-route message to a log file somewhere, or
print in the response buffer.
*)
let safe_prerr_endline s =
try prerr_endline s;flush stderr with _ -> ()
(* Hints to partially detects if two paths refer to the same repertory *)
let rec remove_path_dot p =
let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *)
let n = String.length curdir in
let l = String.length p in
if l > n && String.sub p 0 n = curdir then
let n' =
let sl = String.length Filename.dir_sep in
let i = ref n in
while !i <= l - sl && String.sub p !i sl = Filename.dir_sep do i := !i + sl done; !i in
remove_path_dot (String.sub p n' (l - n'))
else
p
let strip_path p =
let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *)
let n = String.length cwd in
let l = String.length p in
if l > n && String.sub p 0 n = cwd then
let n' =
let sl = String.length Filename.dir_sep in
let i = ref n in
while !i <= l - sl && String.sub p !i sl = Filename.dir_sep do i := !i + sl done; !i in
remove_path_dot (String.sub p n' (l - n'))
else
remove_path_dot p
let canonical_path_name p =
let current = Sys.getcwd () in
try
Sys.chdir p;
let p' = Sys.getcwd () in
Sys.chdir current;
p'
with Sys_error _ ->
(* We give up to find a canonical name and just simplify it... *)
strip_path p
let correct_path f dir = if Filename.is_relative f then Filename.concat dir f else f
(*
checks if two file names refer to the same (existing) file by
comparing their device and inode.
It seems that under Windows, inode is always 0, so we cannot
accurately check if
*)
(* Optimised for partial application (in case many candidates must be
compared to f1). *)
let same_file f1 =
try
let s1 = Unix.stat f1 in
(fun f2 ->
try
let s2 = Unix.stat f2 in
s1.Unix.st_dev = s2.Unix.st_dev &&
if Sys.os_type = "Win32" then f1 = f2
else s1.Unix.st_ino = s2.Unix.st_ino
with
Unix.Unix_error _ -> false)
with
Unix.Unix_error _ -> (fun _ -> false)
|
