[isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP

[Makarius]

On 01/09/18 14:39, Manuel Eberl wrote:
>> This thread consists of two sub-threads. The hardware / OS question
>> still needs to be sorted out: it might be something with Arch Linux.
> 
> I don't really have much of an opportunity to test this on other systems
> atm, but I'll see what I can do.
> 
>> Apart from that, my reading of blast.ML is that the "continuous_on" rule
>> is applied in the search independently of its fine-grained type
>> information. Is that correct?
> 
> Even if it is, it has no preconditions, so I don't see how it could
> cause nontermination.

This is where Larry could take a closer look. The argument ?f of
function type (with sort constraints) looks like a candidate for
unexpected problems.


	Makarius