Option to run only the external kernels (skip the builtin replay) #102

Comparator always runs the builtin Lean kernel replay after any external_kernels. In Main.lean, result := result <|> (← runBuiltinKernel solution) runs unconditionally.

So the README's trust assumption can be reduced to "at least one of the Lean kernel or the external_kernels is correct", but the run time can't. For very large solutions, the single-threaded builtin replay dominates.

Proposal. An opt-in config field, for example "builtin_kernel": false (default true). It would only be allowed together with a non-empty external_kernels, and it would skip runBuiltinKernel. The trust assumption would then read "at least one of the external_kernels is correct".

Motivation. Take https://github.com/dpwoodru/general-courtade-kumar-lean: a ~100 GB export with 22.1M constants.

• Builtin replay: projected at one to two weeks single-threaded (see Optional parallel kernel replay #95 and feat: optional parallel kernel replay (parallel_replay) #99).
• con-leche: it checks in parallel and has a formal consistency proof. It accepted the whole export in 5.7 h with 150 workers, though with raised step budgets (fuel exhausted: whnf loop on a large decide +kernel proof (~100 GB export); raising the loop budgets 1000x makes it pass con-leche#10).

As @nomeata noted on #99, there is currently no supported way to do this. Happy to send a PR if this sounds acceptable.