Greetings! "Bill Page" <[EMAIL PROTECTED]> 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: http://people.debian.org/~camm 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 [EMAIL PROTECTED] ========================================================================== "The earth is but one country, and mankind its citizens." -- Baha'u'llah _______________________________________________ Gcl-devel mailing list Gcl-devel@gnu.org http://lists.gnu.org/mailman/listinfo/gcl-devel
