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
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)
~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 wpo =
Server.Main.async
(fun wpo ->
let r = Wpo.get_result wpo VCS.Qed in
VCS.( r.verdict == Valid ) ||
begin
started ?start wpo ;
if Wpo.reduce wpo then
let time = qed_time wpo in
let res = VCS.result ~time VCS.Valid in
(update ?result wpo VCS.Qed res ; true)
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 =
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 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