Skip to content

Commit 9767499

Browse files
added timestamps in the CakeML proof
1 parent 9e41c08 commit 9767499

File tree

1 file changed

+16
-0
lines changed

1 file changed

+16
-0
lines changed

hol/policy_to_table/fwd_proof_cakeLib.sml

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -122,6 +122,11 @@ open bdd_utilsLib;
122122
val _ = write_term_to_file ("../bdd_cake_test/" ^ file_name ^ "_policy_out_test.txt", var_policy);
123123
val _ = write_term_to_file ("../bdd_cake_test/" ^ file_name ^ "_order_out_test.txt", policy_order);
124124

125+
val _ = time_stage ("Stage 2 prepp policy ", start_cpu_total_stage2, start_real_total_stage2)
126+
127+
val start_cpu_total_stage2a = Timer.startCPUTimer ();
128+
val start_real_total_stage2a = Timer.startRealTimer ();
129+
125130

126131
val status_exec_policy = OS.Process.system
127132
("cd ../bdd_cake_test/ && time ./test_bdd_policy.cake " ^
@@ -135,6 +140,10 @@ open bdd_utilsLib;
135140
else (print "Nej, policy NDD compilation failed\n";
136141
OS.Process.exit OS.Process.failure)
137142

143+
val _ = time_stage ("Stage 2 from var policy to BDD ", start_cpu_total_stage2a, start_real_total_stage2a)
144+
val start_cpu_total_stage2b = Timer.startCPUTimer ();
145+
val start_real_total_stage2b = Timer.startRealTimer ();
146+
138147

139148

140149
val filename_policy_export = "../bdd_cake_test/" ^ file_name ^ "_bdd_policy_cakeml_export.txt"
@@ -182,6 +191,10 @@ open bdd_utilsLib;
182191

183192
val _ = write_term_to_file ("../bdd_cake_test/" ^ file_name ^ "_table_out_test.txt", gen_var_table_auto)
184193

194+
val _ = time_stage ("Stage 2 prepp tables ", start_cpu_total_stage2b, start_real_total_stage2b)
195+
val start_cpu_total_stage2c = Timer.startCPUTimer ();
196+
val start_real_total_stage2c = Timer.startRealTimer ();
197+
185198
val status_exec_table = OS.Process.system
186199
("cd ../bdd_cake_test/ && time ./test_bdd_table.cake " ^
187200
file_name ^ "_table_out_test.txt " ^
@@ -195,6 +208,9 @@ open bdd_utilsLib;
195208
OS.Process.exit OS.Process.failure)
196209

197210

211+
val _ = time_stage ("Stage 2 from table to BDD ", start_cpu_total_stage2c, start_real_total_stage2c)
212+
213+
198214
val filename_policy_export = "../bdd_cake_test/" ^ file_name ^ "_bdd_table_cakeml_export.txt"
199215
val ins_tbl = TextIO.openIn filename_policy_export
200216
val tbl_content_str = TextIO.inputAll ins_tbl;

0 commit comments

Comments
 (0)