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