[isabelle-dev] Sledgehammer users: SPASS upgrade

[Jasmin Blanchette]

Dear Isabelle developers,

This email is destined to those of you who use SPASS on the repository or snapshot version of Isabelle.

Newer versions of SPASS support the TPTP syntax in addition to the native DFG syntax. They also address other issues (e.g., support for 64+-character symbols). This means we can ditch quite some code in Sledgehammer that deals with the DFG syntax, as soon as you have upgraded your SPASS. Beyond reducing bloat, moving away from the DFG format will also increase Sledgehammer's success rate because Isabelle's DFG code is known to be buggy (see e.g. 86e62a98deea).

The new SPASS is available from

    http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz

The installation procedure is as before: Unpack the archive somewhere. Edit your "~/.isabelle/etc/components" file and replace the line "/path/to/old/spass" with "/path/to/new/spass". Viel Spaß!

Spaß beiseite: I would like to remove the DFG code before the next release, unless there are good objections. Once this is done, if you haven't upgraded SPASS yet you'll get an error message from Sledgehammer telling you (how) to upgrade.

For users of official releases, there will be a new SPASS package on the Download page and SPASS will be included with the pre-built packages, so I trust the transition will be very smooth.

Let me know if you have any questions or issues.

Jasmin