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

[Makarius]

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:
https://github.com/polyml/polyml/commit/86c52cbd8f6d

I have updated the polyml component accordingly in Isabelle/1b8457cc4de8.

So far it looks good, but we still need to test all of AFP.


	Makarius