[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Re: Re: HOL88 on SBCL

Great, thanks!

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.

original message follows:
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
for completeness:

[1] https://github.com/zeuner/HOL88/tree/sbcl

Sébastien Villemot
⣾⠁⢠⠒⠀⣿⡁  Debian

Reply to: