Greetings!
Normally compiled object modules (".o" files) by gcc follow the 'medium'
memory model assumptions, and must be loaded within a limited range of
the base image (typically 2GB). GCL has several ways to work around
this:
1) If a large heap is not needed, the total size can be limited at
runtime via the environment variable GCL_MEM_MULTIPLE
2) (progn (setq si::*code-block-reserve* (make-array 50000000
:element-type 'character :static t)) nil) will allocate 50Mb for code
early on in a low address range before the heap grows out of range.
3) :large-memory-model t arguments to compile file (alternatively
compiler::*default-large-memory-model-p* setting) will produce .o files
which can be loaded at all addresses at a performance cost of about 10%.
I would suggest estimating your code size needs and using 2) in the
acl2 build stage.
Take care,
Matt Kaufmann <[email protected]> writes:
> Hi Camm,
>
> When I built ACL2 with GCL 2.6.14 on my Mac and then ran
>
> (time make proofs LISP=my-fast-gcl) >& make-proofs.log&
>
> where my-fast-gcl points to a script with
>
> gcl -eval "(defparameter user::*fast-acl2-gcl-build* t)" "$@"
>
> then I got this error.
>
> ~/acl2/acl2$ tail -20 make-proofs.log
>
> ACL2 loading '((COMP-FN :EXEC NIL "1" STATE)).
> ACL2 !>(COMP-FN :EXEC NIL "1" STATE)
>
> Error:
> Fast links are on: do (si::use-fast-links nil) for debugging
> Signalled by INITIALIZE-ACL2.
>
> Raw Lisp Break.
> Condition in INITIALIZE-ACL2 [or a callee]: INTERNAL-SIMPLE-ERROR: The
> assertion ovchk(v,~m) on line 61 of
> /Users/kaufmann/lisps/gcl/gcl-2.6.14/o/sfaslmacho.c in function store_val
> failed: Undefined error: 0
>
> Broken at APPLY. Type :H for Help.
> 1 Return to top level.
> ACL2>>Initialization FAILED: acl2-status.txt should contain :INITIALIZED.
> make[1]: *** [check_init_ok] Error 1
> make: *** [proofs] Error 2
>
> real 14m13.032s
> user 10m39.508s
> sys 2m35.435s
> ~/acl2/acl2$
>
> I'm probably going to start my release process for ACL2 Version 8.6
> shortly. I did a successful regression on my Mac with GCL 2.6.12
> (which also had the "make proofs" problem), and users don't do
> "make proofs", and I can do that with other Lisps -- so I don't feel
> the need to wait for a fix. But I thought I should let you know.
>
> Oh, and regarding my previous question: I no longer need to
> be able to tell how many arguments c2call-local has in
> a given GCL
>
> -- Matt
>
> On Wed, Oct 2, 2024 at 11:00 AM Matt Kaufmann <[email protected]>
> wrote:
>
> Hi Camm,
>
> Is there an easy way to tell how many arguments c2call-local has in
> a given GCL? I think your implicit point earlier was that even "2.6.12" can
> be such that sometimes that function has 2 arguments and sometimes
> it has 4.
>
> Thanks,
> Matt
>
> On Wed, Oct 2, 2024 at 10:55 AM Matt Kaufmann <[email protected]>
> wrote:
>
> Good question on gcl27. I just checked, and apparently my last successful
> gcl build was many months ago, and maybe not with 2.7.0. Sorry!
> -- Matt
>
> On Wed, Oct 2, 2024 at 10:31 AM Camm Maguire <[email protected]> wrote:
>
> Greetings again! And just confirming you did have a successful gcl27
> build before a few days ago on this same tree....
>
> Take care,
>
> Matt Kaufmann <[email protected]> writes:
>
> > Hi Camm,
> >
> > I've never seen that error. I wonder if call-argument-limit is
> > somehow being applied to let* where before it was only applied to
> > function calls.
> >
> > Thanks for your two suggested fixes. Since GCL 2.6.12 is quite old
> > now, and I already tried to condition the installation of
> > c2funcall-new as c2funcall (see the WHEN form just below the
> > definition of c2funcall-new), then unless you have a better idea, I'll
> > probably just remove that code.
> >
> > I was able to build ACL2 successfully and run a regression without any
> > GCL problems, using /projects/acl2/lisps/gcl/gcl-2.6.14/bin/gcl. So I
> > have that as a backup, which makes 2.7.0 less urgent for me.
> >
> > Thanks,
> > Matt
> >
> > On Wed, Oct 2, 2024 at 8:24 AM Camm Maguire <[email protected]> wrote:
> >
> > Greetings! /p/bin/gcl27 has been updated and the issue you raised
> > removed. But at least on the master branch of acl2 I now get:
> >
> > Raw Lisp Break.
> > Condition in LET* [or a callee]: INTERNAL-SIMPLE-PROGRAM-ERROR: LET* [or
> a callee] requires less than one hundred forty-eight arguments.
> >
> > Was this issue not there before yesterday? Are you working with a
> > different branch? call-arguments-limit in GCL has always been ~64.
> >
> > Take care,
> >
> > Camm Maguire <[email protected]> writes:
> >
> > > Greetings!
> > >
> > > Please accept my apologies -- I was unaware of your release schedule and
> > > under the impression that no intrepid soul would attempt this build
> > > until I got around to testing in in the space you so graciously
> > > provided. That said it is very good news that it is working for you.
> > >
> > > I will be installing "git: Version_2_7_0pre28" in a few hours to address
> > > the issue you found.
> > >
> > > Separately, I suggest:
> > >
> > > #+gcl
> > > (declaim (ftype (function (si::seqind t) t) si::set-mv))
> > >
> > > in init.lisp, as 'si is the homepackage of 'seqind, and
> > > perhaps conditionalizing he c2funcall-new definition function itself by
> > > gcl version (if possible), as the call to c2call-local requires 4
> > > arguments in later gcl versions. This is only cosmetic to avoid
> > > needless warnings, as the code of course is not used in recent gcl
> > > versions.
> > >
> > > I will henceforward ensure /p/bin/gcl27 introduces no new acl2 problems
> > > without first coordinating with you.
> > >
> > > Take care,
> > >
> > > Matt Kaufmann <[email protected]> writes:
> > >
> > >> Hi Camm,
> > >>
> > >> A moment ago an ACL2 build at UT CS failed using /p/bin/gcl27,
> although that
> > >> has worked fine in the past. I've attached both a shell log (log.txt)
> that has
> > >> all the information you need to reproduce the problem, as well as the
> > >> output log (make.log) from the attempted build. I was planning to
> start testing
> > >> for a release in the next few days, so if you can't get this working
> soon,
> > >> could you restore the /p/bin/gcl27 that was there till recently
> (perhaps in a
> > >> different location)?
> > >>
> > >> Thanks,
> > >> Matt
> > >>
> > >> On Tue, Oct 1, 2024 at 9:46 PM Camm Maguire <[email protected]>
> wrote:
> > >>
> > >> Greetings, and so lovely to here from you!
> > >>
> > >> I agree about the bug and will commit this shortly:
> > >>
> > >> modified gcl/lsp/gcl_seqlib.lsp
> > >> @@ -381,8 +381,7 @@
> > >> (string (sort sequence predicate :key key))
> > >> (bit-vector (sort sequence predicate :key key))
> > >> (otherwise
> > >> - (coerce (list-merge-sort (coerce sequence 'list) predicate key)
> > >> - (seqtype sequence)))))
> > >> + (replace sequence (list-merge-sort (coerce sequence 'list)
> predicate key)))))
> > >>
> > >> (eval-when (compile eval)
> > >> (defmacro f+ (x y) `(the fixnum (+ (the fixnum ,x) (the fixnum
> ,y))))
> > >>
> > >> Implementing vector-merge-sort with displaced arrays is a future
> > >> improvement. Incorporating your file even more so! I've downloaded
> it
> > >> and am investigating....
> > >>
> > >> You may be interested to check out /p/bin/gcl27 at ut. I've just
> > >> refreshed it. This is pre-release, the chief release obstacle being
> > >> compiler speed. Notably type inferencing on nested loops is
> exponential
> > >> in the number of loops at present. I am in dialogue with some cmucl
> > >> compiler developers on a possible better course, but I don't see the
> > >> solution yet. This being said, essentially all of the improvements we
> > >> worked on long ago are incorporated here, which I can detail to
> refresh
> > >> your memory if desired. All ansi tests pass. Getting this release
> > >> worthy is on my bucket list.
> > >>
> > >> Take care,
> > >>
> > >> Robert Boyer <[email protected]> writes:
> > >>
> > >> > Dear Camm,
> > >> >
> > >> > I cannot express how pleased I am that I can do sudo get-apt
> install acl2!
> > >> >
> > >> > I think there might be a bug in GCL's stable-sort, at least with
> respect to
> > >> > the ANSI standard.
> > >> >
> > >> > >(setq foo #(("foo" . 1) ("bar" . 2)))
> > >> >
> > >> > #(("foo" . 1) ("bar" . 2))
> > >> >
> > >> > >(stable-sort foo 'string< :key 'car)
> > >> >
> > >> > #(("bar" . 2) ("foo" . 1))
> > >> >
> > >> > >foo
> > >> >
> > >> > #(("foo" . 1) ("bar" . 2))
> > >> >
> > >> > >
> > >> >
> > >> > I think that stable-sort is intended to smash its first arg.
> > >> >
> > >> > http://clhs.lisp.se/Body/f_sort_.htm#stable-sort
> > >> >
> > >> > says
> > >> >
> > >> > sort and stable-sort destructively sort sequences according to the
> order
> > >> > determined by the predicate function.
> > >> >
> > >> > By the way, I highly recommend that you consider the file
> 'nms.lisp' on my working directory, below, as a replacement for
> > >> > stable-sort in gcl. The function 'msa' is 3 times faster than
> SBCL's stable sort. I intend it to be a complete
> > >> > 'drop-in' replacement for stable-sort in Common Lisp, so let me
> know if you determine the slightest flaw in it, however tiny.
> > >> >
> > >> > With Highest Regards,
> > >> >
> > >> > Bob
> > >> >
> > >> > Here is my working directory:
> > >> >
> https://drive.google.com/drive/folders/1UoCT8YaisJBE-deMYJ8n1VE1rNg6K_MW?usp=drive_link
> > >> >
> > >> > The file 0README.txt has more about me than you probably care to
> know.
> > >> >
> > >> > ... to take away the possibility of the vision of the divine
> essence by man is to take away happiness itself. Aquinas, Com. John, Ch 1 Lec
> 11 Sct 212 p 102.
> > >> >
> > >> > Bob Morris (then chief scientist of the National Computer Security
> Center of the NSA) said: ``To a first approximation, every computer in the
> world is connected with every other computer.''
> > >> >
> > >> > Could an explanation for the irrational support for Trump be
> addiction? I know of no cure for addiction.
> > >> >
> > >> > Any piece of computer software is nothing but an integer. It is
> clearly unconstitutional, under the First Amendment, for the US government to
> ban the publication of an integer.
> > >> >
> > >> > Therefore Mind thinks itself, if it is that which is best; and its
> thinking is a thinking of thinking. -- Aristotle
> > >> >
> > >>
> > >> --
> > >> Camm Maguire
> [email protected]
> > >>
> ==========================================================================
> > >> "The earth is but one country, and mankind its citizens." --
> Baha'u'llah
> > >>
> > >>
> > >>
> >
> > --
> > Camm Maguire [email protected]
> > ==========================================================================
> > "The earth is but one country, and mankind its citizens." -- Baha'u'llah
> >
>
> --
> Camm Maguire [email protected]
> ==========================================================================
> "The earth is but one country, and mankind its citizens." -- Baha'u'llah
>
--
Camm Maguire [email protected]
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah
