1 (* Copyright (C) 2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
34 let out_comment och s =
35 let s = if s <> "" && s.[0] = '*' then "#" ^ s else s in
36 Printf.fprintf och "%s%s%s\n\n" "(*" s "*)"
38 let out_line_comment och s =
39 let l = 70 - String.length s in
40 let s = Printf.sprintf " %s %s" s (String.make l '*') in
43 let out_preamble och (path, lines) =
44 let ich = open_in path in
47 let s = input_line ich in
48 begin Printf.fprintf och "%s\n" s; print (pred i) end
51 out_line_comment och "This file was automatically generated: do not edit"
55 let pp_ast_statement st =
56 GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
57 ~map_unicode_to_tex:(Helm_registry.get_bool
58 "matita.paste_unicode_as_tex")
59 ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) st
62 Helm_registry.set_bool "matita.moo" false;
63 let floc = H.dummy_floc in
64 let nl_ast = G.Comment (floc, G.Note (floc, "")) in
65 let och = open_out f in
66 let atexit () = close_out och in
67 let nl () = output_string och (pp_ast_statement nl_ast) in
68 let rt_base_dir = Filename.dirname Sys.argv.(0) in
69 let path = Filename.concat rt_base_dir "matita.ma.templ" in
71 out_preamble och (path, lines);
72 let grafite_parser_cb fname =
73 let ast = G.Executable (floc, G.Command (floc, G.Include (floc, fname))) in
74 output_string och (pp_ast_statement ast); nl (); nl ()
76 let matita_engine_cb = function
77 | G.Executable (_, G.Macro (_, G.Inline _))
78 | G.Executable (_, G.Command (_, G.Include _)) -> ()
80 output_string och (pp_ast_statement ast); nl (); nl ()
82 let matitac_lib_cb = output_string och in
83 GrafiteParser.set_callback grafite_parser_cb;
84 MatitaEngine.set_callback matita_engine_cb;
85 MatitacLib.set_callback matitac_lib_cb;
89 (* compiler ala pascal/java using make *)
90 let main_compiler () =
91 MatitaInit.initialize_all ();
92 (* targets and deps *)
93 let targets = Helm_registry.get_list Helm_registry.string "matita.args" in
97 (match Librarian.find_roots_in_dir (Sys.getcwd ()) with
99 Make.load_deps_file (Filename.dirname x ^ "/depends")
101 HLog.error "No targets and no root found"; exit 1
103 HLog.error ("Too many roots found, move into one and retry: "^
104 String.concat ", " roots);exit 1);
106 let root, _, _ = Librarian.baseuri_of_script hd in
107 Make.load_deps_file (root ^ "/depends")
109 (* must be called after init since args are set by cmdline parsing *)
110 let system_mode = Helm_registry.get_bool "matita.system" in
111 if system_mode then HLog.message "Compiling in system space";
112 if not (Helm_registry.get_bool "matita.verbose") then MatitaMisc.shutup ();
116 type source_object = string
117 type target_object = string
118 let string_of_source_object s = s;;
119 let string_of_target_object s = s;;
121 let target_of mafile =
122 let _,baseuri,_ = Librarian.baseuri_of_script mafile in
123 LibraryMisc.obj_file_of_baseuri
124 ~must_exist:false ~baseuri ~writable:true
127 let mtime_of_source_object s =
128 try Some (Unix.stat s).Unix.st_mtime
129 with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s ->
130 raise (Failure ("Unable to stat a source file: " ^ s))
133 let mtime_of_target_object s =
134 try Some (Unix.stat s).Unix.st_mtime
135 with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> None
140 Helm_registry.get_opt
141 Helm_registry.string "matita.filename"
143 let rc = MatitacLib.compile fname in
145 | Some n -> Helm_registry.set_string "matita.filename" n;
146 | _ -> Helm_registry.unset "matita.filename");
151 let module Make = Make.Make(F) in
152 Make.make deps targets
156 Helm_registry.set_bool "matita.moo" true;
157 match Filename.basename Sys.argv.(0) with
158 |"gragrep" |"gragrep.opt" |"gragrep.opt.static" ->Gragrep.main()
159 |"matitadep" |"matitadep.opt" |"matitadep.opt.static" ->Matitadep.main()
160 |"matitaclean"|"matitaclean.opt"|"matitaclean.opt.static"->Matitaclean.main()
161 |"matitamake" |"matitamake.opt" |"matitamake.opt.static" ->Matitamake.main()
162 |"matitaprover"|"matitaprover.opt"
163 |"matitaprover.opt.static" ->Matitaprover.main()
164 |"matitawiki"|"matitawiki.opt" ->MatitaWiki.main()
166 let dump_msg = "<filename> Dump with expanded macros to <filename>" in
167 MatitaInit.add_cmdline_spec ["-dump", Arg.String dump, dump_msg];