Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP
I've removed the two rules from continuous_intros as of 1254f3e57fed. Manuel On 07/09/2018 14:56, Makarius wrote: > On 02/09/18 16:00, Manuel Eberl wrote: >> Okay I did some more experiments and I was now, interestingly enough, >> completely unable to reproduce the situation where Green /didn't/ >> timeout. So I have no idea what was going on there; perhaps I made a >> mistake in testing it. I don't know. >> >> It might be wise to remove "continuous_on_discrete" etc. from >> intro/continuous_intros and declare it as a simp rule instead. I'm still >> not quite sure what causes these problems. > The official isabelle-dev test results show that Ergodic_Theory and Lp > have suffered a lot: > > https://isabelle.sketis.net/devel/build_status/AFP/index.html#session_Ergodic_Theory > https://isabelle.sketis.net/devel/build_status/AFP/index.html#session_Lp > > > Here are some manual measurements: > > Isabelle/9207ada0ca31 + AFP/6d7e0f6b8096 > Finished HOL (0:03:18 elapsed time, 0:11:01 cpu time, factor 3.33) > Finished HOL-Analysis (0:05:44 elapsed time, 0:26:07 cpu time, factor 4.55) > Finished HOL-Probability (0:01:15 elapsed time, 0:05:25 cpu time, factor > 4.30) > Finished Lp (0:00:15 elapsed time, 0:01:03 cpu time, factor 4.21) > > Isabelle/f443ec10447d + AFP/6d7e0f6b8096 > Finished HOL (0:03:19 elapsed time, 0:11:03 cpu time, factor 3.33) > Finished HOL-Analysis (0:05:58 elapsed time, 0:27:06 cpu time, factor 4.54) > Finished HOL-Probability (0:01:16 elapsed time, 0:05:24 cpu time, factor > 4.22) > Finished Lp (0:02:41 elapsed time, 0:03:42 cpu time, factor 1.38) > > > So it is probably better to revise the rule declarations in main HOL. > > > Makarius pEpkey.asc Description: application/pgp-keys ___ 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 02/09/18 16:00, Manuel Eberl wrote: > Okay I did some more experiments and I was now, interestingly enough, > completely unable to reproduce the situation where Green /didn't/ > timeout. So I have no idea what was going on there; perhaps I made a > mistake in testing it. I don't know. > > It might be wise to remove "continuous_on_discrete" etc. from > intro/continuous_intros and declare it as a simp rule instead. I'm still > not quite sure what causes these problems. The official isabelle-dev test results show that Ergodic_Theory and Lp have suffered a lot: https://isabelle.sketis.net/devel/build_status/AFP/index.html#session_Ergodic_Theory https://isabelle.sketis.net/devel/build_status/AFP/index.html#session_Lp Here are some manual measurements: Isabelle/9207ada0ca31 + AFP/6d7e0f6b8096 Finished HOL (0:03:18 elapsed time, 0:11:01 cpu time, factor 3.33) Finished HOL-Analysis (0:05:44 elapsed time, 0:26:07 cpu time, factor 4.55) Finished HOL-Probability (0:01:15 elapsed time, 0:05:25 cpu time, factor 4.30) Finished Lp (0:00:15 elapsed time, 0:01:03 cpu time, factor 4.21) Isabelle/f443ec10447d + AFP/6d7e0f6b8096 Finished HOL (0:03:19 elapsed time, 0:11:03 cpu time, factor 3.33) Finished HOL-Analysis (0:05:58 elapsed time, 0:27:06 cpu time, factor 4.54) Finished HOL-Probability (0:01:16 elapsed time, 0:05:24 cpu time, factor 4.22) Finished Lp (0:02:41 elapsed time, 0:03:42 cpu time, factor 1.38) So it is probably better to revise the rule declarations in main HOL. 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
This trace doesn’t tell us much because it’s only blast’s internal search. Looks like every “continuous_on” goal is immediately solved. But after this search exits, the reconstructed Isabelle proof will fail. Blast will re-enter but it will only find these unsound proofs, and probably won’t ever terminate. Larry > On 2 Sep 2018, at 15:00, Manuel Eberl wrote: > > Okay I did some more experiments and I was now, interestingly enough, > completely unable to reproduce the situation where Green /didn't/ > timeout. So I have no idea what was going on there; perhaps I made a > mistake in testing it. I don't know. > > It might be wise to remove "continuous_on_discrete" etc. from > intro/continuous_intros and declare it as a simp rule instead. I'm still > not quite sure what causes these problems. I attached a log of blast > with "blast_trace" enabled. > > Manuel > > On 01/09/2018 14:20, Makarius wrote: >> This thread consists of two sub-threads. The hardware / OS question >> still needs to be sorted out: it might be something with Arch Linux. >> >> Apart from that, my reading of blast.ML is that the "continuous_on" rule >> is applied in the search independently of its fine-grained type >> information. Is that correct? >> >> >> Makarius >> >> >> On 01/09/18 13:19, Lawrence Paulson wrote: >>> Surely the main issue that blast somehow behaves differently depending upon >>> which machine it’s running on? >>> >>> Larry >>> On 31 Aug 2018, at 22:35, Makarius 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. > ___ 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
Okay I did some more experiments and I was now, interestingly enough, completely unable to reproduce the situation where Green /didn't/ timeout. So I have no idea what was going on there; perhaps I made a mistake in testing it. I don't know. It might be wise to remove "continuous_on_discrete" etc. from intro/continuous_intros and declare it as a simp rule instead. I'm still not quite sure what causes these problems. I attached a log of blast with "blast_trace" enabled. Manuel On 01/09/2018 14:20, Makarius wrote: > This thread consists of two sub-threads. The hardware / OS question > still needs to be sorted out: it might be something with Arch Linux. > > Apart from that, my reading of blast.ML is that the "continuous_on" rule > is applied in the search independently of its fine-grained type > information. Is that correct? > > > Makarius > > > On 01/09/18 13:19, Lawrence Paulson wrote: >> Surely the main issue that blast somehow behaves differently depending upon >> which machine it’s running on? >> >> Larry >> >>> On 31 Aug 2018, at 22:35, Makarius 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. [0] ¬ (continuous_on S (λx. (f x, g x)) ∧ (∃Sa. finite Sa ∧ (λx. (?etc, ?etc)) C1_differentiable_on S - Sa)) :: bool ⇒ bool branch split: 2 new subgoals + [0] ¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool moving formula to unsafe list + [0] ¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool (Unsafe) Limit reached. Backtracking; now there are 1 branches Backtracking; now there are 1 branches [1] ¬ (continuous_on S (λx. (f x, g x)) ∧ (∃Sa. finite Sa ∧ (λx. (?etc, ?etc)) C1_differentiable_on S - Sa)) :: bool ⇒ bool branch split: 2 new subgoals + [1] ¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool moving formula to unsafe list + [1] ¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool (Unsafe) branch closed by rule (duplicating) [1] ∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool moving formula to unsafe list [1] ∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe) branch extended (1 new subgoal) (duplicating) [0] ¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool branch split: 2 new subgoals + [0] ¬ finite ?var :: bool ⇒ bool branch closed by rule 1 variable UPDATED: set_mset ?var [0] ¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool moving formula to literals [0] ∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe) Limit reached. Backtracking; now there are 2 branches branch closed by rule 1 variable UPDATED: set ?var [0] ¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool moving formula to literals [0] ∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe) Limit reached. Backtracking; now there are 2 branches branch closed by rule 1 variable UPDATED: bot [0] ¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool moving formula to literals [0] ∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe) Limit reached. Backtracking; now there are 2 branches branch extended (1 new subgoal) 1 variable UPDATED: ?var - insert ?var ?var Excessive branching: KILLED moving formula to unsafe list + [0] ¬ finite ?var :: bool ⇒ bool (Unsafe) Limit reached. Backtracking; now there are 1 branches Backtracking; now there are 1 branches Backtracking; now there are 2 branches Backtracking; now there are 1 branches Backtracking; now there are 1 branches [2] ¬ (continuous_on S (λx. (f x, g x)) ∧ (∃Sa. finite Sa ∧ (λx. (?etc, ?etc)) C1_differentiable_on S - Sa)) :: bool ⇒ bool branch split: 2 new subgoals + [2] ¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool moving formula to unsafe list + [2] ¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool (Unsafe) branch closed by rule (duplicating) [2] ∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool moving formula to unsafe list [2] ∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe) branch extended (1 new subgoal) (duplicating) [1] ¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool branch split:
Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP
It’s important to understand that blast knows nothing about type classes. This isn’t a problem for rules like order_trans, where the type class constraint would be satisfied in most cases. But it’s fatal for continuous_on_discrete: it will succeed in all cases, but if the type class constraint isn’t satisfied (and it usually won’t be), then the proof will fail and it’s not clear that backtracking will find an alternative. The PROOF FAILED message (if it still exists) alerts us to this. Larry > On 1 Sep 2018, at 13:39, Manuel Eberl wrote: > >> This thread consists of two sub-threads. The hardware / OS question >> still needs to be sorted out: it might be something with Arch Linux. > > I don't really have much of an opportunity to test this on other systems > atm, but I'll see what I can do. > >> Apart from that, my reading of blast.ML is that the "continuous_on" rule >> is applied in the search independently of its fine-grained type >> information. Is that correct? > > Even if it is, it has no preconditions, so I don't see how it could > cause nontermination. > > Manuel ___ 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 01/09/18 14:39, Manuel Eberl wrote: >> This thread consists of two sub-threads. The hardware / OS question >> still needs to be sorted out: it might be something with Arch Linux. > > I don't really have much of an opportunity to test this on other systems > atm, but I'll see what I can do. > >> Apart from that, my reading of blast.ML is that the "continuous_on" rule >> is applied in the search independently of its fine-grained type >> information. Is that correct? > > Even if it is, it has no preconditions, so I don't see how it could > cause nontermination. This is where Larry could take a closer look. The argument ?f of function type (with sort constraints) looks like a candidate for unexpected problems. 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
> This thread consists of two sub-threads. The hardware / OS question > still needs to be sorted out: it might be something with Arch Linux. I don't really have much of an opportunity to test this on other systems atm, but I'll see what I can do. > Apart from that, my reading of blast.ML is that the "continuous_on" rule > is applied in the search independently of its fine-grained type > information. Is that correct? Even if it is, it has no preconditions, so I don't see how it could cause nontermination. Manuel ___ 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
This thread consists of two sub-threads. The hardware / OS question still needs to be sorted out: it might be something with Arch Linux. Apart from that, my reading of blast.ML is that the "continuous_on" rule is applied in the search independently of its fine-grained type information. Is that correct? Makarius On 01/09/18 13:19, Lawrence Paulson wrote: > Surely the main issue that blast somehow behaves differently depending upon > which machine it’s running on? > > Larry > >> On 31 Aug 2018, at 22:35, Makarius 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. ___ 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
Surely the main issue that blast somehow behaves differently depending upon which machine it’s running on? Larry > On 31 Aug 2018, at 22:35, Makarius 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. > > > 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: > 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
