[isabelle-dev] Nontermination in HOL-Corec_Examples on Epyc
makarius at sketis.net
Thu Jun 21 00:11:15 CEST 2018
On 18/06/18 22:38, Makarius wrote:
> On 18/06/18 21:30, Lars Hupel wrote:
>> The precise invocation is:
>> $ ./isabelle/bin/isabelle build -cbv -a -o threads=2 -j 16
>> - The "poly" process gets stuck at 100% CPU load and keeps calling "mmap"
>> - When trying to build the nonterminating session without "-b", it
> David Matthews is the only one who can address this.
David has worked rather quickly and produced the following commit:
I have updated the polyml component accordingly in Isabelle/1b8457cc4de8.
So far it looks good, but we still need to test all of AFP.
More information about the isabelle-dev