Dear Debian Common Lisp team, with pleasure I noticed that Debian still packages the good old HOL88 theorem proving tool.
I was wondering whether a port to the SBCL Common Lisp implementation would be of any interest to, for packaging purposes. While I like the currently used implementation GCL for its tight integration with the GNU compiler collection, I found that HOL88 runs way faster on SBCL, at least when telling by the benchmark that is included. Considering that not many distributions package HOL88 as of today, I assume that a considerable fraction of today's HOL88 users would benefit from the speedup if a SBCL port would be distributed. If this is of any interest to you, feel free to check out a first working example of a port: [1]. Comments are appreciated. Best regards, Isidor Zeuner [1] https://github.com/zeuner/HOL88/tree/sbcl Diese E-Mail und die Anhaenge koennen vertrauliche und/oder rechtlich geschuetzte Informationen enthalten. Jegliches unbefugtes Kopieren, Veroeffentlichen, Verteilen oder Verbreiten der Inhalte ist untersagt. / This e-mail and its attachments may contain confidential and/or legally privileged information. Any unauthorised copying, disclosure, dissemination or distribution of the material in this e-mail is strictly prohibited.
