Format a `TcError` for user-facing Lean-side display. For the two cases we hit most often we emit a human-tuned multi-line message; everything else falls through to `Debug`.
( e: &TcError<M>, ixon_env: &IxonEnv, lookups: &IxonIngressLookups, )
| 2915 | for (work_idx, item) in work.iter().enumerate() { |
| 2916 | if checks_since_clear >= clear_every { |
| 2917 | kenv.clear_releasing_memory(); |
| 2918 | checks_since_clear = 0; |
| 2919 | } |
| 2920 | let outcome = check_one_const( |
| 2921 | item.primary, |
| 2922 | work_idx, |
| 2923 | work_total, |
| 2924 | &ixon_env, |
| 2925 | &lookups, |
| 2926 | &names, |
| 2927 | &expect_pass, |
| 2928 | &ungrounded, |
| 2929 | &mut kenv, |
| 2930 | |prefix| progress.start(prefix), |
| 2931 | ); |
| 2932 | let prefix = outcome.prefix(); |
| 2933 | |
| 2934 | match outcome.status { |
| 2935 | CheckStatus::CompileFailed => { |
| 2936 | // Unexpected compile failure (should_pass=true) is a real problem and |
| 2937 | // must persist. Expected rejections (should_pass=false) only persist in |
| 2938 | // verbose mode; quiet mode drops them since they're part of the |
| 2939 | // tutorial's bad-constant coverage, not user-visible failures. |
| 2940 | if outcome.should_pass { |
| 2941 | progress.persist(&format!( |
| 2942 | "{prefix} ... FAIL (compile): {}", |
| 2943 | outcome.err_msg() |
| 2944 | )); |
| 2945 | } else if !quiet { |
| 2946 | progress.persist(&format!( |
| 2947 | "{prefix} ... REJECTED (compile): {}", |
| 2948 | outcome.err_msg() |
| 2949 | )); |
| 2950 | } |
| 2951 | }, |
| 2952 | CheckStatus::NotFound => { |
| 2953 | // Not-found is always unexpected — the Lean side asked for a name |
| 2954 | // that compile+ingress didn't produce. Always persist. |
no test coverage detected