Remove Heapster and MRSolver #2574
Description
The Heapster and MRSolver code has proved to be very difficult and expensive to maintain, and should be removed. It has obstructed efforts to implement several other desired changes to SAW (#1612, #2328, #2336, #2429, #2434, #2548, #2573, etc).
Heapster and MRSolver implement a lot of non-trivial functionality for SAW that reproduces features found in other interactive theorem provers, including proof tactics, existential variables, and unification. Unfortunately the implementations of those features depend in deep and subtle ways on low-level details of the SAWCore term representation for things like tuples and bound variables; this means that any attempts to modify the SAWCore term representation usually break Heapster/MRSolver proofs. It turns out that these broken proof scripts are very difficult to debug because failures are not localized: We don't have small unit tests for things like evar unification, only full end-to-end proof scripts. We also lack documented internal invariants that would let us detect failures early enough to aid in debugging.
My personal recommendation is that the Heapster and MRSolver code should be completely removed, in order to simplify SAW and facilitate its further development and maintenance. Many other internal features of SAW that existed only to support Heapster/MRSolver can be removed as well.
If we would like to make use of Heapster/MRSolver in the future, it may make more sense to reimplement them as an extension to an existing dependently-typed interactive proof assistant like Rocq or Lean; we could take advantage of pre-existing support for tactics, unification, evars, etc and probably get a better user experience overall.