Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

html_session.ml 13.3 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-2011                                               *)
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

20
open Format
21
open Why3
22
module C = Whyconf
23 24 25 26 27 28

let files = Queue.create ()
let opt_version = ref false
let output_dir = ref ""
let allow_obsolete = ref true
let opt_config = ref None
29
let opt_context = ref false
30

31 32 33 34 35 36 37 38 39 40
type style =
  | Simple
  | Jstree

let opt_style = ref Jstree

let set_opt_style = function
  | "simple" -> opt_style := Simple
  | "jstree" -> opt_style := Jstree
  | _ -> assert false
41

42 43 44 45 46 47 48 49 50
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)

51 52 53
let spec = Arg.align [
  ("-v",
   Arg.Set opt_version,
54
   " Print version information") ;
55 56
  ("-o",
   Arg.Set_string output_dir,
57
   " The directory to output the files ('-' for stdout)");
58 59
  ("--strict",
   Arg.Clear allow_obsolete,
60
   " Forbid obsolete session");
61 62 63
  "-C", Arg.String (fun s -> opt_config := Some s),
      "<file> Read configuration from <file>";
  "--config", Arg.String (fun s -> opt_config := Some s),
64 65 66 67 68
      " Same as -C";
  "--context", Arg.Set opt_context,
  " Add context around the generated code in order to allow direct \
    visualisation (header, css, ...). It also add in the directory \
    all the needed external file. It can't be set with stdout output";
69 70
  "--style", Arg.Symbol (["simple";"jstree"], set_opt_style),
  " Set the style to use. 'simple' use only 'ul' and 'il' tag. 'jstree' use \
71 72 73 74 75 76 77 78 79 80 81 82
    the 'jstree' plugin of the javascript library 'jquery'.";
  "--add_pp", Arg.Tuple
    [Arg.String set_opt_pp_in;
     Arg.String set_opt_pp_cmd;
     Arg.String set_opt_pp_out],
  "<suffix> <cmd> <out_suffix> \
Add for the given prefix the given pretty-printer, \
the new file as the given out_suffix. cmd must contain '%i' which will be \
replace by the input file and '%o' which will be replaced by the output file.";
    "--coqdoc",
  Arg.Unit (fun ()->
    opt_pp := (".v",("coqdoc --no-index --html -o %o %i",".html"))::!opt_pp),
83 84 85 86
  " same as '--add_pp .v \"coqdoc --no-index --html -o %o %i\" .html'";
    Debug.Opt.desc_debug_list;
    Debug.Opt.desc_debug_all;
    Debug.Opt.desc_debug;
87 88 89
]


90
let version_msg = sprintf
91 92 93
  "Why3 html session output, version %s (build date: %s)"
  Config.version Config.builddate

94
let usage_str = sprintf
95 96 97 98 99 100 101 102 103
  "Usage: %s [options] [<file.why>|<project directory>] ... "
  (Filename.basename Sys.argv.(0))

let set_file f = Queue.push f files

let () = Arg.parse spec set_file usage_str

let () =
  if !opt_version then begin
104
    printf "%s@." version_msg;
105 106 107
    exit 0
  end

108 109 110 111
(* let () = *)
(*   List.iter (fun (in_,(cmd,out)) -> *)
(*     printf "in : %s, cmd : %s, out : %s@." in_ cmd out) !opt_pp *)

112 113 114 115
let () =
  Debug.Opt.set_flags_selected ();
  if  Debug.Opt.option_list () then exit 0

116
let output_dir =
117 118 119 120 121 122 123 124 125
  match !output_dir with
    | "" -> printf
      "Error: output_dir must be set@.";
      exit 1
    | "-" when !opt_context ->
      printf
        "Error: context and stdout output can't be set at the same time@.";
      exit 1
    | _ -> !output_dir
126

127 128
let edited_dst = Filename.concat output_dir "edited"

François Bobot's avatar
François Bobot committed
129 130 131
let whyconf = Whyconf.read_config !opt_config

open Session
132 133
open Util

134
type context =
135
    (string ->
François Bobot's avatar
François Bobot committed
136
     (formatter -> notask session -> unit) -> notask session
137 138 139 140 141
     -> unit, formatter, unit) format

let run_file (context : context) print_session f =
  let session_path = get_project_dir f in
  let basename = Filename.basename session_path in
François Bobot's avatar
François Bobot committed
142
  let session = read_session session_path in
143 144 145 146 147 148 149 150 151 152 153 154 155
  let cout = if output_dir = "-" then stdout else
      open_out (Filename.concat output_dir (basename^".html")) in
  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


module Simple =
struct

156
  let print_prover fmt pd = fprintf fmt "%s" pd.C.prover_name
157 158

  let print_proof_status fmt = function
François Bobot's avatar
François Bobot committed
159
    | Undone _ -> fprintf fmt "Undone"
160 161 162
    | Done pr -> fprintf fmt "Done : %a" Call_provers.print_prover_result pr
    | InternalFailure exn ->
      fprintf fmt "Failure : %a"Exn_printer.exn_printer exn
