= test2 for byte and opt

- version string management updated

diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile
index 02604aae86752c778b93cb5d1cbf02d5ec15b4bb..e21fccf1b423242efef3a3afa89955b534a590f3 100644 (file)
--- a/helm/software/helena/Makefile
+++ b/helm/software/helena/Makefile
@@ -10,7 +10,7 @@ KEEP = README
 
 CLEAN = etc/log.txt etc/profile.txt
 
-TAGS = test-si-fast test-si test2 test3 test6 \
+TAGS = test-si-fast test-si test2-opt test2-byte test3 test6 \
        profile-fast profile profile-coq profile-coq-byte \
        xml-si xml-si-v3 xml xml-v3 \
        export-coq export-matita \
@@ -72,11 +72,15 @@ test-si: $(MAIN).opt etc
 
 test1: $(MAIN).opt etc
        @echo "  HELENA -l -u -1 $(INPUT)"
-       ./$(MAIN).opt $(TEST1) > etc/log.txt
+       $(H)./$(MAIN).opt $(TEST1) > etc/log.txt
 
-test2: $(MAIN).opt etc
+test2-opt: $(MAIN).opt etc
        @echo "  HELENA -l -1 $(INPUT)"
-       ./$(MAIN).opt $(TEST1) $(TEST2) > etc/log.txt
+       $(H)./$(MAIN).opt $(TEST1) $(TEST2) > etc/log.txt
+
+test2-byte: $(MAIN).byte etc
+       @echo "  HELENA -l -1 $(INPUT)"
+       $(H)./$(MAIN).byte $(TEST1) $(TEST2) > etc/log.txt
 
 test3: $(MAIN).opt etc
        @echo "  HELENA -T 3 -l $(INPUT)"

diff --git a/helm/software/helena/src/basic_rg/brgGallina.ml b/helm/software/helena/src/basic_rg/brgGallina.ml
index d78f2a215b8bc4c9db4741e78f83e08ae9815ef9..bc65fe0752244f0c89c737f76c62f325baa57db1 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgGallina.ml
+++ b/helm/software/helena/src/basic_rg/brgGallina.ml
@@ -26,6 +26,8 @@ IFDEF MANAGER THEN
 
 let ok = ref true
 
+let version = KP.sprintf "This file was generated by %s: do not edit" (G.version_string true)
+
 let base = "coq"
 
 let ext = ".v"
@@ -130,7 +132,7 @@ let open_out fname =
    let path = KF.concat dir fname in
    let och = open_out (path ^ ext) in
    out_preamble och;
-   out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
+   out_top_comment och version;
    output_entity och, close_out och
 
 END

diff --git a/helm/software/helena/src/basic_rg/brgGrafite.ml b/helm/software/helena/src/basic_rg/brgGrafite.ml
index b3721e0ee5d2b942e6616dfde8cbd4d0d1387282..27ed9a1c4df539ceb454119a8a69bb9f3f78ac59 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgGrafite.ml
+++ b/helm/software/helena/src/basic_rg/brgGrafite.ml
@@ -26,6 +26,8 @@ IFDEF MANAGER THEN
 
 let ok = ref true
 
+let version = KP.sprintf "This file was generated by %s: do not edit" (G.version_string true)
+
 let base = "matita"
 
 let ext = ".ma"
@@ -124,7 +126,7 @@ let open_out fname =
    let path = KF.concat dir fname in
    let och = open_out (path ^ ext) in
    out_preamble och;
-   out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
+   out_top_comment och version;
    out_include och "basics/pts";
    output_entity och, close_out och
 

diff --git a/helm/software/helena/src/basic_rg/brgLP.ml b/helm/software/helena/src/basic_rg/brgLP.ml
index ac7acd908eef7486713340914759e0661b2ba578..8a8f9d4f296d160550d91cf5e6320f26ce67f003 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgLP.ml
+++ b/helm/software/helena/src/basic_rg/brgLP.ml
@@ -24,6 +24,8 @@ IFDEF MANAGER THEN
 
 (* Internal functions *******************************************************)
 
+let version = KP.sprintf "This file was generated by %s: do not edit" (G.version_string true)
+
 let ok = ref true
 
 let uris = ref []
@@ -192,14 +194,14 @@ let output_entity_tj2 och st (_, na, u, b) =
       let dir, name = mk_name !chunk in
       let soch = open_out (KF.concat dir name ^ ext_tj_sig) in
       out_preamble soch;
