Creating one umbrella issue for SBCL memouts, heap exhaustions, follow-on corruptions, and anything that drops you into ldb.
Can be caused by any of (1) parsing large PVS files (2) typechecking large/weird specs (3) proving hard stuff (4) translating huge specs into Lisp/C (5) all sorts of things because PVS does a lot.
We should see whether issues are on the PVS side or SBCL compiler issues and report them appropriately.
Note that there is no monotonicity: later versions of SBCL may have more/new memory leaks/issues than prior ones.
Among other solutions/band-aids, we might want to look into smarter GC mechanisms.
Creating one umbrella issue for SBCL memouts, heap exhaustions, follow-on corruptions, and anything that drops you into
ldb.Can be caused by any of (1) parsing large PVS files (2) typechecking large/weird specs (3) proving hard stuff (4) translating huge specs into Lisp/C (5) all sorts of things because PVS does a lot.
We should see whether issues are on the PVS side or SBCL compiler issues and report them appropriately.
Note that there is no monotonicity: later versions of SBCL may have more/new memory leaks/issues than prior ones.
Among other solutions/band-aids, we might want to look into smarter GC mechanisms.