]> matita.cs.unibo.it Git - helm.git/commitdiff
Just a few lines test to understand with Cezary Kalinsky how much effort is
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 20 Jan 2007 16:20:16 +0000 (16:20 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 20 Jan 2007 16:20:16 +0000 (16:20 +0000)
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
helm/software/matita/matitaWiki.ml [new file with mode: 0644]
helm/software/matita/matitac.ml

index c0e31d64315558d6709e900a60e58f7429f9aed7..ed5ebb320869dfc1329ce4b5839a75ac83d0f928 100644 (file)
@@ -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 (file)
index 0000000..3beadf1
--- /dev/null
@@ -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)
index b4a3119e00f799d1a1f55fbf6b7499f356552347..2249998e9c09d06c8b1534aaeb0524a27ba5db04 100644 (file)
@@ -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  *)