163

164 165
  let print_proof_attempt fmt pa =
    fprintf fmt "<li>%a : %a</li>"
François Bobot's avatar
François Bobot committed
166
      print_prover pa.proof_prover
167 168 169 170 171
      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
172
      (Pp.print_list Pp.newline print_goal) tr.transf_goals
173 174 175

  and print_goal fmt g =
    fprintf fmt "<li>%s : <ul>%a%a</ul></li>"
François Bobot's avatar
François Bobot committed
176 177
      g.goal_name.Ident.id_string
      (Pp.print_iter2 PHprover.iter Pp.newline Pp.nothing
178
         Pp.nothing print_proof_attempt)
François Bobot's avatar
François Bobot committed
179 180
      g.goal_external_proofs
      (Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing
181
         Pp.nothing print_transf)
François Bobot's avatar
François Bobot committed
182
      g.goal_transformations
183 184 185

  let print_theory fmt th =
    fprintf fmt "<li>%s : <ul>%a</ul></li>"
François Bobot's avatar
François Bobot committed
186 187
      th.theory_name.Ident.id_string
      (Pp.print_list Pp.newline print_goal) th.theory_goals
188 189 190 191

  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
192
      (Pp.print_list Pp.newline print_theory) f.file_theories
193 194 195

  let print_session _name fmt s =
    fprintf fmt "<ul>%a</ul>"
François Bobot's avatar
François Bobot committed
196 197
      (Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing Pp.nothing
         print_file) s.session_files
198 199 200


  let context : context = "<!DOCTYPE html
201 202 203 204
PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"
\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">
<html xmlns=\"http://www.w3.org/1999/xhtml\">
<head>
205
<title>Why3 session of %s</title>
206 207 208 209 210 211
</head>
<body>
%a
</body>
</html>
"
212

213 214
  let run_files () =
  Queue.iter (run_file context print_session) files
215

216
end
217

218 219 220
module Jstree =
struct

221 222 223 224 225
  let print_verified fmt b =
    if b
    then fprintf fmt "class='verified'"
    else fprintf fmt "class='notverified'"

226
  let print_prover fmt pd = fprintf fmt "%s" pd.C.prover_name
227 228

  let print_proof_status fmt = function
François Bobot's avatar
François Bobot committed
229
    | Undone _ -> fprintf fmt "<span class='notverified'>Undone</span>"
230 231
    | Done pr -> fprintf fmt "<span class='verified'>Done : %a</span>"
      Call_provers.print_prover_result pr
232
    | InternalFailure exn ->
233 234
      fprintf fmt "<span class='notverified'>Failure : %a</span>"
        Exn_printer.exn_printer exn
235

236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269
  let cmd_regexp = Str.regexp "%\\(.\\)"

  let pp_run input cmd output =
    let replace s = match Str.matched_group 1 s with
      | "%" -> "%"
      | "i" -> input
      | "o" -> output
      | _ -> failwith "unknown format specifier, use %%i, %%o"
    in
    let cmd = Str.global_substitute cmd_regexp replace cmd in
    let c = Sys.command cmd in
    if c <> 0 then
      eprintf "[Error] '%s' stopped abnormaly : code %i" cmd c

  let find_pp edited =
    let basename = Filename.basename edited in
    try
      let suff,(cmd,suff_out) =
        List.find (fun (s,_) -> ends_with basename s) !opt_pp in
      let base =
        String.sub basename 0 (String.length basename - String.length suff) in
      let base_dst = (base^suff_out) in
      if !opt_context then
        pp_run edited cmd (Filename.concat edited_dst base_dst);
      base_dst
    with Not_found ->
      eprintf "Default %s@." basename;
      (** default printer *)
      let base = try Filename.chop_extension basename with _ -> basename in
      let base_dst = base^".txt" in
      if !opt_context then
        Sysutil.copy_file edited (Filename.concat edited_dst base_dst);
      base_dst

270
  let print_proof_attempt fmt pa =
François Bobot's avatar
François Bobot committed
271
    match pa.proof_edited_as with
272 273
      | None ->
        fprintf fmt "@[<hov><li rel='prover' ><a href='#'>%a : %a</a></li>@]"
François Bobot's avatar
François Bobot committed
274
          print_prover pa.proof_prover
275 276 277 278 279 280
          print_proof_status pa.proof_state
      | Some f ->
        let output = find_pp f in
        fprintf fmt "@[<hov><li rel='prover' ><a href='#' \
onclick=\"showedited('%s'); return false;\">%a : %a</a></li>@]"
          output
François Bobot's avatar
François Bobot committed
281
          print_prover pa.proof_prover
282
          print_proof_status pa.proof_state
283 284 285

  let rec print_transf fmt tr =
    fprintf fmt
286 287 288
      "@[<hov><li rel='transf'><a href='#'>\
<span %a>%s</span></a>@,<ul>%a</ul></li>@]"
      print_verified tr.transf_verified
289
      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
