From e465656be7e67ee3c02acf12a53c8388ae384b0a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 20 Jan 2007 16:20:16 +0000 Subject: [PATCH] Just a few lines test to understand with Cezary Kalinsky how much effort is required to integrate Matita in his generic AJAX based interface. matitawiki is an executable that reads from stdin and prints output and error on stdout/stderr (both followed by (Char.chr 249) after each command). All the interactive commands (thus also "undo") are not supported. --- helm/software/matita/Makefile | 13 +- helm/software/matita/matitaWiki.ml | 198 +++++++++++++++++++++++++++++ helm/software/matita/matitac.ml | 3 +- 3 files changed, 211 insertions(+), 3 deletions(-) create mode 100644 helm/software/matita/matitaWiki.ml diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile index c0e31d643..ed5ebb320 100644 --- a/helm/software/matita/Makefile +++ b/helm/software/matita/Makefile @@ -16,7 +16,7 @@ OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS) OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS) INSTALL_PROGRAMS= matita matitac INSTALL_PROGRAMS_LINKS_MATITA= cicbrowser -INSTALL_PROGRAMS_LINKS_MATITAC= matitadep matitamake matitaclean matitaprover +INSTALL_PROGRAMS_LINKS_MATITAC= matitadep matitamake matitaclean matitaprover matitawiki MATITA_FLAGS = -noprofile NODB=false @@ -53,6 +53,8 @@ CCMOS = \ matitaExcPp.cmo \ matitaEngine.cmo \ matitacLib.cmo \ + applyTransformation.cmo \ + matitaWiki.cmo \ matitaprover.cmo \ $(NULL) MAINCMOS = \ @@ -62,7 +64,7 @@ MAINCMOS = \ gragrep.cmo \ $(NULL) PROGRAMS_BYTE = \ - matita matitac cicbrowser matitadep matitaclean matitamake matitaprover + matita matitac cicbrowser matitadep matitaclean matitamake matitaprover matitawiki PROGRAMS = $(PROGRAMS_BYTE) matitatop PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE)) NOINST_PROGRAMS = dump_moo gragrep @@ -157,6 +159,11 @@ matitadep: matitac matitadep.opt: matitac.opt $(H)test -f $@ || ln -s $< $@ +matitawiki: matitac + $(H)test -f $@ || ln -s $< $@ +matitawiki.opt: matitac.opt + $(H)test -f $@ || ln -s $< $@ + matitaclean: matitac $(H)test -f $@ || ln -s $< $@ matitaclean.opt: matitac.opt @@ -357,6 +364,8 @@ matitadep.opt.static: matitac.opt.static $(H)test -f $@ || ln -s $< $@ matitaclean.opt.static: matitac.opt.static $(H)test -f $@ || ln -s $< $@ +matitawiki.opt.static: matitac.opt.static + $(H)test -f $@ || ln -s $< $@ matitamake.opt.static: matitac.opt.static $(H)test -f $@ || ln -s $< $@ cicbrowser.opt.static: matita.opt.static diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml new file mode 100644 index 000000000..3beadf1fe --- /dev/null +++ b/helm/software/matita/matitaWiki.ml @@ -0,0 +1,198 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM 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. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(* $Id: matitacLib.ml 7090 2006-12-12 14:04:59Z fguidi $ *) + +open Printf + +open GrafiteTypes + +exception AttemptToInsertAnAlias + + +(** {2 Initialization} *) + +let grafite_status = (ref None : GrafiteTypes.status option ref) +let lexicon_status = (ref None : LexiconEngine.status option ref) + +let run_script is eval_function = + let lexicon_status',grafite_status' = + match !lexicon_status,!grafite_status with + | Some ss, Some s -> ss,s + | _,_ -> assert false + in + let cb = fun _ _ -> () in + let matita_debug = Helm_registry.get_bool "matita.debug" in + try + match eval_function lexicon_status' grafite_status' is cb with + [] -> raise End_of_file + | ((grafite_status'',lexicon_status''),None)::_ -> + lexicon_status := Some lexicon_status''; + grafite_status := Some grafite_status'' + | (s,Some _)::_ -> raise AttemptToInsertAnAlias + with + | GrafiteEngine.Drop + | End_of_file + | CicNotationParser.Parse_error _ + | HExtlib.Localized _ as exn -> raise exn + | exn -> + if not matita_debug then + HLog.error (snd (MatitaExcPp.to_string exn)) ; + raise exn + +let clean_exit n = + let opt_exit = + function + None -> () + | Some n -> exit n + in + match !grafite_status with + None -> opt_exit n + | Some grafite_status -> + try + let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in + LibraryClean.clean_baseuris ~verbose:false [baseuri]; + opt_exit n + with GrafiteTypes.Option_error("baseuri", "not found") -> + (* no baseuri ==> nothing to clean yet *) + opt_exit n + +let terminate () = + let terminator = String.make 1 (Char.chr 249) in + print_endline terminator; + prerr_endline terminator +;; + +let rec interactive_loop () = + (* every loop is terminated by a terminator both on stdout and stderr *) + let interactive_loop () = terminate(); interactive_loop () in + let str = Ulexing.from_utf8_channel stdin in + let watch_statuses lexicon_status grafite_status = + match grafite_status.GrafiteTypes.proof_status with + GrafiteTypes.Incomplete_proof + {GrafiteTypes.proof = uri,metasenv,bo,ty,attrs ; + GrafiteTypes.stack = stack } -> + let open_goals = Continuationals.Stack.open_goals stack in + print_endline + (String.concat "\n" + (List.map + (fun i -> + ApplyTransformation.txt_of_cic_sequent 80 metasenv + (List.find (fun (j,_,_) -> j=i) metasenv) + ) open_goals)) + | _ -> () + in + let include_paths = + Helm_registry.get_list Helm_registry.string "matita.includes" in + try + run_script str + (MatitaEngine.eval_from_stream ~first_statement_only:true ~prompt:false + ~include_paths ~watch_statuses) ; + interactive_loop () + with + | GrafiteEngine.Macro (floc,_) -> + let x, y = HExtlib.loc_of_floc floc in + HLog.error + (sprintf "A macro has been found in a script at %d-%d" x y); + interactive_loop () + | Sys.Break -> HLog.error "user break!"; interactive_loop () + | GrafiteTypes.Command_error _ -> interactive_loop () + | HExtlib.Localized (floc,CicNotationParser.Parse_error err) -> + let x, y = HExtlib.loc_of_floc floc in + HLog.error (sprintf "Parse error at %d-%d: %s" x y err); + interactive_loop () + | End_of_file as exn -> raise exn + | exn -> HLog.error (Printexc.to_string exn); interactive_loop () + + +let main () = + MatitaInit.initialize_all (); + (* must be called after init since args are set by cmdline parsing *) + let system_mode = Helm_registry.get_bool "matita.system" in + Helm_registry.set_int "matita.verbosity" 0; + let include_paths = + Helm_registry.get_list Helm_registry.string "matita.includes" in + grafite_status := Some (GrafiteSync.init ()); + lexicon_status := + Some (CicNotation2.load_notation ~include_paths + BuildTimeConf.core_notation_script); + Sys.catch_break true; + let origcb = HLog.get_log_callback () in + let origcb t s = origcb t ((if system_mode then "[S] " else "") ^ s) in + let newcb tag s = + match tag with + | `Debug -> () + | `Message | `Warning | `Error -> origcb tag s + in + HLog.set_log_callback newcb; + let matita_debug = Helm_registry.get_bool "matita.debug" in + try + (try + interactive_loop () + with + | End_of_file -> () + | GrafiteEngine.Drop -> clean_exit (Some 1) + ); + let proof_status,moo_content_rev,metadata,lexicon_content_rev = + match !lexicon_status,!grafite_status with + | Some ss, Some s -> + s.proof_status, s.moo_content_rev, ss.LexiconEngine.metadata, + ss.LexiconEngine.lexicon_content_rev + | _,_ -> assert false + in + if proof_status <> GrafiteTypes.No_proof then + begin + HLog.error + "there are still incomplete proofs at the end of the script"; + clean_exit (Some 2) + end + else + begin + let baseuri = + GrafiteTypes.get_string_option + (match !grafite_status with + None -> assert false + | Some s -> s) "baseuri" in + let moo_fname = + LibraryMisc.obj_file_of_baseuri + ~must_exist:false ~baseuri ~writable:true + in + let lexicon_fname= + LibraryMisc.lexicon_file_of_baseuri + ~must_exist:false ~baseuri ~writable:true + in + let metadata_fname = + LibraryMisc.metadata_file_of_baseuri + ~must_exist:false ~baseuri ~writable:true + in + GrafiteMarshal.save_moo moo_fname moo_content_rev; + LibraryNoDb.save_metadata metadata_fname metadata; + LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev; + exit 0 + end + with + | exn -> + if matita_debug then raise exn; + clean_exit (Some 3) diff --git a/helm/software/matita/matitac.ml b/helm/software/matita/matitac.ml index b4a3119e0..2249998e9 100644 --- a/helm/software/matita/matitac.ml +++ b/helm/software/matita/matitac.ml @@ -32,7 +32,8 @@ let main () = |"matitaclean"|"matitaclean.opt"|"matitaclean.opt.static"->Matitaclean.main() |"matitamake" |"matitamake.opt" |"matitamake.opt.static" ->Matitamake.main() |"matitaprover"|"matitaprover.opt" - |"matitaprover.opt.static"->Matitaprover.main() + |"matitaprover.opt.static" ->Matitaprover.main() + |"matitawiki"|"matitawiki.opt" ->MatitaWiki.main() | _ -> (* let _ = Paramodulation.Saturation.init () in *) -- 2.39.2