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
open VCS
open Task
open Wpo
let dispatch ?(config=VCS.default) mode prover wpo =
begin
match prover with
| Qed | Tactical -> Task.return VCS.no_result
| Why3 prover ->
let smoke = Wpo.is_smoke_test wpo in
let kf = match Wpo.get_scope wpo with
| Global -> None
| Kf kf -> Some kf
in
ProverWhy3.prove
~timeout:(VCS.get_timeout ?kf ~smoke config)
~steplimit:(VCS.get_stepout config)
~memlimit:(VCS.get_memlimit config)
~mode ~prover wpo
end
let started ?start wpo =
match start with
| None -> ()
| Some f -> f wpo
let signal ?progress wpo msg =
match progress with
| None -> ()
| Some f -> f wpo msg
let update ?result wpo prover res =
Wpo.set_result wpo prover res ;
match result with
| None -> ()
| Some f -> f wpo prover res
let run_prover wpo ?config ?(mode=Batch) ?progress ?result prover =
signal ?progress wpo (VCS.name_of_prover prover) ;
dispatch ?config mode prover wpo >>>
fun status ->
let res = match status with
| Task.Result r -> r
| Task.Canceled -> VCS.no_result
| Task.Timeout t -> VCS.timeout t
| Task.Failed exn -> VCS.failed (error exn)
in
let res = { res with solver_time = Wpo.qed_time wpo } in
update ?result wpo prover res ;
Task.return (VCS.is_valid res)
let simplify ?start ?result ?(commit=false) wpo =
Server.Main.async
(fun wpo ->
let r = Wpo.get_result wpo VCS.Qed in
VCS.( r.verdict == Valid ) ||
begin
started ?start wpo ;
let ok = Wpo.reduce wpo in
if commit || ok then
let time = qed_time wpo in
let verdict = if ok then VCS.Valid else VCS.Unknown in
let presult = VCS.result ~time verdict in
(update ?result wpo VCS.Qed presult ; ok)
else false
end)
wpo
let prove wpo ?config ?mode ?start ?progress ?result prover =
simplify ?start ?result wpo >>= fun succeed ->
if succeed
then Task.return true
else (run_prover wpo ?config ?mode ?progress ?result prover)
let spawn wpo ~delayed
?config ?start ?progress ?result ?success ?pool provers =
let provers = List.filter (fun (_,p) -> p <> Qed) provers in
if provers<>[] then
let monitor = match success with
| None -> None
| Some on_success ->
Some
begin function
| None -> on_success wpo None
| Some prover ->
let r = Wpo.get_result wpo VCS.Qed in
let prover =
if VCS.( r.verdict == Valid ) then VCS.Qed else prover in
on_success wpo (Some prover)
end in
let process (mode,prover) =
prove wpo ?config ~mode ?start ?progress ?result prover in
let all = Wp_parameters.RunAllProvers.get() in
let smoke = Wpo.is_smoke_test wpo in
ProverTask.spawn ?monitor ?pool ~all ~smoke
(List.map
(fun mp ->
let prover = snd mp in
let task = if delayed then Task.later process mp else process mp in
prover , task
) provers)
else
let process = simplify ?start ?result ~commit:true wpo >>= fun ok ->
begin
match success with
| None -> ()
| Some on_success ->
on_success wpo (if ok then Some VCS.Qed else None) ;
end ;
Task.return ()
in
let thread = Task.thread process in
let server = ProverTask.server () in
Task.spawn server ?pool thread