Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
d1f5eae2
Commit
d1f5eae2
authored
Sep 09, 2015
by
MARCHE Claude
Browse files
info --graph: start from time 0.1 to make a nicer graph
parent
22dc0f26
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/why3session/why3session_info.ml
View file @
d1f5eae2
...
...
@@ -395,7 +395,7 @@ let print_hist stats =
(
fun
p
h
acc
->
let
pf
,
ch
=
Filename
.
open_temp_file
"why3session"
".data"
in
if
acc
=
1
then
fprintf
main_fmt
"plot [0:%d] [0.
0
1:%.2f] "
fprintf
main_fmt
"plot [0:%d] [0.1:%.2f] "
(
stats
.
nb_proved_sub_goals
+
stats
.
nb_proved_root_goals
)
max_sum_times
else
...
...
@@ -406,7 +406,7 @@ let print_hist stats =
let
fmt
=
formatter_of_out_channel
ch
in
(* The time is also accumulated in order to obtain the total cpu time
taken to reach the given number of proved goal *)
fprintf
fmt
"0.
0
1 0@
\n
"
;
fprintf
fmt
"0.1 0@
\n
"
;
let
(
_
:
float
*
int
)
=
Mfloat
.
fold
(
fun
t
c
(
acct
,
accc
)
->
...
...
@@ -414,7 +414,7 @@ let print_hist stats =
let
acct
=
(
float
c
)
*.
t
+.
acct
in
fprintf
fmt
"%.2f %d@
\n
"
acct
accc
;
(
acct
,
accc
))
h
(
0
.
0
,
0
)
h
(
0
.
1
,
0
)
in
fprintf
fmt
"@."
;
close_out
ch
;
...
...
Write
Preview
Supports
Markdown
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