diff --git a/.gitignore b/.gitignore index 674ae831e09287c6e2206a699e51a84defbad72c..323d49ef8fc0bfde37c91aab521d7ab784f17273 100644 --- a/.gitignore +++ b/.gitignore @@ -69,6 +69,9 @@ why3.conf /bin/why3replayer.byte /bin/why3replayer.opt /bin/why3replayer +/bin/why3html.byte +/bin/why3html.opt +/bin/why3html # /doc/ /doc/version.tex diff --git a/Makefile.in b/Makefile.in index 6f62119a68ac2a61bca3778f44eb1e4d243fffd2..48b93b8243ad259631b4a55bb45b78d5fd35ae36 100644 --- a/Makefile.in +++ b/Makefile.in @@ -568,6 +568,56 @@ install_no_local:: install_local: bin/why3replayer +############### +# Html +############### + +HTML_FILES = xml termcode session session_ro html_session + +HTMLMODULES = $(addprefix src/ide/, $(HTML_FILES)) + +HTMLML = $(addsuffix .ml, $(HTMLMODULES)) +HTMLMLI = $(addsuffix .mli, $(HTMLMODULES)) +HTMLCMO = $(addsuffix .cmo, $(HTMLMODULES)) +HTMLCMX = $(addsuffix .cmx, $(HTMLMODULES)) + +$(HTMLCMO) $(HTMLCMX): INCLUDES += -I src/ide + +# build targets + +byte: bin/why3html.byte +opt: bin/why3html.opt + +bin/why3html.opt: src/why3.cmxa $(PGMCMX) $(HTMLCMX) + $(if $(QUIET), @echo 'Linking $@' &&) \ + $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^ + $(STRIP) $@ + +bin/why3html.byte: src/why3.cma $(PGMCMO) $(HTMLCMO) + $(if $(QUIET),@echo 'Linking $@' &&) \ + $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^ + +bin/why3html: bin/why3html.@OCAMLBEST@ + ln -sf why3html.@OCAMLBEST@ $@ + +# depend and clean targets + +include .depend.html + +.depend.html: src/ide/xml.ml + $(OCAMLDEP) -slash -I src -I src/ide $(HTMLML) $(HTMLMLI) > $@ + +depend: .depend.html + +clean:: + rm -f bin/why3html.byte bin/why3html.opt bin/why3html + rm -f .depend.html + +install_no_local:: + cp -f bin/why3html.@OCAMLBEST@ $(BINDIR)/why3html + +install_local: bin/why3html + ############### # Bench diff --git a/src/ide/html_session.ml b/src/ide/html_session.ml new file mode 100644 index 0000000000000000000000000000000000000000..344e83091a725504b30637280a6232900bdc1473 --- /dev/null +++ b/src/ide/html_session.ml @@ -0,0 +1,152 @@ +(**************************************************************************) +(* *) +(* 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. *) +(* *) +(**************************************************************************) + +open Why3 + +let includes = ref [] +let files = Queue.create () +let opt_version = ref false +let output_dir = ref "" +let allow_obsolete = ref true +let opt_config = ref None + + +let spec = Arg.align [ + ("-I", + Arg.String (fun s -> includes := s :: !includes), + " add s to loadpath") ; + ("-v", + Arg.Set opt_version, + " print version information") ; + ("-o", + Arg.Set_string output_dir, + " the directory to output the files"); + ("--strict", + Arg.Clear allow_obsolete, + " forbid obsolete session"); + "-C", Arg.String (fun s -> opt_config := Some s), + " Read configuration from "; + "--config", Arg.String (fun s -> opt_config := Some s), + " same as -C"; +] + + +let version_msg = Format.sprintf + "Why3 html session output, version %s (build date: %s)" + Config.version Config.builddate + +let usage_str = Format.sprintf + "Usage: %s [options] [|] ... " + (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 + Format.printf "%s@." version_msg; + exit 0 + end + +let output_dir = + if !output_dir = "" then begin + Format.printf "output_dir must be set@."; + exit 0 + end + else !output_dir + + +let allow_obsolete = !allow_obsolete +let includes = List.rev !includes + +open Session_ro + +let env = read_config ~includes !opt_config + +open Format +open Util + +let print_prover fmt = function + | Detected_prover pd -> fprintf fmt "%s" pd.prover_name + | Undetected_prover s -> fprintf fmt "%s" s + +let print_proof_status fmt = function + | Undone -> fprintf fmt "Undone" + | 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 = + fprintf fmt "%a : %a" + print_prover pa.prover + print_proof_status pa.proof_state + +let rec print_transf fmt tr = + fprintf fmt "%s :
    %a
" + tr.transf_name + (Pp.print_list Pp.newline print_goal) tr.subgoals + +and print_goal fmt g = + fprintf fmt "%s :
    %a%a
" + g.goal_name + (Pp.print_iter2 Mstr.iter Pp.newline Pp.nothing + Pp.nothing print_proof_attempt) + g.external_proofs + (Pp.print_iter2 Mstr.iter Pp.newline Pp.nothing + Pp.nothing print_transf) + g.transformations + +let print_theory fmt th = + fprintf fmt "%s :
    %a
" + th.theory_name + (Pp.print_list Pp.newline print_goal) th.goals + +let print_file fmt f = + fprintf fmt "%s :
    %a
" + f.file_name + (Pp.print_list Pp.newline print_theory) f.theories + +let print_session fmt s = + fprintf fmt "

    %a

" + (Pp.print_list Pp.newline print_file) s + +let run_file f = + let session_path = get_project_dir f in + let session = read_project_dir ~allow_obsolete ~env session_path in + let basename = Filename.basename session_path in + let cout = open_out (Filename.concat output_dir (basename^".html")) in + let fmt = formatter_of_out_channel cout in + fprintf fmt + " + + +A template for why3html + + +%a + + +" +print_session session + + +let () = Queue.iter run_file files