- version string management updated
CLEAN = etc/log.txt etc/profile.txt
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 \
profile-fast profile profile-coq profile-coq-byte \
xml-si xml-si-v3 xml xml-v3 \
export-coq export-matita \
test1: $(MAIN).opt etc
@echo " HELENA -l -u -1 $(INPUT)"
test1: $(MAIN).opt etc
@echo " HELENA -l -u -1 $(INPUT)"
- ./$(MAIN).opt $(TEST1) > etc/log.txt
+ $(H)./$(MAIN).opt $(TEST1) > etc/log.txt
+test2-opt: $(MAIN).opt etc
@echo " HELENA -l -1 $(INPUT)"
@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)"
test3: $(MAIN).opt etc
@echo " HELENA -T 3 -l $(INPUT)"
+let version = KP.sprintf "This file was generated by %s: do not edit" (G.version_string true)
+
let base = "coq"
let ext = ".v"
let base = "coq"
let ext = ".v"
let path = KF.concat dir fname in
let och = open_out (path ^ ext) in
out_preamble och;
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
output_entity och, close_out och
END
+let version = KP.sprintf "This file was generated by %s: do not edit" (G.version_string true)
+
let base = "matita"
let ext = ".ma"
let base = "matita"
let ext = ".ma"
let path = KF.concat dir fname in
let och = open_out (path ^ ext) in
out_preamble och;
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
out_include och "basics/pts";
output_entity och, close_out och
(* Internal functions *******************************************************)
(* 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 []
let ok = ref true
let uris = ref []
let dir, name = mk_name !chunk in
let soch = open_out (KF.concat dir name ^ ext_tj_sig) in
out_preamble soch;
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_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;
out_clause soch (KP.sprintf "module %s." name);
sub_och := soch
end;
let path = KF.concat dir fname in
let och = open_out (path ^ "1" ^ ext_lp) in
out_preamble och;
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
out_clause och "main :- grundlagen.";
out_clause och "grundlagen :- gv+";
output_entity_lp1 och, close_out_lp1 och
let path = KF.concat dir fname in
let och = open_out (path ^ "2" ^ ext_lp) in
out_preamble och;
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 =
output_entity_lp2 och, close_out_lp2 och
let open_out_tj2 fname =
let path = KF.concat dir fname ^ "2" in
let och = open_out (path ^ ext_tj) in
out_preamble och;
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
out_clause och "module grundlagen.";
output_entity_tj2 och, close_out_tj2 och
let path = KF.concat dir fname in
let och = open_out (path ^ "3" ^ ext_tj) in
out_preamble och;
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
out_clause och "module grundlagen.";
out_clause och "accumulate helena.";
output_entity_tj3 och, close_out_tj3 och
(* interface functions ******************************************************)
(* 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 *)
let kernel = ref V3 (* kernel type *)
- 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
if !G.trace > 0 && i = 0 then Y.utime_stamp "at exit";
G.trace := i;
IFDEF SUMMARY THEN
] in
let map s = s <> "" in
let features_string = KT.concat " " (KL.filter map features) in
] 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 =
exit 0
in
let set_hierarchy s =
streaming := false;
in
let undefined opt () =
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
exit 0
in
let arg_undefined opt = Arg.Unit (undefined opt) in