Status of `Tactic/Sat/FromLRAT`

Stream: mathlib4

[Michael Rothgang]

What's the current status of Tactic/Sat/FromLRAT? Is this file still relevant and used, with the LeanSAT project being up and coming? The tactic defined there is not used in mathlib, and it is rarely used on github: search results
All results are either forks of mathlib, a fork of leansat (once) or the

• the leanbv repository,
• the formal Ramsey project which appears not dead,

[Kim Morrison]

@Mario Carneiro can answer better, but my understanding is that it is intended for kernel verification/translation of small LRat proofs. (With large LRat proofs implausibly slow to verify in the kernel.)

By contrast, https://github.com/leanprover/leansat, which is nearing official release (cc'ing @Henrik Böving to the conversation) targets processing LRat proofs using compiled code (and hence the proofs it generates depends on the ofReduceBool axiom, indicating trust in the compiler), and mostly does not intend to expose the LRat proved statement to the user, but instead provides an end to end bitblasting tactic. It successfully handles realistic size problems.

My ideal would be that this eventually be moved out to its own repository (or slated for deprecation if there is not energy to do that).

[Mario Carneiro]

FromLRAT is a proof of concept, which does what it is intended to do and has limited applicability. It's not really replaced by leansat, in particular because it does not rely on any extra axioms like reduceBool or other external trust mechanisms, but lean's kernel is a bit limited in the size of proofs it can handle.

[Michael Rothgang]

Thanks for clarifying! In particular, I understand this file will stay in mathlib short-term and cleaning it up is worthwhile.