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

Makarius 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
>> terminates
> 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 mailing list