Dear Sébastien, dear Camm, thanks for having a look.
My apologies if the list was the wrong place for asking. However, I don't know too much about the Debian package maintenance policies. In particular, it wasn't obvious to me whether the maintenance decision for the current hol88 package is more based on hol88 experience or on gcl experience (where the latter would imply that someone who maintain other sbcl-based packages would be more interested). Anyway, I'm happy if my work is of some use, and I'm open to comments or questions. Best regards, Isidor Zeuner 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:
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
