Dear Isidor, On Tue, Jul 03, 2018 at 03:46:12PM +0200, Isidor Zeuner wrote: > 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. As you may have noticed, the hol88 package in Debian is not maintained by the Debian Common Lisp Team, but by Camm Maguire (in CC). He is the one who can take the decision of introducing a separate hol88 binary package (probably out of the same source package), compiled with SBCL. Best, -- ⢀⣴⠾⠻⢶⣦⠀ Sébastien Villemot ⣾⠁⢠⠒⠀⣿⡁ Debian Developer ⢿⡄⠘⠷⠚⠋⠀ http://sebastien.villemot.name ⠈⠳⣄⠀⠀⠀⠀ http://www.debian.org
Attachment:
signature.asc
Description: PGP signature