This is very useful to track places where F* starts consuming a bunch of
memory or taking too long. Example:
[...]
sub_comp of Prims.Tot (Rust_primitives.unsize_tc (*?u476*) _) --and-- Prims.Tot (Rust_primitives.unsize_tc (*?u476*) _) --with-- SUB
sub_comp of Prims.Tot (Rust_primitives.unsize_tc (*?u476*) _) --and-- Prims.Tot (Rust_primitives.unsize_tc (*?u476*) _) --with-- SUB --- solved in 0 ms
ramon: poll wall=03m57.000s usage=34.780s user=32.207s sys=02.573s mem=2099MiB roottime=20.400s load=0.97 rootload=0.96
ramon: poll wall=03m58.000s usage=35.780s user=33.207s sys=02.573s mem=2099MiB roottime=21.400s load=1.00 rootload=1.00
ramon: poll wall=03m59.000s usage=36.780s user=34.207s sys=02.573s mem=2123MiB roottime=22.400s load=1.00 rootload=1.00
ramon: poll wall=04m00.000s usage=37.780s user=35.207s sys=02.573s mem=2153MiB roottime=23.400s load=1.00 rootload=1.00
ramon: poll wall=04m01.000s usage=38.780s user=36.192s sys=02.588s mem=2592MiB roottime=24.390s load=1.00 rootload=0.99
ramon: poll wall=04m02.000s usage=39.780s user=37.152s sys=02.628s mem=3031MiB roottime=25.350s load=1.00 rootload=0.96
ramon: poll wall=04m03.000s usage=40.780s user=38.120s sys=02.660s mem=3418MiB roottime=26.320s load=1.00 rootload=0.97
ramon: poll wall=04m04.000s usage=41.780s user=39.112s sys=02.668s mem=3803MiB roottime=27.310s load=1.00 rootload=0.99
^C* Info at Libcrux_ml_kem.Ind_cca.fst(196,0-325,75):
- GOT SIGINT! Exiting
- Stack trace:
Raised by primitive operation at FStar_Compiler_Util.stack_dump in file "fstar-lib/FStar_Compiler_Util.ml", line 134, characters 53-82
Called from FStar_Errors_Msg.backtrace_doc in file "fstar-lib/generated/FStar_Errors_Msg.ml", line 43, characters 12-45
Called from FStar_Errors.maybe_add_backtrace in file "fstar-lib/generated/FStar_Errors.ml", line 643, characters 32-65
Called from FStar_Errors.diag_doc in file "fstar-lib/generated/FStar_Errors.ml", line 654, characters 19-42
Called from FStar_Main.go.h' in file "fstar-lib/generated/FStar_Main.ml", line 147, characters 15-97
Called from FStar_Syntax_Subst.compose_uvar_subst.aux.(fun) in file "fstar-lib/generated/FStar_Syntax_Subst.ml", line 691, characters 38-53
Called from BatList.map in file "src/batList.ml", line 246, characters 23-28
Called from FStar_List.collect in file "fstar-lib/FStar_List.ml" (inlined), line 43, characters 34-51
[...]
Called from FStar_TypeChecker_Normalize.norm.fallback in file "fstar-lib/generated/FStar_TypeChecker_Normalize.ml", line 3362, characters 28-208
Called from FStar_TypeChecker_Normalize.norm.fallback in file "fstar-lib/generated/FStar_TypeChecker_Normalize.ml", line 3362, characters 28-208
Called from FStar_TypeChecker_Normalize.norm.fallback in file "fstar-lib/generated/FStar_TypeChecker_Normalize.ml", line 3362, characters 28-208
Called from FStar_TypeChecker_Normalize.norm.fallback in file "fstar-lib/generated/FStar_TypeChecker_Normalize.ml", line 3362, characters 28-208
Called from FStar_TypeChecker_Normalize.norm in file "fstar-lib/generated/FStar_TypeChecker_Normalize.ml", line 3717, characters 29-49
Called from FStar_TypeChecker_Normalize.norm_comp.(fun) in file "fstar-lib/generated/FStar_TypeChecker_Normalize.ml", line 5576, characters 43-61
Called from BatList.mapi in file "src/batList.ml", line 1022, characters 23-30
Called from FStar_TypeChecker_Normalize.norm_comp in file "fstar-lib/generated/FStar_TypeChecker_Normalize.ml", line 5577, characters 15-56
Called from FStar_Compiler_Util.record_time in file "fstar-lib/FStar_Compiler_Util.ml", line 26, characters 14-18
Called from FStar_Errors.with_ctx in file "fstar-lib/generated/FStar_Errors.ml", line 1014, characters 27-31
Called from FStar_TypeChecker_Normalize.normalize_comp.(fun) in file "fstar-lib/generated/FStar_TypeChecker_Normalize.ml", line 8221, characters 16-221
Called from FStar_TypeChecker_TcTerm.norm_c in file "fstar-lib/generated/FStar_TypeChecker_TcTerm.ml" (inlined), line 213, characters 13-73
Called from FStar_TypeChecker_TcTerm.check_expected_effect in file "fstar-lib/generated/FStar_TypeChecker_TcTerm.ml", line 782, characters 30-43
Called from FStar_TypeChecker_TcTerm.tc_abs in file "fstar-lib/generated/FStar_TypeChecker_TcTerm.ml", line 6658, characters 45-151
Called from FStar_TypeChecker_TcTerm.check_let_bound_def in file "fstar-lib/generated/FStar_TypeChecker_TcTerm.ml", line 11978, characters 21-1023
Called from FStar_TypeChecker_TcTerm.check_top_level_let in file "fstar-lib/generated/FStar_TypeChecker_TcTerm.ml", line 10531, characters 22-54
Called from FStar_TypeChecker_Tc.tc_sig_let.(fun) in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 1254, characters 40-1023
Called from FStar_TypeChecker_Tc.tc_sig_let.(fun) in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 1251, characters 33-1023
Called from FStar_TypeChecker_Tc.run_phase1 in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 682, characters 13-17
Called from FStar_TypeChecker_Tc.tc_sig_let in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 1154, characters 26-1023
Called from FStar_TypeChecker_Tc.tc_decl in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 4323, characters 16-32
Called from FStar_Errors.with_ctx in file "fstar-lib/generated/FStar_Errors.ml", line 1014, characters 27-31
Called from FStar_TypeChecker_Tc.tc_decls.process_one_decl in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 5071, characters 20-102
Called from FStar_TypeChecker_Tc.tc_decls.process_one_decl_timed in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 5154, characters 15-159
Called from FStar_Compiler_Util.fold_flatten in file "fstar-lib/FStar_Compiler_Util.ml", line 775, characters 30-37
Called from FStar_Syntax_Unionfind.with_uf_enabled in file "fstar-lib/generated/FStar_Syntax_Unionfind.ml", line 107, characters 12-16
Called from FStar_TypeChecker_Tc.tc_decls in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 5172, characters 8-170
Called from FStar_TypeChecker_Tc.tc_partial_modul.(fun) in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 5371, characters 25-77
Called from FStar_TypeChecker_Tc.tc_modul in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 5481, characters 20-44
Called from FStar_TypeChecker_Tc.check_module in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 5672, characters 22-38
Called from FStar_Universal.tc_one_file.tc_source_file.check_mod.check.(fun) in file "fstar-lib/generated/FStar_Universal.ml", line 1140, characters 29-141
Called from FStar_Universal.with_tcenv_of_env in file "fstar-lib/generated/FStar_Universal.ml", line 131, characters 65-73
Called from FStar_Universal.tc_one_file.tc_source_file.check_mod in file "fstar-lib/generated/FStar_Universal.ml", line 1161, characters 21-134
Called from FStar_Universal.tc_one_file in file "fstar-lib/generated/FStar_Universal.ml", line 1251, characters 32-49
Called from FStar_Universal.tc_one_file_from_remaining in file "fstar-lib/generated/FStar_Universal.ml", line 1393, characters 16-97
Called from FStar_Universal.tc_fold_interleave in file "fstar-lib/generated/FStar_Universal.ml", line 1433, characters 19-71
Called from FStar_Universal.batch_mode_tc in file "fstar-lib/generated/FStar_Universal.ml", line 1478, characters 20-72
Called from FStar_Main.go in file "fstar-lib/generated/FStar_Main.ml", line 283, characters 39-130
Called from FStar_Compiler_Util.record_time in file "fstar-lib/FStar_Compiler_Util.ml", line 26, characters 14-18
Called from FStar_Main.main.(fun) in file "fstar-lib/generated/FStar_Main.ml", line 401, characters 28-62
Called from Dune__exe__Main.x in file "fstar/main.ml", line 19, characters 6-24
- > While normalizing a computation type
> While typechecking the top-level declaration `let decapsulate`
ramon: end Sat Aug 17 15:02:43 2024
ramon: root.execname fstar.exe
ramon: root.utime 28.210s
ramon: root.stime 2.660s
ramon: group.total 42.732s
ramon: group.utime 40.019s
ramon: group.stime 2.712s
ramon: group.mempeak 4250MiB
ramon: group.pidpeak 4
ramon: status exited
ramon: exitcode 1
ramon: walltime 244.941s
ramon: loadavg 0.17
This is very useful to track places where F* starts consuming a bunch of memory or taking too long. Example: