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
matitaExcPp.cmo \
matitaEngine.cmo \
matitacLib.cmo \
+ applyTransformation.cmo \
+ matitaWiki.cmo \
matitaprover.cmo \
$(NULL)
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
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
$(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
--- /dev/null
+(* 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)
projects / helm.git / commitdiff