[isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP
Manuel Eberl
eberlm at in.tum.de
Sat Sep 1 14:39:55 CEST 2018
> 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.
Manuel
More information about the isabelle-dev
mailing list