Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP
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. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP
It works on both my work laptop and my private desktop PC. The work laptop is an Intel i7 something (I cannot recall the exact model off the top of my head) and the desktop is an AMD Ryzen 1800X. Both run with an up-to-date Arch Linux. At least on the desktop, I tried it with both the 32 and 64 bit ML system, and both worked. Manuel On 31/08/2018 23:04, Makarius wrote: > On 31/08/18 22:00, Manuel Eberl wrote: >> >> What puzzles me the most is the fact that this behaviour seems to depend >> on the underlying hardware, and it appears to be 100% reproducible on >> machines where it does happen. If this is a race condition, it must be >> one of the strangest one I have ever seen (note that it even happens in >> single-threaded mode). >> >> Perhaps it might also be of interest to try this with different versions >> of Poly/ML, just to make sure it's not an issue with the underlying ML >> environment. > > I see the same effect with Poly/ML 5.6 from Isabelle2017: a quite > different environment compared to Isabelle2018. > > It requires the included change, and the following in > $ISABELLE_HOME_USER/etc/settings: > > init_component "$HOME/.isabelle/contrib/polyml-5.6-1" > > Moreover, it probably requires this adhoc Unix environment variable: > > export LD_LIBRARY_PATH=$HOME/.isabelle/contrib/polyml-5.6-1/x86-linux > > > This is Ubuntu 16.04.5 LTS on Intel(R) Xeon(R) CPU E5-2620 v3 @ 2.40GHz. > > What is actually your system where it happens to work? > > > Makarius > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP
On 31/08/18 22:00, Manuel Eberl wrote: > > What puzzles me the most is the fact that this behaviour seems to depend > on the underlying hardware, and it appears to be 100% reproducible on > machines where it does happen. If this is a race condition, it must be > one of the strangest one I have ever seen (note that it even happens in > single-threaded mode). > > Perhaps it might also be of interest to try this with different versions > of Poly/ML, just to make sure it's not an issue with the underlying ML > environment. I see the same effect with Poly/ML 5.6 from Isabelle2017: a quite different environment compared to Isabelle2018. It requires the included change, and the following in $ISABELLE_HOME_USER/etc/settings: init_component "$HOME/.isabelle/contrib/polyml-5.6-1" Moreover, it probably requires this adhoc Unix environment variable: export LD_LIBRARY_PATH=$HOME/.isabelle/contrib/polyml-5.6-1/x86-linux This is Ubuntu 16.04.5 LTS on Intel(R) Xeon(R) CPU E5-2620 v3 @ 2.40GHz. What is actually your system where it happens to work? Makarius # HG changeset patch # User wenzelm # Date 1535749047 -7200 # Fri Aug 31 22:57:27 2018 +0200 # Node ID a83229cc624d7236a2ef2158a33be611ae54500e # Parent dd44e31ca2c639b0915695c88020c14f044a73d8 test diff -r dd44e31ca2c6 -r a83229cc624d src/Pure/Concurrent/single_assignment.ML --- a/src/Pure/Concurrent/single_assignment.ML Fri Aug 31 22:25:58 2018 +0200 +++ b/src/Pure/Concurrent/single_assignment.ML Fri Aug 31 22:57:27 2018 +0200 @@ -55,7 +55,7 @@ SOME _ => assign_fail name | NONE => Thread_Attributes.uninterruptible (fn _ => fn () => - (state := Set x; RunCall.clearMutableBit state; ConditionVar.broadcast cond)) (; + (state := Set x; (* RunCall.clearMutableBit state; *) ConditionVar.broadcast cond)) (; end; diff -r dd44e31ca2c6 -r a83229cc624d src/Pure/Concurrent/synchronized.ML --- a/src/Pure/Concurrent/synchronized.ML Fri Aug 31 22:25:58 2018 +0200 +++ b/src/Pure/Concurrent/synchronized.ML Fri Aug 31 22:57:27 2018 +0200 @@ -54,7 +54,7 @@ Immutable _ => immutable_fail name | Mutable _ => Thread_Attributes.uninterruptible (fn _ => fn () => - (state := Immutable x; RunCall.clearMutableBit state; + (state := Immutable x; (* RunCall.clearMutableBit state; *) ConditionVar.broadcast cond)) (; ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP
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. What puzzles me the most is the fact that this behaviour seems to depend on the underlying hardware, and it appears to be 100% reproducible on machines where it does happen. If this is a race condition, it must be one of the strangest one I have ever seen (note that it even happens in single-threaded mode). Perhaps it might also be of interest to try this with different versions of Poly/ML, just to make sure it's not an issue with the underlying ML environment. Manuel On 31/08/2018 21:53, Makarius wrote: > 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=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 > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP
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=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 \ continuous ?F ?g \ continuous ?F (\x. ?f x * ?g x) > continuous ?F ?f \ continuous ?F ?g \ continuous ?F (\x. ?f x ^ ?g x) > continuous_on ?A ?f \ continuous_on ?A ?g \ continuous_on ?A (\x. ?f x * ?g x) > continuous_on ?A ?f \ continuous_on ?A ?g \ continuous_on ?A (\x. ?f x ^ ?g x) > (\i. i \ ?I \ continuous ?F (?f i)) \ continuous ?F (\x. \i\?I. ?f i x) > (\i. i \ ?I \ continuous_on ?S (?f i)) \ continuous_on ?S (\x. \i\?I. ?f i x) ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP
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=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. 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. Manuel On 8/31/18 1:34 AM, Manuel Eberl wrote: > It seems that my latest commit f443ec10447d causes nontermination of the > AFP entry "Green". > > I saw this timeout on the testboard, but everything worked fine locally > despite trying several times, so I thought it was perhaps some spurious > issue and pushed the commit anyway. > > Unfortunately, "Green" seems to time out on Jenkins every time now. > Seeing as a while ago, we had spurious timeout issues that went away > when we increased the timeout, I tried doubling the timeout on the > Testboard (to 20 minutes!) and that did not help either. > > For comparison, on my modest machine, the entry needs a very reasonable > 2 minutes (both CPU and wall clock) when run with 1 thread, so >20 > minutes seems quite absurd. > > I looked at the entry in Isabelle/jEdit and found some invocations of > blast/force that took up to 8 seconds, but that should not be a problem. > > Does anyone have any idea what is going on here or how I could track > down this issue? > > Manuel > > > Forwarded Message > Subject: [Isabelle-ci] Build failure in AFP > Date: Thu, 30 Aug 2018 22:53:44 +0200 (CEST) > From: Isabelle/Jenkins > To: isabelle...@mail46.informatik.tu-muenchen.de > > The AFP build failed. See the log at: > https://ci.isabelle.systems/jenkins/job/isabelle-all/288/ > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
