From ebc063e65d908c9f35619c92454dbbe76bdabd40 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 1 Jul 2005 14:40:19 +0000 Subject: [PATCH] first snapshot of separate compilation --- helm/matita/Makefile.in | 3 +- helm/matita/Makefile.tests | 40 +++++++++++ helm/matita/matita.lang | 1 + helm/matita/matitaDb.ml | 11 +++ helm/matita/matitaDb.mli | 1 + helm/matita/matitaSync.ml | 31 +++++++-- helm/matita/matitaSync.mli | 4 +- helm/matita/matitacLib.ml | 2 + helm/matita/matitaclean.ml | 96 +++++++++++++++++--------- helm/matita/matitadep.ml | 32 +++++---- helm/matita/tests/apply.ma | 2 +- helm/matita/tests/auto.ma | 2 +- helm/matita/tests/baseuri.ma | 4 +- helm/matita/tests/coercions.ma | 2 +- helm/matita/tests/comments.ma | 2 +- helm/matita/tests/fguidi.ma | 2 +- helm/matita/tests/first.ma | 25 +++++++ helm/matita/tests/fix_betareduction.ma | 2 +- helm/matita/tests/inversion.ma | 2 +- helm/matita/tests/letrec.ma | 2 +- helm/matita/tests/match.ma | 2 +- helm/matita/tests/match_inference.ma | 2 +- helm/matita/tests/mysql_escaping.ma | 2 +- helm/matita/tests/record.ma | 2 +- helm/matita/tests/rewrite.ma | 2 +- helm/matita/tests/second.ma | 10 +++ helm/matita/tests/simpl.ma | 2 +- helm/matita/tests/test2.ma | 2 +- helm/matita/tests/test3.ma | 2 +- helm/matita/tests/test4.ma | 2 +- helm/matita/tests/third.ma | 10 +++ 31 files changed, 234 insertions(+), 70 deletions(-) create mode 100644 helm/matita/Makefile.tests create mode 100644 helm/matita/tests/first.ma create mode 100644 helm/matita/tests/second.ma create mode 100644 helm/matita/tests/third.ma diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index 168dfa305..bed070a51 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -107,7 +107,8 @@ clean: rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o \ matita matita.opt matitac matitac.opt \ cicbrowser cicbrowser.opt \ - matitadep matitadep.opt + matitadep matitadep.opt \ + matitaclean matitaclean.opt distclean: clean rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli rm -f config.log config.status Makefile buildTimeConf.ml diff --git a/helm/matita/Makefile.tests b/helm/matita/Makefile.tests new file mode 100644 index 000000000..cab67026a --- /dev/null +++ b/helm/matita/Makefile.tests @@ -0,0 +1,40 @@ +TODO=\ + tests/apply.moo\ + tests/auto.moo\ + tests/baseuri.moo\ + tests/coercions.moo\ + tests/comments.moo\ + tests/fguidi.moo\ + tests/first.moo\ + tests/fix_betareduction.moo\ + tests/inversion.moo\ + tests/letrec.moo\ + tests/match.moo\ + tests/match_inference.moo\ + tests/mysql_escaping.moo\ + tests/record.moo\ + tests/replace.moo\ + tests/rewrite.moo\ + tests/second.moo\ + tests/simpl.moo\ + tests/test2.moo\ + tests/test3.moo\ + tests/test4.moo\ + tests/third.moo + +DEPEND_NAME=.depend.moo + +all: $(TODO) + +clean: + rm -f $(DEPEND_NAME) $(TODO) + ./matitaclean all + +%.moo:%.ma + [ ! -e $@ ] || ./matitaclean $< + ./matitac $< || ./matitaclean $< + +$(DEPEND_NAME): $(TODO:%.moo=%.ma) + ./matitadep $^ > $@ + +include $(DEPEND_NAME) diff --git a/helm/matita/matita.lang b/helm/matita/matita.lang index 439440710..f74da76e7 100644 --- a/helm/matita/matita.lang +++ b/helm/matita/matita.lang @@ -28,6 +28,7 @@ coinductive corec in + on inductive let match diff --git a/helm/matita/matitaDb.ml b/helm/matita/matitaDb.ml index c5bdbf84b..17aac3745 100644 --- a/helm/matita/matitaDb.ml +++ b/helm/matita/matitaDb.ml @@ -150,3 +150,14 @@ let remove_uri uri = with exn -> raise exn (* no errors should be accepted *) +let xpointers_of_ind uri = + let dbd = instance () in + let name_tbl = MetadataTypes.name_tbl () in + let query = sprintf + "SELECT source FROM %s WHERE source LIKE '%s#xpointer%%'" name_tbl + (Mysql.escape (UriManager.string_of_uri uri)) + in + let rc = Mysql.exec dbd query in + let l = ref [] in + Mysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l); + List.map UriManager.uri_of_string !l diff --git a/helm/matita/matitaDb.mli b/helm/matita/matitaDb.mli index 112b2d0b2..3b3bd58c1 100644 --- a/helm/matita/matitaDb.mli +++ b/helm/matita/matitaDb.mli @@ -29,3 +29,4 @@ val clean_owner_environment : unit -> unit val create_owner_environment : unit -> unit val remove_uri: UriManager.uri -> string list +val xpointers_of_ind: UriManager.uri -> UriManager.uri list diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 42e8f1c40..660be6c10 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -223,8 +223,31 @@ let alias_diff ~from status = status.aliases Map.empty let remove uri = - let path = Http_getter.resolve' uri in - remove_object_from_disk uri path; - remove_coercion uri; - ignore(MatitaDb.remove_uri uri) + let derived_uris_of_uri uri = + UriManager.innertypesuri_of_uri uri :: + UriManager.annuri_of_uri uri :: + (match UriManager.bodyuri_of_uri uri with + | None -> [] + | Some u -> [u]) + in + let to_remove = + uri :: + (if UriManager.uri_is_ind uri then MatitaDb.xpointers_of_ind uri else []) @ + derived_uris_of_uri uri + in + List.iter + (fun uri -> + (try + let path = + let path = Http_getter.resolve' (UriManager.strip_xpointer uri) in + assert (String.sub path 0 7 = "file://"); + String.sub path 7 (String.length path - 7) + in + remove_object_from_disk uri path; + with + Http_getter_types.Key_not_found _ -> Http_getter.unregister' uri); + remove_coercion uri; + ignore(MatitaDb.remove_uri uri)) + to_remove + diff --git a/helm/matita/matitaSync.mli b/helm/matita/matitaSync.mli index 0c866d4e5..376ba3794 100644 --- a/helm/matita/matitaSync.mli +++ b/helm/matita/matitaSync.mli @@ -36,6 +36,8 @@ val time_travel: val alias_diff: from:MatitaTypes.status -> MatitaTypes.status -> DisambiguateTypes.environment - (* removes the object from DB, Disk, CoercionsDB *) + (* removes the object from DB, Disk, CoercionsDB, getter + * asserts the uri is resolved to file:// so it is only for + * user's objects *) val remove: UriManager.uri -> unit diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index ea8888eb7..5f07aa406 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -103,8 +103,10 @@ let main ~mode = Helm_registry.load_from "matita.conf.xml"; Http_getter.init (); MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); +(* MatitaDb.clean_owner_environment (); MatitaDb.create_owner_environment (); +*) status := Some (ref (Lazy.force MatitaEngine.initial_status)); at_exit (fun () -> diff --git a/helm/matita/matitaclean.ml b/helm/matita/matitaclean.ml index 60292515a..eb0c5787d 100644 --- a/helm/matita/matitaclean.ml +++ b/helm/matita/matitaclean.ml @@ -1,6 +1,7 @@ module HGT = Http_getter_types;; module HG = Http_getter;; module UM = UriManager;; +module TA = TacticAst;; let _ = Helm_registry.load_from "matita.conf.xml"; @@ -13,34 +14,49 @@ let clean_all () = exit 0 let dbd = MatitaDb.instance () +let cache_of_processed_baseuri = Hashtbl.create 1024 let one_step_depend suri = - let dbg_q = - let suri = Mysql.escape suri in - (**** FIX FIX FIX ***) - (****** let obj_tbl = MetadataTypes.obj_tbl () in ******) - let obj_tbl = MetadataTypes.library_obj_tbl in - (**** FIX FIX FIX ***) - Printf.sprintf - "SELECT source FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl suri + let buri = + try + UM.buri_of_uri (UM.uri_of_string suri) + with UM.IllFormedUri _ -> suri in - try - let rc = Mysql.exec dbd dbg_q in - let l = ref [] in - Mysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l); - let l = List.sort Pervasives.compare !l in - MatitaMisc.list_uniq l - with - exn -> raise exn (* no errors should be accepted *) + if Hashtbl.mem cache_of_processed_baseuri buri then + [] + else + begin + Hashtbl.add cache_of_processed_baseuri buri true; + let query = + let buri = buri ^ "/" in + let buri = Mysql.escape buri in + let obj_tbl = MetadataTypes.obj_tbl () in + Printf.sprintf + "SELECT source FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl buri + in + try + let rc = Mysql.exec dbd query in + let l = ref [] in + Mysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l:=a:: !l); + let l = List.sort Pervasives.compare !l in + MatitaMisc.list_uniq l + with + exn -> raise exn (* no errors should be accepted *) + end -let cache_of_processed_baseuri = Hashtbl.create 1024 +let safe_buri_of_suri suri = + try + UM.buri_of_uri (UM.uri_of_string suri) + with + UM.IllFormedUri _ -> suri + let close_uri_list uri_to_remove = (* to remove an uri you have to remove the whole script *) let buri_to_remove = MatitaMisc.list_uniq (List.fast_sort Pervasives.compare - (List.map UM.buri_of_uri uri_to_remove)) + (List.map safe_buri_of_suri uri_to_remove)) in (* cleand the already visided baseuris *) let buri_to_remove = @@ -50,9 +66,6 @@ let close_uri_list uri_to_remove = else true) buri_to_remove in - List.iter - (fun buri -> Hashtbl.add cache_of_processed_baseuri buri true) - buri_to_remove; (* now calculate the list of objects that belong to these baseuris *) let uri_to_remove = List.fold_left @@ -64,7 +77,7 @@ let close_uri_list uri_to_remove = in let inhabitants = List.map (function - | HGT.Ls_object e -> UM.uri_of_string (buri ^ "/" ^ e.HGT.uri) + | HGT.Ls_object e -> buri ^ "/" ^ e.HGT.uri | _ -> assert false) inhabitants in @@ -74,15 +87,27 @@ let close_uri_list uri_to_remove = (* now we want the list of all uri that depend on them *) let depend = List.fold_left - (fun acc u -> one_step_depend (UM.string_of_uri u) @ acc) [] uri_to_remove + (fun acc u -> one_step_depend u @ acc) [] uri_to_remove in let depend = MatitaMisc.list_uniq (List.fast_sort Pervasives.compare depend) in - let depend = List.map UM.uri_of_string depend in uri_to_remove, depend +let buri_of_file file = + let ic = open_in file in + let stms = CicTextualParser2.parse_statements (Stream.of_channel ic) in + close_in ic; + let uri = ref "" in + List.iter + (function + | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", buri))) -> + uri := MatitaMisc.strip_trailing_slash buri + | _ -> ()) + stms; + !uri + let main uri_to_remove = let rec fix uris next = match next with @@ -96,8 +121,8 @@ let usage () = prerr_endline ""; prerr_endline "usage:"; prerr_endline "\tmatitaclean all"; - prerr_endline "\tmatitaclean dry uris..."; - prerr_endline "\tmatitaclean uris..."; + prerr_endline "\tmatitaclean dry (uri|file)+"; + prerr_endline "\tmatitaclean (uri|file)+"; prerr_endline ""; exit 1 @@ -113,24 +138,31 @@ let _ = if Sys.argv.(1) = "dry" then 2, true else 1, false in let uri_to_remove =ref [] in - try + (try for i = start to Array.length Sys.argv - 1 do let suri = Sys.argv.(i) in - let uri = UM.uri_of_string suri in + let uri = + try + UM.buri_of_uri (UM.uri_of_string suri) + with + UM.IllFormedUri _ -> buri_of_file suri + in uri_to_remove := uri :: !uri_to_remove done with - Invalid_argument _ -> usage (); + Invalid_argument _ -> usage ()); let l = main !uri_to_remove in if dry then begin - List.iter (fun x -> let u = UM.string_of_uri x in prerr_endline u) l; + List.iter prerr_endline l; exit 0 end else List.iter (fun u -> - prerr_endline ("Removing " ^ UM.string_of_uri u); - MatitaSync.remove u) + prerr_endline ("Removing " ^ u); + try + MatitaSync.remove (UM.uri_of_string u) + with Sys_error _ -> ()) l diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml index df6cff273..c1ccce780 100644 --- a/helm/matita/matitadep.ml +++ b/helm/matita/matitadep.ml @@ -27,20 +27,26 @@ let main () = for i = 1 to Array.length Sys.argv - 1 do let file = Sys.argv.(i) in let ic = open_in file in - let stms = CicTextualParser2.parse_statements (Stream.of_channel ic) in - close_in ic; - let stms = - List.iter - (function - | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", uri))) -> - let uri = MatitaMisc.strip_trailing_slash uri in - baseuri := (uri, file) :: !baseuri - | TA.Executable (_, TA.Command - (_, TA.Alias (_, TA.Ident_alias(_, uri)))) -> - Hashtbl.add aliases file uri - | _ -> ()) - stms + let stms = + try + CicTextualParser2.parse_statements (Stream.of_channel ic) + with + (CicTextualParser2.Parse_error _) as exc -> + prerr_endline ("Unable to parse: " ^ file); + prerr_endline (MatitaExcPp.to_string exc); + exit 1 in + close_in ic; + List.iter + (function + | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", uri))) -> + let uri = MatitaMisc.strip_trailing_slash uri in + baseuri := (uri, file) :: !baseuri + | TA.Executable (_, TA.Command + (_, TA.Alias (_, TA.Ident_alias(_, uri)))) -> + Hashtbl.add aliases file uri + | _ -> ()) + stms; Hashtbl.iter (fun file alias -> let dep = resolve alias in diff --git a/helm/matita/tests/apply.ma b/helm/matita/tests/apply.ma index 09b80cd4e..e53d315f0 100644 --- a/helm/matita/tests/apply.ma +++ b/helm/matita/tests/apply.ma @@ -1,5 +1,5 @@ (* test _with_ the WHD on the apply argument *) -set "baseuri" "cic:/matita/tests/". +set "baseuri" "cic:/matita/tests/apply/". alias id "not" = "cic:/Coq/Init/Logic/not.con". alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)". diff --git a/helm/matita/tests/auto.ma b/helm/matita/tests/auto.ma index c6b525b2b..66b973cfd 100755 --- a/helm/matita/tests/auto.ma +++ b/helm/matita/tests/auto.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/tests/". +set "baseuri" "cic:/matita/tests/auto/". alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)". diff --git a/helm/matita/tests/baseuri.ma b/helm/matita/tests/baseuri.ma index 3715a268a..eb4ae6a68 100644 --- a/helm/matita/tests/baseuri.ma +++ b/helm/matita/tests/baseuri.ma @@ -1,2 +1,2 @@ -set "baseuri" "cic:/matita/tests/". -set "baseuri" "cic:/matita/tests/". +set "baseuri" "cic:/matita/tests/baseuri/". +set "baseuri" "cic:/matita/tests/baseuri/". diff --git a/helm/matita/tests/coercions.ma b/helm/matita/tests/coercions.ma index 507147cef..2444b1d74 100644 --- a/helm/matita/tests/coercions.ma +++ b/helm/matita/tests/coercions.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/tests/". +set "baseuri" "cic:/matita/tests/coercions/". inductive pos: Set \def | one : pos diff --git a/helm/matita/tests/comments.ma b/helm/matita/tests/comments.ma index 3e3ec9d5e..cd21535e7 100644 --- a/helm/matita/tests/comments.ma +++ b/helm/matita/tests/comments.ma @@ -12,7 +12,7 @@ (* *) (****************************************************************************) -set "baseuri" "cic:/matita/tests/". +set "baseuri" "cic:/matita/tests/comments/". (* commento che va nell'ast, ma non viene contato come step perche' non e' un executable diff --git a/helm/matita/tests/fguidi.ma b/helm/matita/tests/fguidi.ma index fc2c717eb..e42de00b5 100644 --- a/helm/matita/tests/fguidi.ma +++ b/helm/matita/tests/fguidi.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/tests/". +set "baseuri" "cic:/matita/tests/fguidi/". alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". diff --git a/helm/matita/tests/first.ma b/helm/matita/tests/first.ma new file mode 100644 index 000000000..d75f372ce --- /dev/null +++ b/helm/matita/tests/first.ma @@ -0,0 +1,25 @@ +set "baseuri" "cic:/matita/tests/first/". + +inductive nat : Set \def + | O : nat + | S : nat \to nat. + +inductive eq (A:Set): A \to A \to Prop \def + refl: \forall x:A.eq A x x. + +inductive list (A:Set) : Set \def + | nil : list A + | cons : A \to list A \to list A. +alias symbol "cast" (instance 0) = "type cast". + +let rec list_len (A:Set) (l:list A) on l \def + [\lambda x.nat] + match (l:list A) with + [ nil \Rightarrow O + | (cons a tl) \Rightarrow S (list_len A tl)]. + +theorem stupid: \forall A:Set.eq ? (list_len A (nil ?)) O. +intros. +normalize. +apply refl. +qed. diff --git a/helm/matita/tests/fix_betareduction.ma b/helm/matita/tests/fix_betareduction.ma index d86602c57..b4ea8d8b5 100644 --- a/helm/matita/tests/fix_betareduction.ma +++ b/helm/matita/tests/fix_betareduction.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/tests/". +set "baseuri" "cic:/matita/tests/fix_betareduction/". alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)". alias id "n" = "cic:/Suresnes/BDD/canonicite/Canonicity_BDT/n.con". diff --git a/helm/matita/tests/inversion.ma b/helm/matita/tests/inversion.ma index 4ea9e2deb..c76851f59 100644 --- a/helm/matita/tests/inversion.ma +++ b/helm/matita/tests/inversion.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/tests/". +set "baseuri" "cic:/matita/tests/inversion/". inductive nat : Set \def O : nat diff --git a/helm/matita/tests/letrec.ma b/helm/matita/tests/letrec.ma index b47c5aebb..e8e81fa01 100644 --- a/helm/matita/tests/letrec.ma +++ b/helm/matita/tests/letrec.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/tests/". +set "baseuri" "cic:/matita/tests/letrec/". alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". diff --git a/helm/matita/tests/match.ma b/helm/matita/tests/match.ma index e36e684c2..f006a7045 100644 --- a/helm/matita/tests/match.ma +++ b/helm/matita/tests/match.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/". +set "baseuri" "cic:/matita/tests/match/". inductive True: Prop \def diff --git a/helm/matita/tests/match_inference.ma b/helm/matita/tests/match_inference.ma index d5df929bb..5cfa19cc9 100644 --- a/helm/matita/tests/match_inference.ma +++ b/helm/matita/tests/match_inference.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/tests/". +set "baseuri" "cic:/matita/tests/match_inference/". inductive pos: Set \def | one : pos diff --git a/helm/matita/tests/mysql_escaping.ma b/helm/matita/tests/mysql_escaping.ma index b8a6d9be7..e1698abd2 100644 --- a/helm/matita/tests/mysql_escaping.ma +++ b/helm/matita/tests/mysql_escaping.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/tests/". +set "baseuri" "cic:/matita/tests/mysql_escaping/". theorem a' : Prop \to Prop.intros.assumption.qed. diff --git a/helm/matita/tests/record.ma b/helm/matita/tests/record.ma index 96463f599..02ef85a05 100644 --- a/helm/matita/tests/record.ma +++ b/helm/matita/tests/record.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/tests/". +set "baseuri" "cic:/matita/tests/record/". record empty : Type \def {}. diff --git a/helm/matita/tests/rewrite.ma b/helm/matita/tests/rewrite.ma index bf4f3a6e5..3941ab0cb 100644 --- a/helm/matita/tests/rewrite.ma +++ b/helm/matita/tests/rewrite.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/tests/". +set "baseuri" "cic:/matita/tests/rewrite/". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias num (instance 0) = "natural number". diff --git a/helm/matita/tests/second.ma b/helm/matita/tests/second.ma new file mode 100644 index 000000000..ef13fc18c --- /dev/null +++ b/helm/matita/tests/second.ma @@ -0,0 +1,10 @@ +set "baseuri" "cic:/matita/tests/second/". +alias id "nat" = "cic:/matita/tests/first/nat.ind#xpointer(1/1)". +alias id "O" = "cic:/matita/tests/first/nat.ind#xpointer(1/1/1)". +alias id "eq" = "cic:/matita/tests/first/eq.ind#xpointer(1/1)". +alias id "refl" = "cic:/matita/tests/first/eq.ind#xpointer(1/1/1)". + +theorem ultrastupid : eq nat O O. +apply refl. +qed. + diff --git a/helm/matita/tests/simpl.ma b/helm/matita/tests/simpl.ma index d77f91fcd..3edc4cf35 100644 --- a/helm/matita/tests/simpl.ma +++ b/helm/matita/tests/simpl.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/tests/". +set "baseuri" "cic:/matita/tests/simpl/". alias id "not" = "cic:/Coq/Init/Logic/not.con". alias symbol "eq" (instance 0) = "leibnitz's equality". diff --git a/helm/matita/tests/test2.ma b/helm/matita/tests/test2.ma index d622703b4..cf2656710 100644 --- a/helm/matita/tests/test2.ma +++ b/helm/matita/tests/test2.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/tests/". +set "baseuri" "cic:/matita/tests/test2/". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias symbol "and" (instance 0) = "logical and". diff --git a/helm/matita/tests/test3.ma b/helm/matita/tests/test3.ma index 08ca19682..9a8958b21 100644 --- a/helm/matita/tests/test3.ma +++ b/helm/matita/tests/test3.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/tests/". +set "baseuri" "cic:/matita/tests/test3/". alias symbol "eq" (instance 0) = "leibnitz's equality". theorem a:\forall x.x=x. diff --git a/helm/matita/tests/test4.ma b/helm/matita/tests/test4.ma index e25472d3c..be67f3a8e 100644 --- a/helm/matita/tests/test4.ma +++ b/helm/matita/tests/test4.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/tests/". +set "baseuri" "cic:/matita/tests/test4/". (* commento che va nell'ast, ma non viene contato diff --git a/helm/matita/tests/third.ma b/helm/matita/tests/third.ma new file mode 100644 index 000000000..e0ae453b4 --- /dev/null +++ b/helm/matita/tests/third.ma @@ -0,0 +1,10 @@ +set "baseuri" "cic:/matita/tests/third/". +alias id "nat" = "cic:/matita/tests/first/nat.ind#xpointer(1/1)". +alias id "O" = "cic:/matita/tests/first/nat.ind#xpointer(1/1/1)". +alias id "eq" = "cic:/matita/tests/first/eq.ind#xpointer(1/1)". +alias id "ultrastupid" = "cic:/matita/tests/second/ultrastupid.con". + +theorem iperstupid : eq nat O O. +exact ultrastupid. +qed. + -- 2.39.2