Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
Why3
why3
Commits
a465e9b2
Commit
a465e9b2
authored
Jun 27, 2017
by
MARCHE Claude
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
restored why3session html
parent
420977e1
Changes
5
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
5 changed files
with
229 additions
and
245 deletions
+229
-245
Makefile.in
Makefile.in
+2
-1
examples/dijkstra/why3session.xml
examples/dijkstra/why3session.xml
+142
-154
examples/dijkstra/why3shapes.gz
examples/dijkstra/why3shapes.gz
+0
-0
src/why3session/why3session_html.ml
src/why3session/why3session_html.ml
+84
-89
src/why3session/why3session_main.ml
src/why3session/why3session_main.ml
+1
-1
No files found.
Makefile.in
View file @
a465e9b2
...
...
@@ -822,9 +822,10 @@ install_local:: bin/why3webserver
###############
SESSION_FILES
=
why3session_lib why3session_info
\
why3session_html
\
why3session_main
# TODO: why3session_copy why3session_rm why3session_csv why3session_run
# why3session_latex
why3session_html
why3session_output
# why3session_latex why3session_output
SESSIONMODULES
=
$(
addprefix
src/why3session/,
$(SESSION_FILES)
)
...
...
examples/dijkstra/why3session.xml
View file @
a465e9b2
This diff is collapsed.
Click to expand it.
examples/dijkstra/why3shapes.gz
View file @
a465e9b2
No preview for this file type
src/why3session/why3session_html.ml
View file @
a465e9b2
...
...
@@ -65,12 +65,12 @@ open Session_itp
type
context
=
(
string
->
(
formatter
->
unit
session
->
unit
)
->
unit
session
(
formatter
->
session
->
unit
)
->
session
->
unit
,
formatter
,
unit
)
format
let
run_file
(
context
:
context
)
print_session
fname
=
let
project_dir
=
S
.
get_project_dir
fname
in
let
session
,_
use_shapes
=
S
.
read_session
projec
t_dir
in
let
ses
,_
=
read_session
fname
in
let
project_dir
=
ge
t_dir
ses
in
let
output_dir
=
if
!
output_dir
=
""
then
project_dir
else
!
output_dir
in
...
...
@@ -81,8 +81,8 @@ let run_file (context : context) print_session fname =
in
let
fmt
=
formatter_of_out_channel
cout
in
if
!
opt_context
then
fprintf
fmt
context
basename
(
print_session
basename
)
ses
sion
else
print_session
basename
fmt
ses
sion
;
then
fprintf
fmt
context
basename
(
print_session
basename
)
ses
else
print_session
basename
fmt
ses
;
pp_print_flush
fmt
()
;
if
output_dir
<>
"-"
then
close_out
cout
...
...
@@ -91,21 +91,21 @@ module Table =
struct
let
rec
transf_depth
tr
=
let
rec
transf_depth
s
tr
=
List
.
fold_left
(
fun
depth
g
->
max
depth
(
goal_depth
g
))
0
tr
.
S
.
transf_goals
and
goal_depth
g
=
S
.
PH
st
r
.
fold
(
fun
_st
tr
depth
->
max
depth
(
1
+
transf_depth
tr
))
(
S
.
goal
_transformations
g
)
1
(
fun
depth
g
->
max
depth
(
goal_depth
s
g
))
0
(
get_sub_tasks
s
tr
)
and
goal_depth
s
g
=
Li
st
.
fold
_left
(
fun
depth
tr
->
max
depth
(
1
+
transf_depth
s
tr
))
1
(
get
_transformations
s
g
)
let
theory_depth
t
=
let
theory_depth
s
t
=
List
.
fold_left
(
fun
depth
g
->
max
depth
(
goal_depth
g
))
0
t
.
S
.
theory_goals
(
fun
depth
g
->
max
depth
(
goal_depth
s
g
))
0
(
theory_goals
t
)
let
provers_stats
provers
theory
=
S
.
theory_iter_proof_attempt
(
fun
a
->
Hprover
.
replace
provers
a
.
S
.
proof_
prover
a
.
S
.
proof_
prover
)
theory
let
provers_stats
s
provers
theory
=
theory_iter_proof_attempt
s
(
fun
a
->
Hprover
.
replace
provers
a
.
prover
a
.
prover
)
theory
let
print_prover
=
Whyconf
.
print_prover
...
...
@@ -115,16 +115,16 @@ struct
if
dark
then
"008000"
else
"C0FFC0"
else
"FF0000"
)
let
print_results
fmt
provers
proofs
=
let
print_results
fmt
s
provers
proofs
=
List
.
iter
(
fun
p
->
fprintf
fmt
"<td bgcolor=
\"
#"
;
begin
try
let
pr
=
S
.
P
Hprover
.
find
proofs
p
in
let
s
=
pr
.
S
.
proof_state
in
let
pr
=
get_proof_attempt_node
s
(
Hprover
.
find
proofs
p
)
in
let
s
=
pr
.
proof_state
in
begin
match
s
with
|
S
.
Don
e
res
->
|
S
om
e
res
->
begin
match
res
.
Call_provers
.
pr_answer
with
|
Call_provers
.
Valid
->
...
...
@@ -133,10 +133,10 @@ let print_results fmt provers proofs =
fprintf
fmt
"FF0000
\"
>Invalid"
|
Call_provers
.
Timeout
->
fprintf
fmt
"FF8000
\"
>Timeout (%ds)"
pr
.
S
.
proof_
limit
.
Call_provers
.
limit_time
pr
.
limit
.
Call_provers
.
limit_time
|
Call_provers
.
OutOfMemory
->
fprintf
fmt
"FF8000
\"
>Out Of Memory (%dM)"
pr
.
S
.
proof_
limit
.
Call_provers
.
limit_mem
pr
.
limit
.
Call_provers
.
limit_mem
|
Call_provers
.
StepLimitExceeded
->
fprintf
fmt
"FF8000
\"
>Step limit exceeded"
|
Call_provers
.
Unknown
_
->
...
...
@@ -146,81 +146,78 @@ let print_results fmt provers proofs =
|
Call_provers
.
HighFailure
->
fprintf
fmt
"FF8000
\"
>High Failure"
end
|
S
.
InternalFailure
_
->
fprintf
fmt
"E0E0E0
\"
>Internal Failure"
|
S
.
Interrupted
->
fprintf
fmt
"E0E0E0
\"
>Not yet run"
|
S
.
Unedited
->
fprintf
fmt
"E0E0E0
\"
>Not yet edited"
|
S
.
Scheduled
|
S
.
Running
|
S
.
JustEdited
->
assert
false
|
None
->
fprintf
fmt
"E0E0E0
\"
>result missing"
end
;
if
pr
.
S
.
proof_obsolete
then
fprintf
fmt
" (obsolete)"
with
Not_found
->
fprintf
fmt
"E0E0E0
\"
>---"
end
;
fprintf
fmt
"</td>"
)
provers
let
rec
num_lines
acc
tr
=
let
rec
num_lines
s
acc
tr
=
List
.
fold_left
(
fun
acc
g
->
1
+
PH
st
r
.
fold
(
fun
_
tr
acc
->
1
+
num_lines
acc
tr
)
(
goal
_transformations
g
)
acc
)
acc
tr
.
transf_goals
Li
st
.
fold
_left
(
fun
acc
tr
->
1
+
num_lines
s
acc
tr
)
acc
(
get
_transformations
s
g
))
acc
(
get_sub_tasks
s
tr
)
let
rec
print_transf
fmt
depth
max_depth
provers
tr
=
let
rec
print_transf
fmt
s
depth
max_depth
provers
tr
=
fprintf
fmt
"<tr>"
;
for
_i
=
1
to
0
(* depth-1 *)
do
fprintf
fmt
"<td></td>"
done
;
fprintf
fmt
"<td bgcolor=
\"
#%a
\"
colspan=
\"
%d
\"
>"
(
color_of_status
~
dark
:
false
)
(
Opt
.
inhabited
tr
.
S
.
transf_verified
)
(
color_of_status
~
dark
:
false
)
(
tn_proved
s
tr
)
(
max_depth
-
depth
+
1
);
(* for i=1 to depth-1 do fprintf fmt " " done; *)
fprintf
fmt
"%s</td>"
tr
.
transf_name
;
let
name
=
(
get_transf_name
s
tr
)
^
(
String
.
concat
""
(
get_transf_args
s
tr
))
in
fprintf
fmt
"%s</td>"
name
;
for
_i
=
1
(* depth *)
to
(*max_depth - 1 + *)
List
.
length
provers
do
fprintf
fmt
"<td bgcolor=
\"
#E0E0E0
\"
></td>"
done
;
fprintf
fmt
"</tr>@
\n
"
;
fprintf
fmt
"<td rowspan=
\"
%d
\"
> </td>"
(
num_lines
0
tr
);
fprintf
fmt
"<td rowspan=
\"
%d
\"
> </td>"
(
num_lines
s
0
tr
);
let
(
_
:
bool
)
=
List
.
fold_left
(
fun
is_first
g
->
print_goal
fmt
is_first
(
depth
+
1
)
max_depth
provers
g
;
print_goal
fmt
s
is_first
(
depth
+
1
)
max_depth
provers
g
;
false
)
true
tr
.
transf_goals
true
(
get_sub_tasks
s
tr
)
in
()
and
print_goal
fmt
is_first
depth
max_depth
provers
g
=
and
print_goal
fmt
s
is_first
depth
max_depth
provers
g
=
if
not
is_first
then
fprintf
fmt
"<tr>"
;
(* for i=1 to 0 (\* depth-1 *\) do fprintf fmt "<td></td>" done; *)
fprintf
fmt
"<td bgcolor=
\"
#%a
\"
colspan=
\"
%d
\"
>"
(
color_of_status
~
dark
:
false
)
(
Opt
.
inhabited
(
S
.
goal_verified
g
)
)
(
color_of_status
~
dark
:
false
)
(
pn_proved
s
g
)
(
max_depth
-
depth
+
1
);
(* for i=1 to depth-1 do fprintf fmt " " done; *)
fprintf
fmt
"%s</td>"
(
S
.
goal_user
_name
g
);
fprintf
fmt
"%s</td>"
(
get_proof
_name
s
g
)
.
Ident
.
id_string
;
(* for i=depth to max_depth-1 do fprintf fmt "<td></td>" done; *)
print_results
fmt
provers
(
g
oal_external_proof
s
g
);
print_results
fmt
s
provers
(
g
et_proof_attempt_ids
s
g
);
fprintf
fmt
"</tr>@
\n
"
;
PH
st
r
.
iter
(
fun
_
tr
->
print_transf
fmt
depth
max_depth
provers
tr
)
(
g
oal
_transformations
g
)
Li
st
.
iter
(
print_transf
fmt
s
depth
max_depth
provers
)
(
g
et
_transformations
s
g
)
let
print_theory
fn
fmt
th
=
let
depth
=
theory_depth
th
in
let
print_theory
s
fn
fmt
th
=
let
depth
=
theory_depth
s
th
in
if
depth
>
0
then
let
provers
=
Hprover
.
create
9
in
provers_stats
provers
th
;
provers_stats
s
provers
th
;
let
provers
=
Hprover
.
fold
(
fun
_
pr
acc
->
pr
::
acc
)
provers
[]
in
let
provers
=
List
.
sort
Whyconf
.
Prover
.
compare
provers
in
let
name
=
try
let
(
l
,
t
,_
)
=
Theory
.
restore_path
th
.
theory_name
in
let
(
l
,
t
,_
)
=
Theory
.
restore_path
(
theory_name
th
)
in
String
.
concat
"."
([
fn
]
@
l
@
[
t
])
with
Not_found
->
fn
^
"."
^
th
.
theory_name
.
Ident
.
id_string
with
Not_found
->
fn
^
"."
^
(
theory_name
th
)
.
Ident
.
id_string
in
fprintf
fmt
"<h2><font color=
\"
#%a
\"
>Theory
\"
%s
\"
: "
(
color_of_status
~
dark
:
true
)
(
Opt
.
inhabited
th
.
S
.
theory_verified
)
(
color_of_status
~
dark
:
true
)
(
th_proved
s
th
)
name
;
begin
match
th
.
S
.
theory_verified
with
|
Some
t
->
fprintf
fmt
"fully verified in %.02f s"
t
|
None
->
fprintf
fmt
"not fully verified"
end
;
if
th_proved
s
th
then
fprintf
fmt
"fully verified in %%.02f s"
else
fprintf
fmt
"not fully verified"
;
fprintf
fmt
"</font></h2>@
\n
"
;
fprintf
fmt
"<table border=
\"
1
\"
><tr><td colspan=
\"
%d
\"
>Obligations</td>"
depth
;
...
...
@@ -229,21 +226,21 @@ let rec num_lines acc tr =
(
fun
pr
->
fprintf
fmt
"<td text-rotation=
\"
90
\"
>%a</td>"
print_prover
pr
)
provers
;
fprintf
fmt
"</td></tr>@
\n
"
;
List
.
iter
(
print_goal
fmt
true
1
depth
provers
)
th
.
theory_goals
;
List
.
iter
(
print_goal
fmt
s
true
1
depth
provers
)
(
theory_goals
th
)
;
fprintf
fmt
"</table>@
\n
"
let
print_file
fmt
f
=
let
print_file
s
fmt
f
=
(* fprintf fmt "<h1>File %s</h1>@\n" f.file_name; *)
let
fn
=
Filename
.
basename
f
.
file_name
in
let
fn
=
Filename
.
basename
(
file_name
f
)
in
let
fn
=
Filename
.
chop_extension
fn
in
fprintf
fmt
"%a"
(
Pp
.
print_list
Pp
.
newline
(
print_theory
fn
))
f
.
file_theories
(
Pp
.
print_list
Pp
.
newline
(
print_theory
s
fn
))
(
file_theories
f
)
let
print_session
name
fmt
s
=
fprintf
fmt
"<h1>Why3 Proof Results for Project
\"
%s
\"
</h1>@
\n
"
name
;
fprintf
fmt
"%a"
(
Pp
.
print_iter2
P
Hstr
.
iter
Pp
.
newline
Pp
.
nothing
Pp
.
nothing
print_file
)
s
.
session
_files
(
Pp
.
print_iter2
Stdlib
.
Hstr
.
iter
Pp
.
newline
Pp
.
nothing
Pp
.
nothing
(
print_file
s
))
(
get
_files
s
)
let
context
:
context
=
"<!DOCTYPE html\
...
...
@@ -271,47 +268,45 @@ struct
let
print_prover
=
Whyconf
.
print_prover
let
print_proof_status
fmt
=
function
|
Interrupted
->
fprintf
fmt
"Not yet run"
|
Unedited
->
fprintf
fmt
"Not yet edited"
|
JustEdited
|
Scheduled
|
Running
->
assert
false
|
Done
pr
->
fprintf
fmt
"Done: %a"
Call_provers
.
print_prover_result
pr
|
InternalFailure
exn
->
fprintf
fmt
"Failure: %a"
Exn_printer
.
exn_printer
exn
let
print_proof_attempt
fmt
pa
=
|
None
->
fprintf
fmt
"No result"
|
Some
res
->
fprintf
fmt
"Done: %a"
Call_provers
.
print_prover_result
res
let
print_proof_attempt
s
fmt
pa
=
let
pa
=
get_proof_attempt_node
s
pa
in
fprintf
fmt
"<li>%a : %a</li>"
print_prover
pa
.
proof_
prover
print_prover
pa
.
prover
print_proof_status
pa
.
proof_state
let
rec
print_transf
fmt
tr
=
let
rec
print_transf
s
fmt
tr
=
let
name
=
(
get_transf_name
s
tr
)
^
(
String
.
concat
""
(
get_transf_args
s
tr
))
in
fprintf
fmt
"<li>%s : <ul>%a</ul></li>"
tr
.
transf_
name
(
Pp
.
print_list
Pp
.
newline
print_goal
)
tr
.
transf_goals
name
(
Pp
.
print_list
Pp
.
newline
(
print_goal
s
))
(
get_sub_tasks
s
tr
)
and
print_goal
fmt
g
=
and
print_goal
s
fmt
g
=
fprintf
fmt
"<li>%s : <ul>%a%a</ul></li>"
(
goal_name
g
)
.
Ident
.
id_string
(
Pp
.
print_iter2
PHprover
.
iter
Pp
.
newline
Pp
.
nothing
Pp
.
nothing
print_proof_attempt
)
(
goal_external_proofs
g
)
(
Pp
.
print_iter2
PHstr
.
iter
Pp
.
newline
Pp
.
nothing
Pp
.
nothing
print_transf
)
(
goal_transformations
g
)
let
print_theory
fmt
th
=
(
get_proof_name
s
g
)
.
Ident
.
id_string
(
Pp
.
print_iter2
Hprover
.
iter
Pp
.
newline
Pp
.
nothing
Pp
.
nothing
(
print_proof_attempt
s
))
(
get_proof_attempt_ids
s
g
)
(
Pp
.
print_iter1
List
.
iter
Pp
.
newline
(
print_transf
s
))
(
get_transformations
s
g
)
let
print_theory
s
fmt
th
=
fprintf
fmt
"<li>%s : <ul>%a</ul></li>"
th
.
theory_name
.
Ident
.
id_string
(
Pp
.
print_list
Pp
.
newline
print_goal
)
th
.
theory_goals
(
theory_name
th
)
.
Ident
.
id_string
(
Pp
.
print_list
Pp
.
newline
(
print_goal
s
))
(
theory_goals
th
)
let
print_file
fmt
f
=
let
print_file
s
fmt
f
=
fprintf
fmt
"<li>%s : <ul>%a</ul></li>"
f
.
file_name
(
Pp
.
print_list
Pp
.
newline
print_theory
)
f
.
file_theories
(
file_name
f
)
(
Pp
.
print_list
Pp
.
newline
(
print_theory
s
))
(
file_theories
f
)
let
print_session
_name
fmt
s
=
fprintf
fmt
"<ul>%a</ul>"
(
Pp
.
print_iter2
P
Hstr
.
iter
Pp
.
newline
Pp
.
nothing
Pp
.
nothing
print_file
)
s
.
session
_files
(
Pp
.
print_iter2
Stdlib
.
Hstr
.
iter
Pp
.
newline
Pp
.
nothing
Pp
.
nothing
(
print_file
s
))
(
get
_files
s
)
let
context
:
context
=
"<!DOCTYPE html\
...
...
src/why3session/why3session_main.ml
View file @
a465e9b2
...
...
@@ -16,9 +16,9 @@ open Why3session_lib
let
cmds
=
[
|
Why3session_info
.
cmd
;
Why3session_html
.
cmd
;
(*
Why3session_latex.cmd;
Why3session_html.cmd;
Why3session_csv.cmd;
Why3session_copy.cmd_mod;
Why3session_copy.cmd_copy;
...
...
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