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

[Lawrence Paulson]

This trace doesn’t tell us much because it’s only blast’s internal search. Looks like every “continuous_on” goal is immediately solved. But after this search exits, the reconstructed Isabelle proof will fail. Blast will re-enter but it will only find these unsound proofs, and probably won’t ever terminate.
Larry

> On 2 Sep 2018, at 15:00, Manuel Eberl <eberlm at in.tum.de> wrote:
> 
> Okay I did some more experiments and I was now, interestingly enough,
> completely unable to reproduce the situation where Green /didn't/
> timeout. So I have no idea what was going on there; perhaps I made a
> mistake in testing it. I don't know.
> 
> It might be wise to remove "continuous_on_discrete" etc. from
> intro/continuous_intros and declare it as a simp rule instead. I'm still
> not quite sure what causes these problems. I attached a log of blast
> with "blast_trace" enabled.
> 
> Manuel
> 
> On 01/09/2018 14:20, Makarius 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.
>> 
>> 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?
>> 
>> 
>> 	Makarius
>> 
>> 
>> On 01/09/18 13:19, Lawrence Paulson wrote:
>>> Surely the main issue that blast somehow behaves differently depending upon which machine it’s running on?
>>> 
>>> Larry
>>> 
>>>> On 31 Aug 2018, at 22:35, Makarius <makarius at sketis.net> wrote:
>>>> 
>>>> On 31/08/18 22:00, Manuel Eberl wrote:
>>>>> That's interesting. I suspected one of the "continuous_on" rules would
>>>>> be the cause. In any case, I don't know how the unification works
>>>>> exactly w.r.t. sorts, but the "continuous_on_discrete" rule does not
>>>>> apply to this goal at all due to its restrictive type class constraint.
>>>> Blast does its own unification, without taking fully account of types
>>>> and type classes. The found proof is then reconstructed as in "fast" and
>>>> its friends, using regular Isabelle term + type unification.
>>>> 
>>>> Larry should be able to say more precisely, what the limits of blast are.
> <log.txt><pEpkey.asc>