From 849001febdebe045a1309e6c2c854e421e6e476b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 7 Jul 2015 15:44:51 +0000 Subject: [PATCH] = test2 for byte and opt - version string management updated --- helm/software/helena/Makefile | 12 ++++++++---- helm/software/helena/src/basic_rg/brgGallina.ml | 4 +++- helm/software/helena/src/basic_rg/brgGrafite.ml | 4 +++- helm/software/helena/src/basic_rg/brgLP.ml | 16 ++++++++++------ helm/software/helena/src/common/options.ml | 4 +++- helm/software/helena/src/toplevel/top.ml | 6 +++--- 6 files changed, 30 insertions(+), 16 deletions(-) diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile index 02604aae8..e21fccf1b 100644 --- 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 d78f2a215..bc65fe075 100644 --- 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 b3721e0ee..27ed9a1c4 100644 --- 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 ac7acd908..8a8f9d4f2 100644 --- 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 8bc7c9356..dc63b1ca6 100644 --- 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 1d1de3572..c80bff4f8 100644 --- 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 -- 2.39.2