| 3176 | let clear_every = kernel_check_clear_every(); |
| 3177 | let mut checks_since_clear = clear_every; |
| 3178 | |
| 3179 | for (work_idx, item) in work.iter().enumerate() { |
| 3180 | if checks_since_clear >= clear_every { |
| 3181 | kenv.clear_releasing_memory(); |
| 3182 | checks_since_clear = 0; |
| 3183 | } |
| 3184 | let outcome = check_one_const( |
| 3185 | item.primary, |
| 3186 | work_idx, |
| 3187 | work_total, |
| 3188 | &ixon_env, |
| 3189 | &lookups, |
| 3190 | &names, |
| 3191 | &expect_pass, |
| 3192 | &ungrounded, |
| 3193 | &mut kenv, |
| 3194 | |prefix| progress.start(prefix), |
| 3195 | ); |
| 3196 | let prefix = outcome.prefix(); |
| 3197 | |
| 3198 | match outcome.status { |
| 3199 | CheckStatus::CompileFailed => { |
| 3200 | // Unexpected compile failure (should_pass=true) is a real problem and |
| 3201 | // must persist. Expected rejections (should_pass=false) only persist in |
| 3202 | // verbose mode; quiet mode drops them since they're part of the |
| 3203 | // tutorial's bad-constant coverage, not user-visible failures. |
| 3204 | if outcome.should_pass { |
| 3205 | progress.persist(&format!( |
| 3206 | "{prefix} ... FAIL (compile): {}", |
| 3207 | outcome.err_msg() |
| 3208 | )); |
| 3209 | } else if !quiet { |
| 3210 | progress.persist(&format!( |
| 3211 | "{prefix} ... REJECTED (compile): {}", |
| 3212 | outcome.err_msg() |
| 3213 | )); |
| 3214 | } |
| 3215 | }, |
| 3216 | CheckStatus::NotFound => { |
| 3217 | // Not-found is always unexpected — the Lean side asked for a name |
| 3218 | // that compile+ingress didn't produce. Always persist. |
| 3219 | progress.persist(&format!("{prefix} ? not found")); |
| 3220 | }, |
| 3221 | CheckStatus::Checked => { |
| 3222 | // Outcomes that must persist in quiet mode: |
| 3223 | // - Unexpected pass / unexpected failure: user cares about these. |
| 3224 | // - Slow runs with the expected outcome: useful for bisecting perf. |
| 3225 | // |
| 3226 | // Fast runs with the expected outcome stay ephemeral and are |
| 3227 | // overwritten on the next iteration. |
| 3228 | let must_persist = |
| 3229 | !outcome.is_expected() || outcome.is_slow(slow_threshold); |
| 3230 | progress.finish( |
| 3231 | &prefix, |
| 3232 | &outcome.checked_suffix(slow_threshold), |
| 3233 | must_persist, |
| 3234 | ); |
| 3235 | }, |