( env_path: LeanString<LeanBorrowed<'_>>, out_path: LeanString<LeanBorrowed<'_>>, isolate: LeanBool<LeanBorrowed<'_>>, quiet: LeanBool<LeanBorrowed<'_>>, )
| 1897 | if names_vec.is_empty() { |
| 1898 | return LeanIOResult::error_string( |
| 1899 | "rs_kernel_check_anon_consts: no constant names given", |
| 1900 | ); |
| 1901 | } |
| 1902 | if !json_path.is_empty() && fail_out_path.is_some() { |
| 1903 | return LeanIOResult::error_string( |
| 1904 | "rs_kernel_check_anon_consts: --fail-out is not supported with per-name rows (--json)", |
| 1905 | ); |
| 1906 | } |
| 1907 | |
| 1908 | let ctx = match load_anon_seed_context( |
| 1909 | "rs_kernel_check_anon_consts", |
| 1910 | &path, |
| 1911 | &names_vec, |
| 1912 | ) { |
| 1913 | Ok(ctx) => ctx, |
| 1914 | Err(e) => return LeanIOResult::error_string(&e), |
| 1915 | }; |
| 1916 | |
| 1917 | // ---- Per-name rows mode: one independent closure run per name (the |
| 1918 | // zkVM hosts' per-constant scope), timing only each name's closure |
| 1919 | // selection + check. Rows flush per name; a rejected name records |
| 1920 | // `status: rejected` and the loop continues. |
| 1921 | if !json_path.is_empty() { |
| 1922 | let json_file = std::path::PathBuf::from(&json_path); |
| 1923 | let mut all_addrs: Vec<Address> = Vec::new(); |
| 1924 | let mut all_results = Vec::new(); |
| 1925 | for (name, item_idx) in &ctx.seeds { |
nothing calls this directly
no test coverage detected