Re: [isabelle] Isabelle2021-RC1 - Any way to limit "veriT" memory use?



Hi,
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.)

Best wishes,
Dominique.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.