Build an `IO (Array (String × Option CheckError))` from Rust `(address, result)` pairs. Used by `rs_kernel_check_anon` to return per-result content addresses alongside the check outcome — the anon CLI has no Lean-side name to associate with each result slot, so the `# ` address label has to come back through the FFI to keep `--fail-out` and `[check]` summary lines content-addressed.
( addrs: &[Address], results: &[CheckRes], )
| 2991 | &ixon_env, |
| 2992 | &lookups, |
| 2993 | &names, |
| 2994 | &expect_pass, |
| 2995 | &ungrounded, |
| 2996 | &mut kenv, |
| 2997 | |prefix| progress.start(prefix), |
| 2998 | ); |
| 2999 | let prefix = outcome.prefix(); |
| 3000 | |
| 3001 | match outcome.status { |
| 3002 | CheckStatus::CompileFailed => { |
| 3003 | // Unexpected compile failure (should_pass=true) is a real problem and |
| 3004 | // must persist. Expected rejections (should_pass=false) only persist in |
| 3005 | // verbose mode; quiet mode drops them since they're part of the |
| 3006 | // tutorial's bad-constant coverage, not user-visible failures. |
| 3007 | if outcome.should_pass { |
| 3008 | progress.persist(&format!( |
| 3009 | "{prefix} ... FAIL (compile): {}", |
| 3010 | outcome.err_msg() |
| 3011 | )); |
| 3012 | } else if !quiet { |
| 3013 | progress.persist(&format!( |
no test coverage detected