FStar
FStar copied to clipboard
--trace_error incompatible with --debug?
trafficstars
No idea why this is happening, but making a note to not forget
module XX
let x = 1 + 'a'
$ ./bin/fstar.exe XX.fst --trace_error
Unexpected error
FStar_Errors.Error(_)
Raised at FStar_Compiler_Effect.raise in file "fstar-lib/FStar_Compiler_Effect.ml" (inlined), line 10, characters 12-17
Called from FStar_Errors.raise_error_doc in file "fstar-lib/generated/FStar_Errors.ml", line 926, characters 10-44
Called from FStar_TypeChecker_Util.check_has_type_maybe_coerce in file "fstar-lib/generated/FStar_TypeChecker_Util.ml", line 6847, characters 18-107
Called from FStar_TypeChecker_TcTerm.value_check_expected_typ in file "fstar-lib/generated/FStar_TypeChecker_TcTerm.ml", line 518, characters 19-109
Called from FStar_Compiler_Util.record_time in file "fstar-lib/FStar_Compiler_Util.ml", line 26, characters 14-18
Called from FStar_TypeChecker_TcTerm.tc_term in file "fstar-lib/generated/FStar_TypeChecker_TcTerm.ml", line 1732, characters 9-1023
Called from FStar_TypeChecker_TcTerm.check_application_args.tc_args in file "fstar-lib/generated/FStar_TypeChecker_TcTerm.ml", line 7667, characters 47-61
Called from FStar_TypeChecker_TcTerm.tc_maybe_toplevel_term in file "fstar-lib/generated/FStar_TypeChecker_TcTerm.ml", line 3553, characters 28-118
Called from FStar_TypeChecker_TcTerm.check_let_bound_def in file "fstar-lib/generated/FStar_TypeChecker_TcTerm.ml", line 11959, characters 21-1023
Called from FStar_TypeChecker_TcTerm.check_top_level_let in file "fstar-lib/generated/FStar_TypeChecker_TcTerm.ml", line 10501, characters 22-54
Called from FStar_TypeChecker_Tc.tc_sig_let.(fun) in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 1402, characters 40-1023
Called from FStar_TypeChecker_Tc.tc_sig_let.(fun) in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 1399, characters 33-1023
Called from FStar_TypeChecker_Tc.run_phase1 in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 824, characters 13-17
Called from FStar_TypeChecker_Tc.tc_sig_let in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 1302, characters 26-1023
Called from FStar_Errors.with_ctx in file "fstar-lib/generated/FStar_Errors.ml", line 995, characters 27-31
Called from FStar_TypeChecker_Tc.tc_decls.process_one_decl in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 4840, characters 20-102
Called from FStar_TypeChecker_Tc.tc_decls.process_one_decl_timed in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 4936, characters 15-159
Called from FStar_Compiler_Util.fold_flatten in file "fstar-lib/FStar_Compiler_Util.ml", line 811, 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 4954, characters 8-170
Called from FStar_TypeChecker_Tc.tc_partial_modul.(fun) in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 5142, characters 25-77
Called from FStar_TypeChecker_Tc.tc_modul in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 5225, characters 20-44
Called from FStar_TypeChecker_Tc.check_module in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 5407, characters 22-39
Called from FStar_Universal.tc_one_file.tc_source_file.check_mod.check.(fun) in file "fstar-lib/generated/FStar_Universal.ml", line 1081, characters 29-141
Called from FStar_Universal.with_tcenv_of_env in file "fstar-lib/generated/FStar_Universal.ml", line 130, characters 65-73
Called from FStar_Universal.tc_one_file.tc_source_file.check_mod in file "fstar-lib/generated/FStar_Universal.ml", line 1102, characters 21-134
Called from FStar_Universal.tc_one_file in file "fstar-lib/generated/FStar_Universal.ml", line 1175, characters 32-49
Called from FStar_Universal.tc_one_file_from_remaining in file "fstar-lib/generated/FStar_Universal.ml", line 1328, characters 16-98
Called from FStar_Universal.tc_fold_interleave in file "fstar-lib/generated/FStar_Universal.ml", line 1358, characters 19-71
Called from FStar_Universal.batch_mode_tc in file "fstar-lib/generated/FStar_Universal.ml", line 1403, characters 20-72
Called from FStar_Main.go in file "fstar-lib/generated/FStar_Main.ml", line 235, characters 36-124
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 344, characters 28-62
* Error 189 at XX.fst(3,12-3,15):
- Expected expression of type Prims.int
got expression 'a'
of type FStar.Char.char
1 error was reported (see above)
$ ./bin/fstar.exe XX.fst --trace_error --debug XX
Will try to load cmxs files: []
Opening file XX.fst
Chosen Z3 executable: z3-4.8.5
Opening file XX.fst
Checking module: XX
Now verifying implementation of XX
Processing let x
* Error 189 at XX.fst(3,12-3,15):
- Expected expression of type Prims.int
got expression 'a'
of type FStar.Char.char
Unexpected error
FStar_Errors.Error(_)
Raised at BatString.find_from.find in file "src/batString.ml", line 112, characters 31-46
Called from BatString.split_on_string_comp.loop in file "src/batString.ml", line 410, characters 19-43
1 error was reported (see above)