why3session_html.ml 11.3 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
11

12
open Format
13
open Why3
14
open Why3session_lib
15

16
module Hprover = Whyconf.Hprover
17 18
module S = Session

19
let output_dir = ref ""
20
let opt_context = ref false
21

22
type style = SimpleTree | Table
23

24 25
let opt_style = ref Table
let default_style = "table"
26 27

let set_opt_style = function
28
  | "simpletree" -> opt_style := SimpleTree
29
  | "table" -> opt_style := Table
Andrei Paskevich's avatar
Andrei Paskevich committed
30
  | _ ->
31 32 33
    eprintf "Unknown html style, ignored@."

let () = set_opt_style default_style
34

35 36 37 38 39 40 41 42 43
let opt_pp = ref []

let set_opt_pp_in,set_opt_pp_cmd,set_opt_pp_out =
  let suf = ref "" in
  let cmd = ref "" in
  (fun s -> suf := s),
  (fun s -> cmd := s),
  (fun s -> opt_pp := (!suf,(!cmd,s))::!opt_pp)

44
let spec =
45 46
  ("-o",
   Arg.Set_string output_dir,
MARCHE Claude's avatar
MARCHE Claude committed
47
   "<path> output directory ('-' for stdout)") ::
48
  ("--context", Arg.Set opt_context,
49
   " add context around the generated HTML code") ::
50
  ("--style", Arg.Symbol (["simpletree";"table"], set_opt_style),
MARCHE Claude's avatar
MARCHE Claude committed
51
   " style to use, defaults to '" ^ default_style ^ "'."
52
) ::
53
  ("--add_pp", Arg.Tuple
54 55 56
    [Arg.String set_opt_pp_in;
     Arg.String set_opt_pp_cmd;
     Arg.String set_opt_pp_out],
57
  "<suffix> <cmd> <out_suffix> declare a pretty-printer for edited proofs") ::
58 59
  ("--coqdoc",
   Arg.Unit (fun ()->
60
    opt_pp := (".v",("coqdoc --no-index --html -o %o %i",".html"))::!opt_pp),
MARCHE Claude's avatar
MARCHE Claude committed
61
  " use coqdoc to print Coq proofs") ::
62
  common_options
63

François Bobot's avatar
François Bobot committed
64
open Session
65

66
type context =
67
    (string ->
68
     (formatter -> unit session -> unit) -> unit session
69 70
     -> unit, formatter, unit) format

71 72
let run_file (context : context) print_session fname =
  let project_dir = Session.get_project_dir fname in
73
  let session,_use_shapes = Session.read_session project_dir in
74 75 76 77 78 79
  let output_dir =
    if !output_dir = "" then project_dir else !output_dir
  in
  let basename = Filename.basename project_dir in
  let cout =
    if output_dir = "-" then stdout else
80
      open_out (Filename.concat output_dir ("why3session.html"))
81
  in
82 83 84 85 86 87 88 89
  let fmt = formatter_of_out_channel cout in
  if !opt_context
  then fprintf fmt context basename (print_session basename) session
  else print_session basename fmt session;
  pp_print_flush fmt ();
  if output_dir <> "-" then close_out cout


90 91 92 93 94 95 96 97 98 99
module Table =
struct


  let rec transf_depth tr =
    List.fold_left
      (fun depth g -> max depth (goal_depth g)) 0 tr.S.transf_goals
  and goal_depth g =
    S.PHstr.fold
      (fun _st tr depth -> max depth (1 + transf_depth tr))
100
      (S.goal_transformations g) 1
101 102 103 104 105

  let theory_depth t =
    List.fold_left
      (fun depth g -> max depth (goal_depth g)) 0 t.S.theory_goals

106
  let provers_stats provers theory =
107
    S.theory_iter_proof_attempt (fun a ->
108
      Hprover.replace provers a.S.proof_prover a.S.proof_prover) theory
109 110 111 112

  let print_prover = Whyconf.print_prover


