vprover / vampire

The Vampire Theorem Prover
https://vprover.github.io/
Other
302 stars 52 forks source link

put LTB and dependencies on hiatus #533

Closed MichaelRawson closed 8 months ago

MichaelRawson commented 8 months ago

See #157. @quickbeam123's recent interactive mode removes the need for LTB from a user perspective. LTB is also on hiatus at CASC.

My view is that if LTB comes back and we need to restore it in the future, we can pay the maintenance cost then. Therefore: remove LTB and some of its dependencies from Vampire. Lib::FreshnessGuard is apparently unrelated but also unused.

MichaelRawson commented 8 months ago

Also remove tTwoVampires. This has been of questionable value for a while but now it mostly tests stuff that no longer exists.