From: Stefano Zacchiroli Date: Thu, 5 Feb 2004 17:22:54 +0000 (+0000) Subject: - added testlibrary .opts X-Git-Tag: V_0_2_3~33 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=16f4538e0eb7deba0e145298aa8fef847d8a51f9;p=helm.git - added testlibrary .opts - build just gTopLevel per default --- diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index 54a2f1d16..8a41c7dc2 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -13,8 +13,8 @@ OCAMLDEP = ocamldep -pp camlp4o LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES)) LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES)) -all: styles gTopLevel regtest -opt: styles gTopLevel.opt regtest.opt +all: styles gTopLevel +opt: styles gTopLevel.opt start: $(MAKE) -C ../hbugs/ start @@ -59,6 +59,8 @@ gTopLevel.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT) testlibrary: $(TESTLIBOBJS) $(LIBRARIES) $(OCAMLC) -linkpkg -o $@ $(TESTLIBOBJS) +testlibrary.opt: $(TESTLIBOBJS:.cmo=.cmx) $(LIBRARIES) + $(OCAMLOPT) -linkpkg -o $@ $(TESTLIBOBJS:.cmo=.cmx) regtest: $(REGTESTOBJS) $(LIBRARIES) $(OCAMLC) -linkpkg -o $@ $(REGTESTOBJS) regtest.opt: $(REGTESTOBJS:.cmo=.cmx) $(LIBRARIES) @@ -91,9 +93,9 @@ cleantest: rm -f $(OUTTESTS) tests/%.cic.test: tests/%.cic regtest time ./regtest -gen $< -test: +test: regtest ./regtest $(INTESTS) 2> /dev/null -envtest: +envtest: regtest ./regtest -dump $(INTESTS) 2> /dev/null ifneq ($(MAKECMDGOALS), depend) diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml index bdc07e977..a4675a751 100644 --- a/helm/gTopLevel/testlibrary.ml +++ b/helm/gTopLevel/testlibrary.ml @@ -1,4 +1,6 @@ +open Printf + let mqi_debug_fun = ignore let mqi_flags = [] let mqi_handle = MQIConn.init mqi_flags mqi_debug_fun @@ -28,8 +30,7 @@ module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks) let debug_print s = prerr_endline ("^^^^^^ " ^ s) -let main () = - let uri = UriManager.uri_of_string (Sys.argv.(1)) in +let test_uri uri = let obj = CicCache.get_obj uri in let (annobj, _, _, ids_to_inner_sorts, _, _, _) = Cic2acic.acic_object_of_cic_object obj @@ -52,8 +53,10 @@ let main () = debug_print "Cic.AConstant (ty)"; round_trip ty | Cic.AConstant (_, _, _, Some bo, ty, _) -> +(* debug_print "Cic.AConstant (bo)"; round_trip bo; +*) debug_print "Cic.AConstant (ty)"; round_trip ty | Cic.AVariable (_, _, None, ty, _) -> @@ -72,5 +75,37 @@ let main () = | Cic.AInductiveDefinition _ -> debug_print "AInductiveDefinition: boh ..." -let _ = main () +let test_uri uri = try test_uri uri; true with _ -> false + +let _ = + let idx = ref 0 in + let ok = ref [] in + let nok = ref [] in + try + let mode = if Sys.argv.(1) = "-" then `Stdin else `Cmdline in + while true do + incr idx; + let uri_str = + match mode with + | `Stdin -> input_line stdin + | `Cmdline -> Sys.argv.(!idx) + in + printf "Testing URI: %s ...\t"; + let uri = UriManager.uri_of_string uri_str in + if test_uri uri then begin + print_endline "[ OK ]"; + ok := uri_str :: !ok + end else begin + print_endline "[ FAILED ]"; + nok := uri_str :: !nok + end + done + with Invalid_argument _ | End_of_file -> + print_newline (); + print_endline "TestLibrary report"; + print_endline "Succeeded URIs:"; + List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !ok); + print_endline "Failed URIs:"; + List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !nok); + print_newline ()