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



> 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.

Jasmin





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