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":
> https://bitbucket.org/isa-afp/afp-devel/src/e15414dceb2836d07d50546ee94ff8083fbcc80d/thys/Green/Derivs.thy?at=default&fileviewer=file-view-default#Derivs.thy-165
> 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.

>   continuous_on ?A ?f
>   continuous (at ?x within ?A) ?f
>   continuous ?F ?f \<Longrightarrow> continuous ?F ?g \<Longrightarrow> continuous ?F (\<lambda>x. ?f x * ?g x)
>   continuous ?F ?f \<Longrightarrow> continuous ?F ?g \<Longrightarrow> continuous ?F (\<lambda>x. ?f x ^ ?g x)
>   continuous_on ?A ?f \<Longrightarrow> continuous_on ?A ?g \<Longrightarrow> continuous_on ?A (\<lambda>x. ?f x * ?g x)
>   continuous_on ?A ?f \<Longrightarrow> continuous_on ?A ?g \<Longrightarrow> continuous_on ?A (\<lambda>x. ?f x ^ ?g x)
>   (\<And>i. i \<in> ?I \<Longrightarrow> continuous ?F (?f i)) \<Longrightarrow> continuous ?F (\<lambda>x. \<Prod>i\<in>?I. ?f i x)
>   (\<And>i. i \<in> ?I \<Longrightarrow> continuous_on ?S (?f i)) \<Longrightarrow> continuous_on ?S (\<lambda>x. \<Prod>i\<in>?I. ?f i x)
isabelle-dev mailing list

Reply via email to