294 295 296
      "@[<hov><li rel='goal'><a href='#'>\
<span %a>%s</a></a>@,<ul>%a%a</ul></li>@]"
      print_verified g.goal_verified
François Bobot's avatar
François Bobot committed
297 298
      g.goal_name.Ident.id_string
      (Pp.print_iter2 PHprover.iter Pp.newline Pp.nothing
299
         Pp.nothing print_proof_attempt)
François Bobot's avatar
François Bobot committed
300 301
      g.goal_external_proofs
      (Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing
302
         Pp.nothing print_transf)
François Bobot's avatar
François Bobot committed
303
      g.goal_transformations
304 305 306

  let print_theory fmt th =
    fprintf fmt
307 308 309
      "@[<hov><li rel='theory'><a href='#'>\
<span %a>%s</span></a>@,<ul>%a</ul></li>@]"
      print_verified th.theory_verified
François Bobot's avatar
François Bobot committed
310 311
      th.theory_name.Ident.id_string
      (Pp.print_list Pp.newline print_goal) th.theory_goals
312 313

  let print_file fmt f =
314 315 316 317
    fprintf fmt
      "@[<hov><li rel='file'><a href='#'>\
<span %a>%s</span></a>@,<ul>%a</ul></li>@]"
      print_verified f.file_verified
318
      f.file_name
François Bobot's avatar
François Bobot committed
319
      (Pp.print_list Pp.newline print_theory) f.file_theories
320 321 322 323

  let print_session_aux name fmt s =
    fprintf fmt "@[<hov><ul><a href='#'>%s</a>@,%a</ul>@]"
      name
François Bobot's avatar
François Bobot committed
324 325
      (Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing Pp.nothing print_file)
      s.session_files
326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374


  let print_session name fmt s =
    fprintf fmt
      "<a href='#' onclick=\"$('#%s_session').jstree('open_all');\">
expand all
</a> <a href='#' onclick=\"$('#%s_session').jstree('close_all');\">
close all
</a>
<div id=\"%s_session\" class=\"session\">
%a
</div>
<script type=\"text/javascript\" class=\"source\">
$(function () {
  $(\"#%s_session\").jstree({ 
      \"types\" : {
	   \"types\" : {
	   \"file\" : {
		\"icon\" : { \"image\" : \"images/folder16.png\"},
		      },
	   \"theory\" : {
		\"icon\" : { \"image\" : \"images/folder16.png\"},
		      },
	   \"goal\" : {
		\"icon\" : { \"image\" : \"images/file16.png\"},
		      },
	   \"prover\" : {
		\"icon\" : { \"image\" : \"images/wizard16.png\"},
		      },
	   \"transf\" : {
		\"icon\" : { \"image\" : \"images/configure16.png\"},
		      },
                        }
                },
      \"plugins\" : [\"themes\",\"html_data\",\"types\"]
        });
});
</script>
"
  name name name (print_session_aux name) s name


  let context : context = "<!DOCTYPE html
PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"
\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">
<html xmlns=\"http://www.w3.org/1999/xhtml\">
<head>
    <meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\" />
    <title>Why3 session of %s</title>
375 376
    <link rel=\"stylesheet\" type=\"text/css\"
     href=\"javascript/session.css\" />
377
    <script type=\"text/javascript\" src=\"javascript/jquery.js\"></script>
378 379 380 381
    <script type=\"text/javascript\" src=\"javascript/jquery.jstree.js\">\
</script>
    <script type=\"text/javascript\" src=\"javascript/session.js\">\
</script>
382 383 384
</head>
<body>
%a
385 386 387 388 389 390 391 392
<iframe src=\"\"  id='edited'>
<p>Your browser does not support iframes.</p>
</iframe>
<script type=\"text/javascript\" class=\"source\">
$(function () {
  $('#edited').hide()
})
</script>
393 394 395 396 397
</body>
</html>
"

  let run_files () =
398 399
    if !opt_context then
      if not (Sys.file_exists edited_dst) then Unix.mkdir edited_dst 0o755;
400 401
    Queue.iter (run_file context print_session) files;
    if !opt_context then
François Bobot's avatar
François Bobot committed
402
      let data_dir = Whyconf.datadir (Whyconf.get_main whyconf) in
403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423
      (** copy images *)
      let img_dir_src = Filename.concat data_dir "images" in
      let img_dir_dst = Filename.concat output_dir "images" in
      if not (Sys.file_exists img_dir_dst) then Unix.mkdir img_dir_dst 0o755;
      List.iter (fun img_name ->
        let from = Filename.concat img_dir_src img_name in
        let to_  = Filename.concat img_dir_dst img_name in
        Sysutil.copy_file from to_)
        ["folder16.png";"file16.png";"wizard16.png";"configure16.png"];
      (** copy javascript *)
      let js_dir_src = Filename.concat data_dir "javascript" in
      let js_dir_dst = Filename.concat output_dir "javascript" in
      Sysutil.copy_dir js_dir_src js_dir_dst

end


let () =
  match !opt_style with
    | Simple -> Simple.run_files ()
    | Jstree -> Jstree.run_files ()