Re: [isabelle] Isabelle2021-RC1 - Any way to limit "veriT" memory use?
If this is the only or best way to reduce veriT's memory usage, we could consider reverting 478b7599a1a0, but this seems dubious to me.
Perhaps a compromise would be to activate timeouts only for the
interactive session? I find that the most annoying thing about timeouts
is that they can make a build of large heaps fail because the computer
goes into swapping. While in the interactive session, timeouts could be
nice so that the computer does not go into expensive infinite loops when
something changes during editing. And since the interactive session is
usually edited by the same person who inserts the timeout, it's then up
to each person whether they want to use a timeout or not. (And
unpredictability is less of a problem during the interactive editing.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and