Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Date: Wed, 25 Mar 92 03:10:14 MST
From: slind@ca.ucalgary.cpsc (Konrad Slind)
Message-Id: <9203251010.AA14246@fsa.cpsc.ucalgary.ca>
To: info-hol@edu.uidaho.cs.ted
Subject: plea for support letters


Hi,

  Well, the hol90 project ends March 31, and we have to write a final
report for NSERC, the Canadian gov't science research funding agency. I
am requesting letters of support to be included in the report. The sorts
of question that we need answered are

    0. What do you use hol90 for?
    1. What are your future plans for hol90?
    2. What are the advantages/disadvantages of hol90 when it is compared
       with hol88?

Please fax your replies (on department or company letterhead, if possible) to

    Konrad Slind
    403 284 4707

The last useful date that your reply can arrive is this Sunday (March 29).

Thanks,
Konrad.


p.s. This does not mean that work on hol90 ceases. In fact, version 4
     should be ready soon. It features a complete rewrite of the front
     end:

         - type inference is much improved,
         - parsing has been streamlined,
         - terms will be represented much more compactly,
         - the system will be fully functorized (hence libraries can
           be separately compiled and will load more quickly),
         - components of theories will be represented on disk in a
           concrete syntax (hence theories will be much smaller and
           architecture independent),
         - there is a parallel set of functions for cons- and de-structing
           terms. These are record-based rather than pair-based (i.e.,
           these functions use records with identifier labels rather
           than numeric).

     I am also contemplating a Standard hol90 that will run on any
     Standard ML. After version 4, this would be simple, requiring
     merely the abolishment of quotation/antiquotation, which will be
     a lot simpler than putting it in in the first place!


p.p.s. For performance nuts: when doing backward proof set

          System.Control.interp

       to true (it's initially false). This can result in ~30% speedup.
       This flag sets an "interpretation" mode for SML/NJ, in which
       optimization is turned off. Large compound tactics seem not to
       benefit from optimization. However, general purpose code that
       must run fast ought to be compiled with System.Control.interp set
       to false.