[isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP
makarius at sketis.net
Fri Aug 31 21:53:40 CEST 2018
On 31/08/18 15:06, Manuel Eberl wrote:
> Update: I pushed another changeset and now everything is green again (if
> you excuse the pun).
> I tracked the problem to a diverging invocation of "blast":
> However, this "blast" does not diverge on any of my machines, no matter
> if single-threaded or multi-threaded, no matter if "isabelle build" or
> Isabelle/jEdit. It actually terminates almost instantaneously.
> It does, however, seem to diverge reliably on the Testboard, on the
> workermtahpc, and on isabelle-server. I found this "blast" invocation by
> running "isabelle jedit" on isabelle-server via XForwarding, and there
> it was continuously purple and remained purple forever.
This is indeed a bit strange. Apart from the various AMD machines above,
I see the same effect on my own Intel Xeon E5-2620 v3.
> I have no idea why it does that; the proof in question is actually very
> simple. It does use "continuous_intros" and my changeset does introduce
> a few new "continuous_intros" rules and also some "intro" rules, but
> none of them match the goal here at all, so I cannot see how that would
> influence anything. And I am certainly stumped as to how this kind of
> non-deterministic behaviour could come about.
A diff of the two versions of continuous_intros produces the included
The first rule "continuous_on ?A ?f" is continuous_on_discrete, and
removing is already sufficient to recover the original proof:
supply [continuous_intros del] = continuous_on_discrete
by (blast intro!: continuous_intros C1_differentiable_on_pair intro:
C1_differentiable_on_subset elim: )
This finishes in 0.250s on my Intel Xeon.
It would be still nice to understand the problem: maybe something odd
with higher-order unification, or the unification within blast.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 831 bytes
Desc: not available
More information about the isabelle-dev