Andrei Paskevich's avatar
Andrei Paskevich committed
113 114 115
  let color_of_status ?(dark=false) fmt b =
    fprintf fmt "%s" (if b then
        if dark then "008000" else "C0FFC0"
116 117 118 119
      else "FF0000")

let print_results fmt provers proofs =
  List.iter (fun p ->
120
    fprintf fmt "<td style=\"background-color:#";
121 122 123 124
    begin
      try
        let pr = S.PHprover.find proofs p in
        let s = pr.S.proof_state in
125 126
        begin
          match s with
127 128 129 130 131 132 133 134
	  | S.Done res ->
	    begin
	      match res.Call_provers.pr_answer with
		| Call_provers.Valid ->
                  fprintf fmt "C0FFC0\">%.2f" res.Call_provers.pr_time
		| Call_provers.Invalid ->
                  fprintf fmt "FF0000\">Invalid"
		| Call_provers.Timeout ->
MARCHE Claude's avatar
MARCHE Claude committed
135
                  fprintf fmt "FF8000\">Timeout (%ds)"
136
                    pr.S.proof_limit.Call_provers.limit_time
137
		| Call_provers.OutOfMemory ->
MARCHE Claude's avatar
MARCHE Claude committed
138
                  fprintf fmt "FF8000\">Out Of Memory (%dM)"
139
                    pr.S.proof_limit.Call_provers.limit_mem
140 141
		| Call_provers.StepLimitExceeded ->
                  fprintf fmt "FF8000\">Step limit exceeded"
142
		| Call_provers.Unknown _ ->
MARCHE Claude's avatar
MARCHE Claude committed
143
                  fprintf fmt "FF8000\">%.2f" res.Call_provers.pr_time
144
		| Call_provers.Failure _ ->
Andrei Paskevich's avatar
Andrei Paskevich committed
145 146 147
                  fprintf fmt "FF8000\">Failure"
		| Call_provers.HighFailure ->
                  fprintf fmt "FF8000\">High Failure"
148
	    end
149
	  | S.InternalFailure _ -> fprintf fmt "E0E0E0\">Internal Failure"
150 151 152 153
          | S.Interrupted -> fprintf fmt "E0E0E0\">Not yet run"
          | S.Unedited -> fprintf fmt "E0E0E0\">Not yet edited"
          | S.Scheduled | S.Running
          | S.JustEdited -> assert false
154
        end;
155
        if pr.S.proof_obsolete then fprintf fmt " (obsolete)"
MARCHE Claude's avatar
MARCHE Claude committed
156
      with Not_found -> fprintf fmt "E0E0E0\">---"
157 158 159
    end;
    fprintf fmt "</td>") provers

MARCHE Claude's avatar
MARCHE Claude committed
160 161
let rec num_lines acc tr =
  List.fold_left
Andrei Paskevich's avatar
Andrei Paskevich committed
162 163
    (fun acc g -> 1 +
      PHstr.fold (fun _ tr acc -> 1 + num_lines acc tr)
164
      (goal_transformations g) acc)
MARCHE Claude's avatar
MARCHE Claude committed
165 166
    acc tr.transf_goals

167 168
  let rec print_transf fmt depth max_depth provers tr =
    fprintf fmt "<tr>";
169
    for _i=1 to 0 (* depth-1 *) do fprintf fmt "<td></td>" done;
170
    fprintf fmt "<td style=\"background-color:#%a\" colspan=\"%d\">"
171
      (color_of_status ~dark:false) (Opt.inhabited tr.S.transf_verified)
MARCHE Claude's avatar
MARCHE Claude committed
172 173 174
      (max_depth - depth + 1);
    (* for i=1 to depth-1 do fprintf fmt "&nbsp;&nbsp;&nbsp;&nbsp;" done; *)
    fprintf fmt "%s</td>" tr.transf_name ;
175
    for _i=1 (* depth *) to (*max_depth - 1 + *) List.length provers do