-      out_top_comment soch (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
+      out_top_comment soch version;
       out_clause soch (KP.sprintf "sig %s." name);
       out_clause soch "accum_sig grundlagen.";
       out_clause soch (KP.sprintf "type line+%02u t -> int -> t -> o." !chunk);
       close_out soch;
       let soch = open_out (KF.concat dir name ^ ext_tj) in
       out_preamble soch;
-      out_top_comment soch (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
+      out_top_comment soch version;
       out_clause soch (KP.sprintf "module %s." name);
       sub_och := soch
    end;
@@ -314,7 +316,8 @@ let open_out_lp1 fname =
    let path = KF.concat dir fname in
    let och = open_out (path ^ "1" ^ ext_lp) in
    out_preamble och;
-   out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
+   out_top_comment och version;
+   out_clause och "accumulate helena.";
    out_clause och "main :- grundlagen.";
    out_clause och "grundlagen :- gv+";
    output_entity_lp1 och, close_out_lp1 och
@@ -324,7 +327,8 @@ let open_out_lp2 fname =
    let path = KF.concat dir fname in
    let och = open_out (path ^ "2" ^ ext_lp) in
    out_preamble och;
-   out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
+   out_top_comment och version;
+   out_clause och "accumulate helena.";
    output_entity_lp2 och, close_out_lp2 och
 
 let open_out_tj2 fname =
@@ -332,7 +336,7 @@ let open_out_tj2 fname =
    let path = KF.concat dir fname ^ "2" in
    let och = open_out (path ^ ext_tj) in
    out_preamble och;
-   out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
+   out_top_comment och version;
    out_clause och "module grundlagen.";
    output_entity_tj2 och, close_out_tj2 och
 
@@ -341,7 +345,7 @@ let open_out_tj3 fname =
    let path = KF.concat dir fname in
    let och = open_out (path ^ "3" ^ ext_tj) in
    out_preamble och;
-   out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
+   out_top_comment och version;
    out_clause och "module grundlagen.";
    out_clause och "accumulate helena.";
    output_entity_tj3 och, close_out_tj3 och

diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml
index 8bc7c935633f2a209bbabe29079633d4172bd8c5..dc63b1ca642a14265523ac2bd9ac9363e77d215d 100644 (file)
--- a/helm/software/helena/src/common/options.ml
+++ b/helm/software/helena/src/common/options.ml
@@ -31,7 +31,9 @@ END
 
 (* interface functions ******************************************************)
 
-let version_string = "Helena 0.8.3 M (June 2015)"
+let version_string b =
+   if b then "Helena 0.8.3 M (June 2015)"
+   else "Helena 0.8.3 M - June 2015"
 
 let kernel = ref V3          (* kernel type *)
 

diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml
index 1d1de357295b8e29d5233d9549a638a0868688cc..c80bff4f85dc06fc82bc2c06ff5a279de9149e32 100644 (file)
--- a/helm/software/helena/src/toplevel/top.ml
+++ b/helm/software/helena/src/toplevel/top.ml
@@ -403,7 +403,7 @@ let set_summary () =
 END
 
 let set_trace i = 
-   if !G.trace = 0 && i > 0 then Y.gmtime G.version_string;
+   if !G.trace = 0 && i > 0 then Y.gmtime (G.version_string false);
    if !G.trace > 0 && i = 0 then Y.utime_stamp "at exit";
    G.trace := i;
 IFDEF SUMMARY THEN
@@ -442,7 +442,7 @@ let main =
       ] in
       let map s = s <> "" in
       let features_string = KT.concat " " (KL.filter map features) in
-      L.warn level (KP.sprintf "%s [%s]" G.version_string features_string);
+      L.warn level (KP.sprintf "%s [%s]" (G.version_string true) features_string);
       exit 0
    in
    let set_hierarchy s = 
@@ -462,7 +462,7 @@ ELSE () END;
       streaming := false;
    in
    let undefined opt () =
-      L.warn level (KP.sprintf "%s was compiled without the support for option %s" G.version_string opt);
+      L.warn level (KP.sprintf "%s was compiled without the support for option %s" (G.version_string true) opt);
       exit 0
    in
    let arg_undefined opt = Arg.Unit (undefined opt) in