[isabelle-dev] Nontermination in HOL-Corec_Examples on Epyc
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