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

On 04/02/2021 09:09, Jasmin Blanchette wrote:
>> The quoted changeset says:
>> changeset:   72347:478b7599a1a0
>> parent:      72342:4195e75a92ef
>> user:        desharna
>> date:        Wed Sep 30 18:37:22 2020 +0200
>> files:       src/HOL/SMT.thy src/HOL/Tools/SMT/smt_config.ML
>> description:
>> Effectively disable timeout for smt method/tactic
>> The log does not provide any explanation.
> The idea came from me. Having a tactic operate with a timeout seems quite fragile. This adds a layer of randomness to Isabelle. In each AFP entry's ROOT file, there's a timeout for the entire session, which is a good practical compromise, but if we start having timeouts in every individual tactic, we might get all sorts of random failures. Other tactics like "auto" or "metis" don't have timeout.
> 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.

For my part, it is formally OK to do nothing for the release.

It is up to the SMT + veriT experts to say if there is something severely
wrong that needs to be changed for the Isabelle2021 release. RC5 is planned
for 08-Feb-2021. The final release approx. 1 week later.


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