[Top][All Lists]

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

[Gcl-devel] HOL88 (was Re: Axiom and the ML language built into the same

From: Camm Maguire
Subject: [Gcl-devel] HOL88 (was Re: Axiom and the ML language built into the same image)
Date: 23 Oct 2006 17:02:58 -0400
User-agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2


"Bill Page" <address@hidden> writes:

> > On October 21, 2006 4:05 PM Camm Maguire wrote:
> > ... 
> > 
> > Lastly, you all in the axiom world might like to know that I'm about
> > to release an HOL88 Debian package build atop GCL.  In addition to
> > providing an alternate theorem proving environment, one also has the
> > ML language built into the same image for potential use by axiom.
> > More on this later.
> > 
> I would like to hear more about how to build Axiom with ML built
> in to the same image!

Am happy to announce the submission today of a set of packages for
HOL88, built atop GCL, to Debian.

You can see the packages at:


Until these are accepted by Debian, after which time one can retrieve
the source and binaries via apt-get, one can:

1) build from source with current gcl (2.6.8 or head) in path:
   dpkg-source -x hol88*dsc
   cd hol88-2.02.19940316
   debian/rules build

2) install the binaries the usual way:
   (as root) dpkg -i *.deb

3) unpack in a local directory:

   for i in *.deb ; do dpkg --fsys-tarfile $i | tar xf - ; done

   (here you will likely have to 'install `new_directory`;;' in the
   unpackaged usr/lib/hol88-2.02.19940316/hol image)
   (You can save a new image with 'lisp `(ml-save "new_image")`;;')

I am far from an expert on the evolution of ML, but my preliminary
understanding is that this ML was one of the main progenators of
today's family of ML's.  Indeed, the authors of the HOL system seemed
to have much to do with the invention of the language itself.  I
believe this dialect was referred to as 'Classic ML'.  I do not know
how it relates to standard ML, but I bet it is quite close.  In any
case, its original implementation was written in lisp, and
conventionally compiled with akcl, the ancestor to GCL.  The build
still works, yielding not only an ML in lisp environment, but a
substantial theorem proving environment with a large library in its
own right.  

Axiom has discussed in the past incorporating ACL2 as a means to
verify its algorithms.  HOL88 should provide yet another such
opportunity in addition to providing ML facilities within axiom.

Please keep in mind that the packages, and the facility in general, are
still in an early stage of development.  In particular, HOL88 loads
right into the user package, so is not well isolated.

Take care,

> Thanks.
> Bill Page.

Camm Maguire                                            address@hidden
"The earth is but one country, and mankind its citizens."  --  Baha'u'llah

reply via email to

[Prev in Thread] Current Thread [Next in Thread]