resizing the SBCL call stack

[Mark Tarver]

I'm doing some heavy theorem proving and once again pushing the

limits of the SBCL call stack.  Is there any convenient way of resizing this?

Mark

[Bruno Deferrari]

I don't know of a way to do it at runtime, but when building the image you can use --control-stack-size SIZE (SIZE is in megabytes, default is 2, you can try 8)

https://www.sbcl.org/manual/#Runtime-Options-1

--
You received this message because you are subscribed to the Google Groups "Shen" group.
To unsubscribe from this group and stop receiving emails from it, send an email to qilang+un...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/qilang/6297fac0-9973-415a-a284-c4582723f2fdn%40googlegroups.com.

--

BD

[Bruno Deferrari]

Oh, one more important detail, I see that in SP one option is missing when creating the executable, you need to add this:

:save-runtime-options t

to the save-lisp-and-die call.

--

BD

[Mark Tarver]

ah, OK.  I'd used sbcl.exe sbcl --control-stack-size 50 --dynamic-space-size 100 --core sbcl.core

on startup but assumed these changes would be saved to the image.  Thx.

BTW I'm testing a new version of the FTP for general release.  Would you be interested in testing this 

under Scheme?

Mark

To view this discussion on the web, visit https://groups.google.com/d/msgid/qilang/CACnPB4re%2BUQgR4x3ycbz4SveNEb0sJJxxvRAReT%3Dk-NEPA3qAw%40mail.gmail.com.

[Mark Tarver]

Um; even with the new settings there is a crash.   Rethinking ..

M.

[Mark Tarver]

Compiling large axiom sets under SBCL/Shen is proving a problem; it is not a program bug

but due to my inability to configure SBCL.  

I'm testing Bruno's Scheme installation.

Mark

[Bruno Deferrari]

On Fri, Sep 2, 2022 at 10:04 AM Mark Tarver <dr.mt...@gmail.com> wrote:

ah, OK.  I'd used sbcl.exe sbcl --control-stack-size 50 --dynamic-space-size 100 --core sbcl.core

on startup but assumed these changes would be saved to the image.  Thx.

BTW I'm testing a new version of the FTP for general release.  Would you be interested in testing this 

under Scheme?

Sure, although I see you have done some tests already. Is there anything in particular you would like to see tested?

I am not familiar with the FTP code and how it runs, but could it be that the issue is not so much the stack limit but that SBCL is not optimizing tail-calls while Scheme is?

 

To view this discussion on the web, visit https://groups.google.com/d/msgid/qilang/CAGp%3DqtT81a6oYCsPXsFaPLhuc7ZVvr-1uOzWMmTZxtpZ4v6bTA%40mail.gmail.com.

--

BD

[Mark Tarver]

Yes; I think I answered my own question, thanks to your handy installation.

I'm not certain exactly what has to be done to SBCL to make it work here.  The issue arises with the Prolog

code which constructs the proofs.    These proofs can be very large; one such is 2,357 lines long, takes a

68K file and consists of 280 steps.    This blew SBCL.

The modus operandus is that the Prolog constructs a proof by search which is stored as a precis in a

variable Prf.  The search is repeated on the same problem with the value of Prf fixed which means

that the full proof is reconstructed in linear time w.o. search.    This 'double jeopardy' approach blew

SBCL.

Mark

[nha...@gmail.com]

I had problems with this before, which is one of the reasons I stopped using the SBCL port.

It was with some continuation passing style code IIRC.