176
      fprintf fmt "<td style=\"background-color:#E0E0E0\"></td>"
177 178
    done;
    fprintf fmt "</tr>@\n";
179
    fprintf fmt "<tr><td rowspan=\"%d\">&nbsp;&nbsp;</td>" (num_lines 0 tr);
MARCHE Claude's avatar
MARCHE Claude committed
180
    let (_:bool) = List.fold_left
181 182 183 184
      (fun needs_tr g ->
        print_goal fmt needs_tr (depth+1) max_depth provers g;
        true)
      false tr.transf_goals
MARCHE Claude's avatar
MARCHE Claude committed
185 186
    in ()

187 188
  and print_goal fmt needs_tr depth max_depth provers g =
    if needs_tr then fprintf fmt "<tr>";
MARCHE Claude's avatar
MARCHE Claude committed
189
    (* for i=1 to 0 (\* depth-1 *\) do fprintf fmt "<td></td>" done; *)
190
    fprintf fmt "<td style=\"background-color:#%a\" colspan=\"%d\">"
191
      (color_of_status ~dark:false) (Opt.inhabited (S.goal_verified g))
192
      (max_depth - depth + 1);
MARCHE Claude's avatar
MARCHE Claude committed
193
    (* for i=1 to depth-1 do fprintf fmt "&nbsp;&nbsp;&nbsp;&nbsp;" done; *)
MARCHE Claude's avatar
MARCHE Claude committed
194
    fprintf fmt "%s</td>" (S.goal_user_name g);
195
(*    for i=depth to max_depth-1 do fprintf fmt "<td></td>" done; *)
196
    print_results fmt provers (goal_external_proofs g);
197 198 199
    fprintf fmt "</tr>@\n";
    PHstr.iter
      (fun _ tr -> print_transf fmt depth max_depth provers tr)
200
      (goal_transformations g)
201

202
  let print_theory fn fmt th =
203 204
    let depth = theory_depth th in
    if depth > 0 then
205
    let provers = Hprover.create 9 in
206 207
    provers_stats provers th;
    let provers =
208
      Hprover.fold (fun _ pr acc -> pr :: acc) provers []
209 210
    in
    let provers = List.sort Whyconf.Prover.compare provers in
211 212 213 214 215 216
    let name =
      try
        let (l,t,_) = Theory.restore_path th.theory_name in
        String.concat "." ([fn]@l@[t])
      with Not_found -> fn ^ "." ^ th.theory_name.Ident.id_string
    in
217
    fprintf fmt "<h2><span style=\"color:#%a\">Theory \"%s\": "
218
      (color_of_status ~dark:true) (Opt.inhabited th.S.theory_verified)
219 220 221 222 223
      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;
224
    fprintf fmt "</span></h2>@\n";
MARCHE Claude's avatar
MARCHE Claude committed
225

226
    fprintf fmt "<table border=\"1\"><tr><td colspan=\"%d\">Obligations</td>" depth;
MARCHE Claude's avatar
MARCHE Claude committed
227
    (* fprintf fmt "<table border=\"1\"><tr><td>Obligations</td>"; *)
228 229 230
    List.iter
      (fun pr -> fprintf fmt "<td text-rotation=\"90\">%a</td>" print_prover pr)
      provers;
231
    fprintf fmt "</tr>@\n";
MARCHE Claude's avatar
MARCHE Claude committed
232
    List.iter (print_goal fmt true 1 depth provers) th.theory_goals;
233 234 235 236
    fprintf fmt "</table>@\n"

  let print_file fmt f =
    (* fprintf fmt "<h1>File %s</h1>@\n" f.file_name; *)
237 238
    let fn = Filename.basename f.file_name in
    let fn = Filename.chop_extension fn in
239
    fprintf fmt "%a"
240
      (Pp.print_list Pp.newline (print_theory fn)) f.file_theories
241 242 243 244 245 246 247 248

  let print_session name fmt s =
    fprintf fmt "<h1>Why3 Proof Results for Project \"%s\"</h1>@\n" name;
    fprintf fmt "%a"
      (Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing Pp.nothing
         print_file) s.session_files


249 250
  let context : context = "<!DOCTYPE html \
PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\" \
251
\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\
252 253 254 255 256 257 258 259 260 261
\n<html xmlns=\"http://www.w3.org/1999/xhtml\">\
\n<head>\
\n  <meta http-equiv=\"Content-Type\" content=\"text/html; charset=UTF-8\" />\
\n  <title>Why3 session of %s</title>\
\n</head>\
\n<body>\
\n%a\
\n</body>\
\n</html>\
\n"
262 263 264 265 266 267 268

  let run_one = run_file context print_session

end



269 270 271
module Simple =
struct

272
  let print_prover = Whyconf.print_prover
273 274

  let print_proof_status fmt = function
275 276 277 278
    | 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
279
    | InternalFailure exn ->
280
      fprintf fmt "Failure: %a"Exn_printer.exn_printer exn
281

282 283
  let print_proof_attempt fmt pa =
    fprintf fmt "<li>%a : %a</li>"
François Bobot's avatar
François Bobot committed
284
      print_prover pa.proof_prover
285 286 287 288 289
      print_proof_status pa.proof_state

  let rec print_transf fmt tr =
    fprintf fmt "<li>%s : <ul>%a</ul></li>"
      tr.transf_name
François Bobot's avatar
François Bobot committed
290
      (Pp.print_list Pp.newline print_goal) tr.transf_goals
291 292 293

  and print_goal fmt g =
    fprintf fmt "<li>%s : <ul>%a%a</ul></li>"
294
      (goal_name g).Ident.id_string
François Bobot's avatar
François Bobot committed
295
      (Pp.print_iter2 PHprover.iter Pp.newline Pp.nothing
296
         Pp.nothing print_proof_attempt)
297
      (goal_external_proofs g)
François Bobot's avatar
François Bobot committed
298
      (Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing
299
         Pp.nothing print_transf)
300
      (goal_transformations g)
301 302 303

  let print_theory fmt th =
    fprintf fmt "<li>%s : <ul>%a</ul></li>"
François Bobot's avatar
François Bobot committed
304 305
      th.theory_name.Ident.id_string
      (Pp.print_list Pp.newline print_goal) th.theory_goals
306 307 308 309

  let print_file fmt f =
    fprintf fmt "<li>%s : <ul>%a</ul></li>"
      f.file_name
François Bobot's avatar
François Bobot committed
310
      (Pp.print_list Pp.newline print_theory) f.file_theories
311 312 313

  let print_session _name fmt s =
    fprintf fmt "<ul>%a</ul>"
François Bobot's avatar
François Bobot committed
314 315
      (Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing Pp.nothing
         print_file) s.session_files
316 317


318 319
  let context : context = "<!DOCTYPE html \
PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\" \
320
\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\
321 322 323 324 325 326 327 328 329 330
\n<html xmlns=\"http://www.w3.org/1999/xhtml\">\
\n<head>\
\n  <meta http-equiv=\"Content-Type\" content=\"text/html; charset=UTF-8\" />\
\n  <title>Why3 session of %s</title>\
\n</head>\
\n<body>\
\n%a\
\n</body>\
\n</html>\
\n"
331

332
  let run_one = run_file context print_session
333

334
end
335

336

337
let run () =
338
  let _,_,should_exit1 = read_env_spec () in
339
  if should_exit1 then exit 1;
340 341 342
  match !opt_style with
    | Table -> iter_files Table.run_one
    | SimpleTree -> iter_files Simple.run_one
343 344 345

let cmd =
  { cmd_spec = spec;
346
    cmd_desc = "output session in HTML format";
347 348 349
    cmd_name = "html";
    cmd_run  = run;
  }
350 351 352 353 354 355 356


(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3session.byte"
End:
*)