[isabelle-dev] Nontermination in HOL-Corec_Examples on Epyc

Lars Hupel hupel at in.tum.de
Mon Jun 25 17:08:13 CEST 2018

> I think it works properly now, see Isabelle/f0f83ce0badd + AFP/f7e9efc65d82.

Thanks for that. I'll proceed with the systems integration process of
that machine now.

> I usually measure the CPU time, multiply it by 2, and take the ceiling
> towards the next multiple of 300. In principle this maintenance of
> options could be automated.

The "multiple of 300" part is now implemented in "afp_check_roots"


More information about the isabelle-dev mailing list