[isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP
lp15 at cam.ac.uk
Sat Sep 1 13:19:54 CEST 2018
Surely the main issue that blast somehow behaves differently depending upon which machine it’s running on?
> 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.
More information about the isabelle-dev