[Top][All Lists]

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

Re: [Gcl-devel] #n= etc.

From: Matt Kaufmann
Subject: Re: [Gcl-devel] #n= etc.
Date: Wed, 29 Jan 2014 09:58:59 -0600

Thanks, Camm.  I've made the appropriate update in ACL2 revision 1227,
documented in the release notes as follows:

  (GCL only) A restriction for structure-sharing (as described in a
  remark, ``Remark on print-circle-files''; see [print-control])
  involving GCL has been removed, since this is no longer required
  for the latest GCL versions (2.6.8 and 2.6.10). Thanks to Jared
  Davis and Camm Maguire for useful discussions and this GCL

-- Matt
   From: Camm Maguire <address@hidden>
   Cc: address@hidden, address@hidden
   Date: Fri, 24 Jan 2014 11:49:30 -0500

   Greetings!  Yes, the updated #= processing is identical in 2.6.8 and
   2.6.10, and should be free from the limitations you describe below.  I
   had to use the old code to bootstrap the system, so its still there in
   the 'pre' image, but all images you would see or use has this
   overwritten with the new stuff.  All structures are dynamically
   allocated with no compile time hard-coded limits.

   Take care,

   Matt Kaufmann <address@hidden> writes:

   > Hi, Camm --
   > Jared Davis reminded me that you did some work to improve the #n=
   > reader in GCL.  In the past we worked around its shortcomings, by
   > avoiding print-circle as in the following comment from the ACL2
   > sources.
   > ; In GCL, at least through Version 2.6.7, there are only 1024 indices n
   > ; available for the #n= reader macro.  That is such a small number that for
   > ; GCL, we turn off the use of this reader macro when printing out files 
such as
   > ; .cert files.
   > We also say the following in the ACL2 User's Manual, topic
   >   .... However, this
   >   behavior is defeated in GCL (Gnu Common Lisp), because of the small
   >   number of indices n available by default (1024) for the #n= reader
   >   macro. For the files described above, what actually happens is that
   >   'print-circle is bound to the value of 'print-circle-files, which
   >   by default is t unless the underlying Lisp is GCL, in which case it
   >   is set to nil. See [assign] for how to set [state] globals such as
   >   'print-circle-files. For example, if you build GCL with a larger
   >   number of #n= indices available, you may wish to restore the
   >   print-circle behavior for [certificate] files by following these
   >   instructions from Camm Maguire:
   >       This can trivially be revised to any larger constant by editing the
   >       following line of read.d and recompiling:
   >       #ifndef SHARP_EQ_CONTEXT_SIZE
   >       #define SHARP_EQ_CONTEXT_SIZE 500
   >       #endif
   > Perhaps all of the above is obsolete, and I should get rid of special
   > treatment related to #n= for GCL.  Do you expect that GCL 2.6.8 and
   > 2.6.10 can handle large numbers of indices for #n=?
   > Thanks --
   > -- Matt

   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]