Source file ProofSession.ml
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
open Wpo
type script =
| NoScript
| Script of string
| Deprecated of string
let files : (string,script) Hashtbl.t = Hashtbl.create 32
let jsonfile (dir:Datatype.Filepath.t) =
Format.sprintf "%s/%s.json" (dir :> string)
let get_script_dir ~force =
Wp_parameters.get_session_dir ~force "script"
let filename ~force wpo =
let dscript = get_script_dir ~force in
jsonfile dscript wpo.po_sid
let legacies wpo =
let mid = WpContext.MODEL.id wpo.po_model in
let dscript = Wp_parameters.get_session_dir ~force:false "script" in
let dmodel = Wp_parameters.get_session_dir ~force:false mid in
[
jsonfile dscript wpo.po_gid ;
jsonfile dmodel wpo.po_gid ;
]
let get wpo =
let f = filename ~force:false wpo in
try Hashtbl.find files f
with Not_found ->
let script =
if Sys.file_exists f then Script f else
try
let f' = List.find Sys.file_exists (legacies wpo) in
Wp_parameters.warning ~current:false
"Deprecated script for '%s'" wpo.po_sid ;
Deprecated f'
with Not_found -> NoScript
in Hashtbl.add files f script ; script
let pp_file fmt s = Filepath.Normalized.(pretty fmt (of_string s))
let pp_script_for fmt wpo =
match get wpo with
| Script f -> Format.fprintf fmt "script '%a'" pp_file f
| Deprecated f -> Format.fprintf fmt "(deprecated) script '%a'" pp_file f
| _ -> Format.fprintf fmt "script '%a'" pp_file @@ filename ~force:false wpo
let exists wpo =
match get wpo with NoScript -> false | Script _ | Deprecated _ -> true
let load wpo =
match get wpo with
| NoScript -> `Null
| Script f | Deprecated f ->
if Sys.file_exists f then Json.load_file f else `Null
let remove wpo =
match get wpo with
| NoScript -> ()
| Script f ->
begin
Extlib.safe_remove f ;
Hashtbl.replace files f NoScript ;
end
| Deprecated f0 ->
begin
Wp_parameters.feedback
"Removed deprecated script for '%s'" wpo.po_sid ;
Extlib.safe_remove f0 ;
let f = filename ~force:false wpo in
Hashtbl.replace files f NoScript ;
end
let save ~stdout wpo js =
let empty =
match js with
| `Null | `List [] | `Assoc [] -> true
| _ -> false in
if stdout then
Wp_parameters.result "Proof script for %s:@.%a"
wpo.po_gid (Json.save_formatter ~pretty:true) js
else
if empty then remove wpo else
match get wpo with
| Script f ->
Json.save_file f js
| NoScript ->
begin
let f = filename ~force:true wpo in
Json.save_file f js ;
Hashtbl.replace files f (Script f) ;
end
| Deprecated f0 ->
begin
Wp_parameters.feedback
"Upgraded script for '%s'" wpo.po_sid ;
Extlib.safe_remove f0 ;
let f = filename ~force:true wpo in
Json.save_file f js ;
Hashtbl.replace files f (Script f) ;
end
let get_marks_dir ~force =
let scripts = Wp_parameters.get_session_dir ~force "script" in
let path = Datatype.Filepath.concat scripts ".marks" in
if force then Wp_parameters.make_output_dir (path :> string) ;
path
let remove_marks ~dry =
let marks = get_marks_dir ~force:false in
let as_str = (marks :> string) in
if Sys.file_exists as_str && Sys.is_directory as_str then
if dry
then Wp_parameters.feedback "[dry] remove marks"
else Extlib.safe_remove_dir as_str
let reset_marks () =
remove_marks ~dry:false ;
ignore @@ get_marks_dir ~force:true
let mark goal =
let marks = get_marks_dir ~force:false in
let as_str = (marks :> string) in
if Sys.file_exists as_str && Sys.is_directory as_str then
let mark = Datatype.Filepath.concat marks (goal.po_sid ^ ".json") in
if Sys.file_exists (mark :> string) then ()
else close_out @@ open_out (mark :> string)
module StringSet = Datatype.String.Set
let remove_unmarked_files ~dry =
let dir = (get_script_dir ~force:false :> string) in
if Sys.file_exists dir && Sys.is_directory dir then
let marks = (get_marks_dir ~force:false :> string) in
if Sys.file_exists marks && Sys.is_directory marks then
begin
let files =
Array.fold_left
(fun s f -> StringSet.add f s) StringSet.empty (Sys.readdir dir)
in
let marks =
Array.fold_left
(fun s f -> StringSet.add f s) StringSet.empty (Sys.readdir marks)
in
let orphans = StringSet.diff files marks in
let orphans = StringSet.remove ".marks" orphans in
let remove file =
let path = dir ^ "/" ^ file in
if dry
then Wp_parameters.feedback "[dry] rm %s" path
else Sys.remove path
in
StringSet.iter remove orphans ;
remove_marks ~dry
end