v1.8.0

This update ships the insert_sorries repair to repair_proofs and allows unqualified names to be passed to the names field.

Removed

• Removed Lean 4.33.0 due to kernel soundness bugs in Lean and replaced with Lean 4.33.1, which patches the bugs. Note that although we only remove Lean 4.33.0, these bugs affect all prior versions as well.

Added

• repair_proofs now implements the insert_sorries repair: a proof that runs out of tactics with goals still open gets a sorry appended (all_goals sorry when more than one goal is left), and an empty proof body is filled the same way, so incomplete proofs compile. It runs as part of the default repair set.
• Added Lean 4.34.0, and added Lean 4.33.1 as a replacement for Lean 4.33.0.

Changed

• A missing type_hash or unfolded_type_hash (returned by extract_decls and extract_theorems) now defaults to None instead of 0.
• The names field now accepts unqualified declaration names: bar selects Foo.bar when exactly one declaration in the file matches, mirroring how Lean resolves a short name. A name matching several declarations returns an error listing the candidates.
• exponent is too big is now a LeanResourceExceeded (non-retriable) error.