Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
119
Issues
119
List
Boards
Labels
Service Desk
Milestones
Merge Requests
16
Merge Requests
16
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
8b1cb55a
Commit
8b1cb55a
authored
Mar 27, 2012
by
MARCHE Claude
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
make -bench option of why3replayer really work
parent
b41c3b5c
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
with
44 additions
and
22 deletions
+44
-22
src/ide/replay.ml
src/ide/replay.ml
+10
-4
src/session/session.ml
src/session/session.ml
+1
-1
src/session/session_scheduler.ml
src/session/session_scheduler.ml
+33
-17
No files found.
src/ide/replay.ml
View file @
8b1cb55a
...
...
@@ -375,12 +375,15 @@ let run_as_bench env_session =
let
sched
=
M
.
init
(
Whyconf
.
running_provers_max
(
Whyconf
.
get_main
config
))
in
eprintf
"Provers:@
.
"
;
eprintf
"Provers:@
"
;
let
provers
=
Whyconf
.
Mprover
.
fold
(
fun
_
p
acc
->
eprintf
"prover: %a@."
Whyconf
.
print_prover
p
.
Whyconf
.
prover
;
p
.
Whyconf
.
prover
::
acc
)
if
p
.
Whyconf
.
interactive
then
acc
else
begin
eprintf
"%a@ "
Whyconf
.
print_prover
p
.
Whyconf
.
prover
;
p
.
Whyconf
.
prover
::
acc
end
)
(
Whyconf
.
get_provers
env_session
.
Session
.
whyconf
)
[]
(*
Session.PHprover.fold
...
...
@@ -394,8 +397,11 @@ let run_as_bench env_session =
env_session.Session.loaded_provers []
*)
in
eprintf
"@."
;
let
callback
()
=
eprintf
"We should now save the session...@."
;
eprintf
"Saving session...@?"
;
Session
.
save_session
config
env_session
.
Session
.
session
;
eprintf
" done.@."
;
exit
0
in
M
.
play_all
env_session
sched
~
callback
~
timelimit
:
2
provers
;
...
...
src/session/session.ml
View file @
8b1cb55a
...
...
@@ -329,7 +329,7 @@ let save_status fmt s =
fprintf
fmt
"<undone/>@
\n
"
|
InternalFailure
msg
->
fprintf
fmt
"<internalfailure reason=
\"
%s
\"
/>@
\n
"
(
Printexc
.
to_string
msg
)
(
String
.
escaped
(
Printexc
.
to_string
msg
)
)
|
Done
r
->
save_result
fmt
r
...
...
src/session/session_scheduler.ml
View file @
8b1cb55a
...
...
@@ -343,21 +343,24 @@ let run_external_proof eS eT ?callback a =
(* info_window `ERROR "Proof already in progress" *)
let
ap
=
a
.
proof_prover
in
match
find_loadable_prover
eS
a
.
proof_prover
with
|
None
->
Debug
.
dprintf
debug
"[Info] Can't redo an external proof since the prover %a is not \
loaded@."
Whyconf
.
print_prover
a
.
proof_prover
|
None
->
Debug
.
dprintf
debug
"[Info] Can't redo an external proof since the prover %a is not loaded@."
Whyconf
.
print_prover
a
.
proof_prover
;
Util
.
apply_option2
()
callback
a
a
.
proof_state
|
Some
(
nap
,
npc
)
->
eprintf
"prover %a on goal %s@."
Whyconf
.
print_prover
a
.
proof_prover
a
.
proof_parent
.
goal_name
.
Ident
.
id_string
;
(* eprintf "prover %a on goal %s@." *)
(* Whyconf.print_prover a.proof_prover a.proof_parent.goal_name.Ident.id_string; *)
let
g
=
a
.
proof_parent
in
try
if
nap
==
ap
then
raise
Not_found
;
let
np_a
=
PHprover
.
find
g
.
goal_external_proofs
nap
in
if
O
.
replace_prover
np_a
a
then
begin
if
O
.
replace_prover
np_a
a
then
begin
(** The notification will be done by the new proof_attempt *)
O
.
remove
np_a
.
proof_key
;
raise
Not_found
end
O
.
remove
np_a
.
proof_key
;
raise
Not_found
end
with
Not_found
->
(** replace [a] by a new_proof attempt if [a.proof_prover] was not
loadable *)
...
...
@@ -366,12 +369,17 @@ loaded@."
let
a
=
copy_external_proof
~
notify
~
keygen
:
O
.
create
~
prover
:
nap
~
env_session
:
eS
a
in
O
.
init
a
.
proof_key
(
Proof_attempt
a
);
a
in
a
in
if
a
.
proof_edited_as
=
None
&&
npc
.
prover_config
.
Whyconf
.
interactive
then
set_proof_state
~
notify
~
obsolete
:
false
~
archived
:
false
(
Undone
Unedited
)
a
else
begin
begin
set_proof_state
~
notify
~
obsolete
:
false
~
archived
:
false
(
Undone
Unedited
)
a
;
Util
.
apply_option2
()
callback
a
a
.
proof_state
end
else
begin
let
previous_result
,
previous_obs
=
a
.
proof_state
,
a
.
proof_obsolete
in
let
timelimit
=
match
previous_result
with
...
...
@@ -407,7 +415,7 @@ loaded@."
let
command
=
String
.
concat
" "
(
npc
.
prover_config
.
Whyconf
.
command
::
npc
.
prover_config
.
Whyconf
.
extra_options
)
in
eprintf
"scheduling it...@."
;
(* eprintf "scheduling it...@."; *)
schedule_proof_attempt
~
timelimit
~
memlimit
:
0
?
old
~
command
...
...
@@ -674,12 +682,20 @@ let check_all eS eT ~callback =
(***********************************)
let
rec
play_on_goal_and_children
eS
eT
~
timelimit
todo
l
g
=
let
callback
_key
status
=
match
status
with
|
Undone
Running
|
Undone
Scheduled
->
()
|
_
->
Todo
.
_done
todo
()
;
(* eprintf "todo decreased to %d@." todo.Todo.todo *)
in
List
.
iter
(
fun
p
->
Todo
.
todo
todo
;
eprintf
"prover %a on goal %s@."
Whyconf
.
print_prover
p
g
.
goal_name
.
Ident
.
id_string
;
prover_on_goal
eS
eT
~
timelimit
p
g
)
(* eprintf "todo increased to %d@." todo.Todo.todo; *)
(* eprintf "prover %a on goal %s@." *)
(* Whyconf.print_prover p g.goal_name.Ident.id_string; *)
prover_on_goal
eS
eT
~
callback
~
timelimit
p
g
)
l
;
PHstr
.
iter
(
fun
_
t
->
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment