On Tue, Jul 10, 2018 at 12:33:47PM +0200, Sébastien Villemot wrote: > 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. I inadvertendly stripped the link to the SBCL port in my message, copied here for completeness: [1] https://github.com/zeuner/HOL88/tree/sbcl -- ⢀⣴⠾⠻⢶⣦⠀ Sébastien Villemot ⣾⠁⢠⠒⠀⣿⡁ Debian Developer ⢿⡄⠘⠷⠚⠋⠀ http://sebastien.villemot.name ⠈⠳⣄⠀⠀⠀⠀ http://www.debian.org
Attachment:
signature.asc
Description: PGP signature