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
a.patch
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.
Makarius
31a32
> continuous_on ?A ?f
35a37
> continuous (at ?x within ?A) ?f
71a74,79
> 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
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
