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
|
open Constrexpr
let mk_temp_dir temp_dir =
let tm = Unix.localtime (Unix.time ()) in
let ts = Printf.sprintf "%02d%02d%02d_" tm.Unix.tm_hour tm.Unix.tm_min tm.Unix.tm_sec in
#if OCAML_VERSION >= (5, 1, 0)
Filename.temp_dir ~temp_dir ts ""
#else
(* https://discuss.ocaml.org/t/how-to-create-a-temporary-directory-in-ocaml/1815/4 *)
let rand_digits () =
let rand = Random.State.(bits (make_self_init ()) land 0xFFFFFF) in
Printf.sprintf "%06x" rand in
let (</>) = Filename.concat in
let pat = temp_dir </> ts in
let mode = 0o700 in
let raise_err msg = raise (Sys_error msg) in
let rec loop count =
if count < 0 then raise_err "mk_temp_dir: too many failing attemps" else
let dir = pat ^ rand_digits () in
try (Unix.mkdir dir mode; dir) with
| Unix.Unix_error (Unix.EEXIST, _, _) -> loop (count - 1)
| Unix.Unix_error (Unix.EINTR, _, _) -> loop count
| Unix.Unix_error (e, _, _) ->
raise_err ("mk_temp_dir: " ^ (Unix.error_message e))
in
loop 1000
#endif
let apply_constr f xs =
#if COQ_VERSION < (8, 15, 0)
let f = (None, f) in
#endif
CApp (f, List.map (fun x -> (x, None)) xs)
#if COQ_VERSION >= (8,20,0)
type indirect_accessor = Global.indirect_accessor
type 'a with_accessor = opaque_access:Global.indirect_accessor -> 'a
let apply_accessor f = f
#else
type indirect_accessor = unit
type 'a with_accessor = 'a
let apply_accessor f ~opaque_access:() = f
#endif
|
