let uri = deref_index_theory uri in
Http_getter_storage.exists (uri ^ xml_suffix)
+let is_an_obj s =
+ try
+ s <> UriManager.buri_of_uri (UriManager.uri_of_string s)
+ with UriManager.IllFormedUri _ -> false
+
let resolve ~writable uri =
if remote () then
resolve_remote ~writable uri
else
let uri = deref_index_theory uri in
try
- Http_getter_storage.resolve ~writable (uri ^ xml_suffix)
+ if is_an_obj uri then
+ Http_getter_storage.resolve ~writable (uri ^ xml_suffix)
+ else
+ Http_getter_storage.resolve ~writable uri
with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri)
let filename ~writable uri =
with Resource_not_found _ -> false
let resolve ?(must_exists=true) ~writable =
- dispatch_single
+ (if must_exists then
+ dispatch_multi
+ else
+ dispatch_single)
{ write = writable;
name="resolve";
exists = must_exists;
GrafiteTypes.add_moo_content [cmd] status,[]
| GrafiteAst.Include (loc, baseuri) ->
let moopath_rw, moopath_r =
- LibraryMisc.obj_file_of_baseuri ~baseuri ~writable:true,
- LibraryMisc.obj_file_of_baseuri ~baseuri ~writable:false
+ LibraryMisc.obj_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:true,
+ LibraryMisc.obj_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:false
in
let moopath =
if Sys.file_exists moopath_r then moopath_r else
LibraryClean.clean_baseuris [value];
assert (Http_getter_storage.is_empty value);
end;
+ HExtlib.mkdir
+ (Filename.dirname (Http_getter.filename ~writable:true (value ^
+ "/foo.con")));
end;
GrafiteTypes.set_option status name value,[]
| GrafiteAst.Drop loc -> raise Drop
match cmd with
| LexiconAst.Include (loc, baseuri) ->
let lexiconpath_rw, lexiconpath_r =
- LibraryMisc.lexicon_file_of_baseuri ~writable:true ~baseuri,
- LibraryMisc.lexicon_file_of_baseuri ~writable:false ~baseuri
+ LibraryMisc.lexicon_file_of_baseuri
+ ~must_exist:false ~writable:true ~baseuri,
+ LibraryMisc.lexicon_file_of_baseuri
+ ~must_exist:false ~writable:false ~baseuri
in
let lexiconpath =
if Sys.file_exists lexiconpath_rw then lexiconpath_rw else
let status = List.fold_left eval_command status lexicon in
if Helm_registry.get_bool "db.nodb" then
let metadatapath_rw, metadatapath_r =
- LibraryMisc.metadata_file_of_baseuri ~baseuri ~writable:true,
- LibraryMisc.metadata_file_of_baseuri ~baseuri ~writable:false
+ LibraryMisc.metadata_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:true,
+ LibraryMisc.metadata_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:false
in
let metadatapath =
if Sys.file_exists metadatapath_rw then metadatapath_rw else
(fun baseuri ->
try
HExtlib.safe_remove
- (LibraryMisc.obj_file_of_baseuri ~writable:true ~baseuri);
+ (LibraryMisc.obj_file_of_baseuri
+ ~must_exist:false ~writable:true ~baseuri);
HExtlib.safe_remove
- (LibraryMisc.metadata_file_of_baseuri ~writable:true ~baseuri);
+ (LibraryMisc.metadata_file_of_baseuri
+ ~must_exist:false ~writable:true ~baseuri);
HExtlib.safe_remove
- (LibraryMisc.lexicon_file_of_baseuri ~writable:true ~baseuri)
+ (LibraryMisc.lexicon_file_of_baseuri
+ ~must_exist:false ~writable:true ~baseuri)
with Http_getter_types.Key_not_found _ -> ())
(HExtlib.list_uniq (List.fast_sort Pervasives.compare
(List.map (UriManager.buri_of_uri) l)));
(* $Id$ *)
-let resolve ~writable baseuri = Http_getter.filename ~writable baseuri
+let resolve ~must_exist ~writable baseuri =
+ if must_exist then
+ Http_getter.resolve ~writable baseuri
+ else
+ Http_getter.filename ~writable baseuri
-let obj_file_of_baseuri ~writable ~baseuri =
- resolve ~writable baseuri ^ ".moo"
-let lexicon_file_of_baseuri ~writable ~baseuri =
- resolve ~writable baseuri ^ ".lexicon"
-let metadata_file_of_baseuri~writable ~baseuri =
- resolve ~writable baseuri ^ ".metadata"
+let obj_file_of_baseuri ~must_exist ~writable ~baseuri =
+ resolve ~must_exist ~writable baseuri ^ ".moo"
+let lexicon_file_of_baseuri ~must_exist ~writable ~baseuri =
+ resolve ~must_exist ~writable baseuri ^ ".lexicon"
+let metadata_file_of_baseuri~must_exist ~writable ~baseuri =
+ resolve ~must_exist ~writable baseuri ^ ".metadata"
* http://helm.cs.unibo.it/
*)
-val obj_file_of_baseuri: writable:bool -> baseuri:string -> string
-val lexicon_file_of_baseuri: writable:bool -> baseuri:string -> string
-val metadata_file_of_baseuri: writable:bool -> baseuri:string -> string
+val obj_file_of_baseuri:
+ must_exist:bool -> writable:bool -> baseuri:string -> string
+val lexicon_file_of_baseuri:
+ must_exist:bool -> writable:bool -> baseuri:string -> string
+val metadata_file_of_baseuri:
+ must_exist:bool -> writable:bool -> baseuri:string -> string
let closed_xml = runtime_base_dir ^ "/closed.xml"
let gtkmathview_conf = runtime_base_dir ^ "/gtkmathview.matita.conf.xml"
let matitamake_makefile_template = runtime_base_dir ^ "/template_makefile.in"
+let matitamake_makefile_template_devel =
+ runtime_base_dir ^ "/template_makefile_devel.in"
let stdlib_dir_devel = runtime_base_dir ^ "/library"
let stdlib_dir_installed = runtime_base_dir ^ "/ma/standard-library"
let help_dir = runtime_base_dir ^ "/help"
(* $Id$ *)
-val base_uri : string
-val blank_uri : string
-val browser_history_size : int
-val closed_xml : string
-val console_history_size : int
-val core_notation_script : string
-val current_proof_uri : string
-val debug : bool
-val default_font_size : int
-val gtkmathview_conf : string
-val gtkrc_file : string
-val help_dir : string
-val images_dir : string
-val lang_file : string
-val matita_conf : string
-val matitamake_makefile_template : string
-val phrase_sep : string
-val runtime_base_dir : string
-val script_font : string
-val script_template : string
-val stdlib_dir_devel : string
-val stdlib_dir_installed : string
-val undo_history_size : int
-val version : string
+val base_uri : string
+val blank_uri : string
+val browser_history_size : int
+val closed_xml : string
+val console_history_size : int
+val core_notation_script : string
+val current_proof_uri : string
+val debug : bool
+val default_font_size : int
+val gtkmathview_conf : string
+val gtkrc_file : string
+val help_dir : string
+val images_dir : string
+val lang_file : string
+val matita_conf : string
+val matitamake_makefile_template : string
+val matitamake_makefile_template_devel : string
+val phrase_sep : string
+val runtime_base_dir : string
+val script_font : string
+val script_template : string
+val stdlib_dir_devel : string
+val stdlib_dir_installed : string
+val undo_history_size : int
+val version : string
+++ /dev/null
-SRC=$(shell find . -name "*.ma" -a -type f)
-
-MATITA_FLAGS = -I ../..
-NODB=false
-ifeq ($(NODB),true)
- MATITA_FLAGS += -nodb
-endif
-
-MATITAC=../../scripts/do_tests.sh $(DO_TESTS_OPTS) "../../matitac $(MATITA_FLAGS)" "../../matitaclean $(MATITA_FLAGS)" /dev/null OK
-MATITACOPT=../../scripts/do_tests.sh $(DO_TESTS_OPTS) "../../matitac.opt $(MATITA_FLAGS)" "../../matitaclean.opt $(MATITA_FLAGS)" /dev/null OK
-VERBOSEMATITAC=../../matitac $(MATITA_FLAGS)
-VERBOSEMATITACOPT=../../matitac.opt $(MATITA_FLAGS)
-
-MATITACLEAN=../../matitaclean $(MATITA_FLAGS)
-MATITACLEANOPT=../../matitaclean.opt $(MATITA_FLAGS)
-
-MATITADEP=../../matitadep $(MATITA_FLAGS)
-MATITADEPOPT=../../matitadep.opt $(MATITA_FLAGS)
-
-DEPEND_NAME=.depend
-
-H=@
-
-all: $(SRC:%.ma=%.mo)
-
-opt:
- $(H)$(MAKE) MATITAC='$(MATITACOPT)' MATITACLEAN='$(MATITACLEANOPT)' MATITADEP='$(MATITADEPOPT)' all
-
-verbose:
- $(H)$(MAKE) MATITAC='$(VERBOSEMATITAC)' MATITACLEAN='$(MATITACLEAN)' MATITADEP='$(MATITADEP)' all
-
-%.opt:
- $(H)$(MAKE) MATITAC='$(MATITACOPT)' MATITACLEAN='$(MATITACLEANOPT)' MATITADEP='$(MATITADEPOPT)' $(@:%.opt=%)
-
-clean_:
- $(H)rm -f __*not_for_matita
-
-clean: clean_
- $(H)$(MATITACLEAN) $(SRC)
-
-cleanall: clean_
- $(H)rm -f $(SRC:%.ma=%.moo)
- $(H)$(MATITACLEAN) all
-
-depend:
- $(H)rm -f $(DEPEND_NAME)
- $(H)$(MAKE) $(DEPEND_NAME)
-.PHONY: depend
-
-%.moo:
- $(H)$(MATITAC) $<
-
-$(DEPEND_NAME): $(SRC)
- $(H)$(MATITADEP) $(SRC) > $@ || rm -f $@
-
-#include $(DEPEND_NAME)
-include .depend
--- /dev/null
+H=@
+
+RT_BASEDIR=../../
+OPTIONS=-bench
+MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS)
+CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS)
+MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS)
+CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS)
+
+devel:=$(shell basename `pwd`)
+
+all: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel)
+clean: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel)
+cleanall: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all
+
+all.opt opt: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel)
+clean.opt: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel)
+cleanall.opt: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all
+
+%.mo: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
+%.mo.opt: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@
+
+preall:
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)
+
+++ /dev/null
-SRC=$(shell find . -name "*.ma" -a -type f)
-
-MATITA_FLAGS = -I ../..
-NODB=false
-ifeq ($(NODB),true)
- MATITA_FLAGS += -nodb
-endif
-
-MATITAC=../../scripts/do_tests.sh $(DO_TESTS_OPTS) "../../matitac $(MATITA_FLAGS)" "../../matitaclean $(MATITA_FLAGS)" /dev/null OK
-MATITACOPT=../../scripts/do_tests.sh $(DO_TESTS_OPTS) "../../matitac.opt $(MATITA_FLAGS)" "../../matitaclean.opt $(MATITA_FLAGS)" /dev/null OK
-VERBOSEMATITAC=../../matitac $(MATITA_FLAGS)
-VERBOSEMATITACOPT=../../matitac.opt $(MATITA_FLAGS)
-
-MATITACLEAN=../../matitaclean $(MATITA_FLAGS)
-MATITACLEANOPT=../../matitaclean.opt $(MATITA_FLAGS)
-
-MATITADEP=../../matitadep $(MATITA_FLAGS)
-MATITADEPOPT=../../matitadep.opt $(MATITA_FLAGS)
-
-DEPEND_NAME=.depend
-
-H=@
-
-all: $(SRC:%.ma=%.mo)
-
-opt:
- $(H)$(MAKE) MATITAC='$(MATITACOPT)' MATITACLEAN='$(MATITACLEANOPT)' MATITADEP='$(MATITADEPOPT)' all
-
-verbose:
- $(H)$(MAKE) MATITAC='$(VERBOSEMATITAC)' MATITACLEAN='$(MATITACLEAN)' MATITADEP='$(MATITADEP)' all
-
-%.opt:
- $(H)$(MAKE) MATITAC='$(MATITACOPT)' MATITACLEAN='$(MATITACLEANOPT)' MATITADEP='$(MATITADEPOPT)' $(@:%.opt=%)
-
-clean_:
- $(H)rm -f __*not_for_matita
-
-clean: clean_
- $(H)$(MATITACLEAN) $(SRC)
-
-cleanall: clean_
- $(H)rm -f $(SRC:%.ma=%.moo)
- $(H)$(MATITACLEAN) all
-
-depend:
- $(H)rm -f $(DEPEND_NAME)
- $(H)$(MAKE) $(DEPEND_NAME)
-.PHONY: depend
-
-%.moo:
- $(H)$(MATITAC) $<
-
-$(DEPEND_NAME): $(SRC)
- $(H)$(MATITADEP) $(SRC) > $@ || rm -f $@
-
-#include $(DEPEND_NAME)
-include .depend
--- /dev/null
+H=@
+
+RT_BASEDIR=../../
+OPTIONS=-bench
+MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS)
+CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS)
+MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS)
+CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS)
+
+devel:=$(shell basename `pwd`)
+
+all: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel)
+clean: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel)
+cleanall: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all
+
+all.opt opt: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel)
+clean.opt: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel)
+cleanall.opt: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all
+
+%.mo: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
+%.mo.opt: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@
+
+preall:
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)
+
+++ /dev/null
-SRC=$(shell find . -name "*.ma" -a -type f)
-
-MATITA_FLAGS =
-NODB=false
-ifeq ($(NODB),true)
- MATITA_FLAGS += -nodb
-endif
-
-MATITAC=../scripts/do_tests.sh $(DO_TESTS_OPTS) "../matitac $(MATITA_FLAGS)" "../matitaclean $(MATITA_FLAGS)" /dev/null OK
-MATITACOPT=../scripts/do_tests.sh $(DO_TESTS_OPTS) "../matitac.opt $(MATITA_FLAGS)" "../matitaclean.opt $(MATITA_FLAGS)" /dev/null OK
-VERBOSEMATITAC=../matitac $(MATITA_FLAGS)
-VERBOSEMATITACOPT=../matitac.opt $(MATITA_FLAGS)
-
-MATITACLEAN=../matitaclean $(MATITA_FLAGS)
-MATITACLEANOPT=../matitaclean.opt $(MATITA_FLAGS)
-
-MATITADEP=../matitadep $(MATITA_FLAGS)
-MATITADEPOPT=../matitadep.opt $(MATITA_FLAGS)
-
-DEPEND_NAME=.depend
-
-H=@
-
-all: $(SRC:%.ma=%.mo)
-
-opt:
- $(H)$(MAKE) MATITAC='$(MATITACOPT)' MATITACLEAN='$(MATITACLEANOPT)' MATITADEP='$(MATITADEPOPT)' all
-
-verbose:
- $(H)$(MAKE) MATITAC='$(VERBOSEMATITAC)' MATITACLEAN='$(MATITACLEAN)' MATITADEP='$(MATITADEP)' all
-
-%.opt:
- $(H)$(MAKE) MATITAC='$(MATITACOPT)' MATITACLEAN='$(MATITACLEANOPT)' MATITADEP='$(MATITADEPOPT)' $(@:%.opt=%)
-
-clean_:
- $(H)rm -f __*not_for_matita
-
-clean: clean_
- $(H)$(MATITACLEAN) $(SRC)
-
-cleanall:
- $(H)rm -f $(SRC:%.ma=%.moo)
- $(H)$(MATITACLEAN) all
-
-depend:
- $(H)rm -f $(DEPEND_NAME)
- $(H)$(MAKE) $(DEPEND_NAME)
-.PHONY: depend
-
-%.moo:
- $(H)$(MATITAC) $<
-
-$(DEPEND_NAME): $(SRC)
- $(H)$(MATITADEP) $(SRC) > $@ || rm -f $@
-
-#include $(DEPEND_NAME)
-include .depend
</key>
<key name="prefix">
cic:/
- file://@RT_BASE_DIR@/legacy-library/coq/
+ file://@RT_BASE_DIR@/xml/legacy-library/coq/
+ legacy
+ </key>
+ <key name="prefix">
+ cic:/
+ file:///projects/helm/library/coq_contribs/
legacy
</key>
</section>
let ask_and_save_moo_if_needed parent fname lexicon_status grafite_status =
let baseuri = DependenciesParser.baseuri_of_script ~include_paths:[] fname in
- let moo_fname = LibraryMisc.obj_file_of_baseuri ~baseuri ~writable:true in
+ let moo_fname =
+ LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri ~writable:true in
let save () =
let metadata_fname =
- LibraryMisc.metadata_file_of_baseuri ~baseuri ~writable:true in
+ LibraryMisc.metadata_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:true in
let lexicon_fname =
- LibraryMisc.lexicon_file_of_baseuri ~baseuri ~writable:true
+ LibraryMisc.lexicon_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:true
in
GrafiteMarshal.save_moo moo_fname
grafite_status.GrafiteTypes.moo_content_rev;
let parse_cmdline init_status =
if not (already_configured [CmdLine] init_status) then begin
let includes = ref [
- BuildTimeConf.stdlib_dir_installed ;
- BuildTimeConf.stdlib_dir_devel ]
+ BuildTimeConf.stdlib_dir_devel;
+ BuildTimeConf.stdlib_dir_installed ; ]
in
let args = ref [] in
let add_l l = fun s -> l := s :: !l in
in
Arg.parse arg_spec (add_l args) (usage ());
set_list ~key:"matita.includes" includes;
+ args := List.filter (fun x -> x <> "") !args;
set_list ~key:"matita.args" args;
HExtlib.set_profiling_printings
(fun () -> Helm_registry.get_bool "matita.profile");
raise exn
let fname () =
- match Helm_registry.get_list Helm_registry.string "matita.args" with
+ let rec aux = function
+ | ""::tl -> aux tl
| [x] -> x
+ | [] -> MatitaInit.die_usage ()
| l ->
- prerr_endline ("Wrong commands: " ^ String.concat " " l);
+ prerr_endline
+ ("Wrong commands: " ^
+ String.concat " " (List.map (fun x -> "'" ^ x ^ "'") l));
MatitaInit.die_usage ()
+ in
+ aux (Helm_registry.get_list Helm_registry.string "matita.args")
let pp_ocaml_mode () =
HLog.message "";
assert (fnamelen > rootlen);
String.sub fname rootlen (fnamelen - rootlen)
in
- let s =
- Printf.sprintf "%s %-35s %-4s %s %s" cc fname rc times extra
+ let fname =
+ if fname.[0] = '/' then
+ String.sub fname 1 (String.length fname - 1)
+ else
+ fname
in
+ let s = Printf.sprintf "%s %-35s %-4s %s %s" cc fname rc times extra in
print_endline s;
flush stdout
end
let baseuri =
DependenciesParser.baseuri_of_script ~include_paths fname in
let moo_fname =
- LibraryMisc.obj_file_of_baseuri ~baseuri ~writable:true
+ LibraryMisc.obj_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:true
in
let lexicon_fname=
- LibraryMisc.lexicon_file_of_baseuri ~baseuri ~writable:true
+ LibraryMisc.lexicon_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:true
in
let metadata_fname =
- LibraryMisc.metadata_file_of_baseuri ~baseuri ~writable:true
+ 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;
module GA = GrafiteAst
module U = UriManager
+
+let obj_file_of_baseuri writable baseuri =
+ try
+ LibraryMisc.obj_file_of_baseuri
+ ~must_exist:true ~baseuri ~writable
+ with
+ | Http_getter_types.Unresolvable_URI _
+ | Http_getter_types.Key_not_found _ ->
+ LibraryMisc.obj_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:true
+;;
let main () =
(* all are maps from "file" to "something" *)
List.iter
(fun ma_file ->
let ic = open_in ma_file in
- let istream = Ulexing.from_utf8_channel ic in
- let dependencies = DependenciesParser.parse_dependencies istream in
+ let istream = Ulexing.from_utf8_channel ic in
+ let dependencies = DependenciesParser.parse_dependencies istream in
close_in ic;
List.iter
(function
let baseuri =
DependenciesParser.baseuri_of_script ~include_paths path in
if not (Http_getter_storage.is_legacy baseuri) then
- let moo_file =
- LibraryMisc.obj_file_of_baseuri ~baseuri ~writable:false in
+ let moo_file = obj_file_of_baseuri false baseuri in
Hashtbl.add include_deps ma_file moo_file
with Sys_error _ ->
HLog.warn
match dep with
| None -> ()
| Some u ->
- Hashtbl.add include_deps file
- (LibraryMisc.obj_file_of_baseuri ~baseuri:u ~writable:false))
+ Hashtbl.add include_deps file (obj_file_of_baseuri false u))
uri_deps;
List.iter
(fun ma_file ->
let deps = HExtlib.list_uniq deps in
let deps = ma_file :: deps in
let baseuri = Hashtbl.find baseuri_of ma_file in
- let moo = LibraryMisc.obj_file_of_baseuri ~baseuri ~writable:false in
- Printf.printf "%s: %s\n" moo (String.concat " " deps);
- Printf.printf "%s: %s\n" (Pcre.replace ~pat:"ma$" ~templ:"mo" ma_file) moo)
+ let moo = obj_file_of_baseuri true baseuri in
+ Printf.printf "%s: %s\n%s: %s\n%s: %s\n" moo (String.concat " " deps)
+ (Filename.basename (Pcre.replace ~pat:"ma$" ~templ:"mo" ma_file)) moo
+ (Pcre.replace ~pat:"ma$" ~templ:"mo" ma_file) moo)
(Helm_registry.get_list Helm_registry.string "matita.args")
let template = Pcre.replace ~pat:"@CLEAN@" ~templ:rm template in
HExtlib.output_file ~filename:makefilepath ~text:template
+let rebuild_makefile_devel development =
+ let path = development.root ^ "/makefile" in
+ if not (Sys.file_exists path) then
+ begin
+ let template =
+ HExtlib.input_file BuildTimeConf.matitamake_makefile_template_devel
+ in
+ let template =
+ Pcre.replace ~pat:"@MATITA_RT_BASE_DIR@"
+ ~templ:BuildTimeConf.runtime_base_dir template
+ in
+ HExtlib.output_file ~filename:path ~text:template
+ end
+
(* creates a new development if possible *)
let initialize_development name dir =
let name = Pcre.replace ~pat:" " ~templ:"_" name in
let dev = {name = name ; root = dir} in
- match development_for_dir dir with
- | Some dev ->
- if dir <> dev.root then begin
- logger `Error
- (sprintf ("Dir \"%s\" is already handled by development \"%s\"\n"
- ^^ "Development \"%s\" is rooted in \"%s\"\n"
- ^^ "Dir \"%s\" is a sub-dir of \"%s\"")
- dir dev.name dev.name dev.root dir dev.root);
- None
- end else (* requirement development alreay exists, do nothing *)
- Some dev
- | None ->
- dump_development dev;
- rebuild_makefile dev;
- developments := dev :: !developments;
- Some dev
+ dump_development dev;
+ rebuild_makefile dev;
+ rebuild_makefile_devel dev;
+ developments := dev :: !developments;
+ Some dev
let make chdir args =
let old = Unix.getcwd () in
let args =
["--no-print-directory"; "-s"; "-k"; "-f"; makefile; target] @ flags
in
+(* prerr_endline (String.concat " " args); *)
make development.root args
let build_development ?matita_flags ?(target="all") development =
let pid = ref ~-1 in
ignore(Sys.signal Sys.sigchld (Sys.Signal_ignore));
try
+(* prerr_endline (String.concat " " args); *)
let argv = Array.of_list ("make"::args) in
pid := Unix.create_process "make" argv Unix.stdin out_w err_w;
Unix.close out_w;
rm -f $(TODO)
%.moo:
- $(MATITAC) $(MATITA_FLAGS) -q -I @ROOT@ $<
+ if [ -z "$<" ]; then \
+ echo "missing dependencies for $@"; \
+ else \
+ $(MATITAC) $(MATITA_FLAGS) -q -I @ROOT@ $<; \
+ fi
@DEPFILE@ : $(SRC)
$(MATITADEP) $(MATITA_FLAGS) -I '@ROOT@' $^ 1> @DEPFILE@
--- /dev/null
+H=@
+
+RT_BASEDIR=@MATITA_RT_BASE_DIR@/
+OPTIONS=-bench
+MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS)
+CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS)
+MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS)
+CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS)
+
+devel:=$(shell basename `pwd`)
+
+all: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel)
+clean: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel)
+cleanall: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all
+
+all.opt opt: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel)
+clean.opt: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel)
+cleanall.opt: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all
+
+%.mo: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
+%.mo.opt: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@
+
+preall:
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)
+
+++ /dev/null
-SRC=$(wildcard *.ma)
-
-MATITA_FLAGS = -I ..
-NODB=false
-ifeq ($(NODB),true)
- MATITA_FLAGS += -nodb
-endif
-
-MATITAC=../scripts/do_tests.sh $(DO_TESTS_OPTS) "../matitac $(MATITA_FLAGS)" "../matitaclean $(MATITA_FLAGS)" /dev/null OK
-MATITACOPT=../scripts/do_tests.sh $(DO_TESTS_OPTS) "../matitac.opt $(MATITA_FLAGS)" "../matitaclean.opt $(MATITA_FLAGS)" /dev/null OK
-VERBOSEMATITAC=../matitac $(MATITA_FLAGS)
-VERBOSEMATITACOPT=../matitac.opt $(MATITA_FLAGS)
-
-MATITACLEAN=../matitaclean $(MATITA_FLAGS)
-MATITACLEANOPT=../matitaclean.opt $(MATITA_FLAGS)
-
-MATITADEP=../matitadep $(MATITA_FLAGS)
-MATITADEPOPT=../matitadep.opt $(MATITA_FLAGS)
-
-DEPEND_NAME=.depend
-
-H=@
-
-all: $(SRC:%.ma=%.mo)
-
-opt:
- $(H)$(MAKE) MATITAC='$(MATITACOPT)' MATITACLEAN='$(MATITACLEANOPT)' MATITADEP='$(MATITADEPOPT)' all
-
-verbose:
- $(H)$(MAKE) MATITAC='$(VERBOSEMATITAC)' MATITACLEAN='$(MATITACLEAN)' MATITADEP='$(MATITADEP)' all
-
-%.opt:
- $(H)$(MAKE) MATITAC='$(MATITACOPT)' MATITACLEAN='$(MATITACLEANOPT)' MATITADEP='$(MATITADEPOPT)' $(@:%.opt=%)
-
-clean_:
- $(H)rm -f __*not_for_matita
-
-clean: clean_
- $(H)$(MATITACLEAN) $(SRC)
-
-cleanall: clean_
- $(H)rm -f $(SRC:%.ma=%.moo)
- $(H)$(MATITACLEAN) all
-
-depend:
- $(H)rm -f $(DEPEND_NAME)
- $(H)$(MAKE) $(DEPEND_NAME)
-.PHONY: depend
-
-%.moo:
- $(H)$(MATITAC) $<
-
-$(DEPEND_NAME): $(SRC)
- $(H)$(MATITADEP) $(SRC) > $@ || rm -f $@
-
-#include $(DEPEND_NAME)
-include .depend
--- /dev/null
+H=@
+
+RT_BASEDIR=../
+OPTIONS=-bench
+MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS)
+CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS)
+MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS)
+CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS)
+
+devel:=$(shell basename `pwd`)
+
+all: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel)
+clean: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel)
+cleanall: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all
+
+all.opt opt: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel)
+clean.opt: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel)
+cleanall.opt: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all
+
+%.mo: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
+%.mo.opt: preall
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@
+
+preall:
+ $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)
+
projects / helm.git / commitdiff