- added testlibrary .opts

- build just gTopLevel per default

diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile
index 54a2f1d1660d48d405f75bba3064a32fde5c2427..8a41c7dc25f8bac87bf85161578b841f3c7ec1e0 100644 (file)
--- 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 bdc07e97798c43afd1f3304aa5e142e8328cb09f..a4675a75100ed18f92493712e9862c740414c489 100644 (file)
--- 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 "\e[01;32m[   OK   ]\e[00m";
+        ok := uri_str :: !ok
+      end else begin
+        print_endline "\e[01;31m[ FAILED ]\e[00m";
+        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 ()