Re: [isabelle-dev] Final consolidation for Isabelle2018-RC2
On 19/07/18 13:42, Tobias Nipkow wrote: > I have the same problem, and on my machine it is reproduceable (and it > did not go away over the past week, although I tried different versions > of the devel repository). However, I cannot reproduce the problem on > testboard. > > Tobias > > On 18/07/2018 17:05, Manuel Eberl wrote: >> I had what seems to be a spurious failure of >> Probabilistic_Timed_Automata yesterday: >> https://ci.isabelle.systems/jenkins/job/testboard/50/consoleFull >> >> The error message is: >> >> *** exception THM 0 raised (line 1136 of "thm.ML"): generalize: bad index The problem occurs with forked proofs in the context of "subgoal premises" with maxidx >= 0. It is difficult to reproduce in batch builds, because the default parallel_proofs = 1 does not fork short-running proofs, but with parallel_proofs = 2 it is easily to be seen in various examples (provided privately). I have now addressed the problem here: https://isabelle.sketis.net/repos/isabelle-release/rev/a9bef20b1e47 changeset: 68687:a9bef20b1e47 user:wenzelm date:Fri Jul 27 17:32:16 2018 +0200 files: src/Pure/goal.ML description: proper adjust_maxidx: assms could have maxidx >= 0, e.g. from command "subgoal premises"; That change will come back to the isabelle-dev repository in 1-2 weeks, when I make a routine merge. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Final consolidation for Isabelle2018-RC2
On 22/07/18 20:13, Makarius wrote: > On 22/07/18 12:44, Makarius wrote: >> On 18/07/18 12:53, Makarius wrote: >>> This is a reminder that we are in the final consolidation phase towards >>> Isabelle2018-RC2. >>> >>> I will say more precisely when the fork of the isabelle-dev vs. >>> isabelle-release repositories will happen, presumably in the next few >>> days. After return from FLoC I still need to sort out many details, and >>> some genuine problems (apart from inevitable last-minute additions). >> >> The present plan is to make the repository fork today, in approx. 6h. So >> this is the last chance to finalize for the Isabelle2018 release. > > I am about to make the repository fork. Right now it looks like > Isabelle2018-RC2 going to be current 89e05bd572c6 89e05bd572c6 is my tentative tag changeset, but the tagged version is the already published 14167c321d22. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Final consolidation for Isabelle2018-RC2
On 22/07/18 12:44, Makarius wrote: > On 18/07/18 12:53, Makarius wrote: >> This is a reminder that we are in the final consolidation phase towards >> Isabelle2018-RC2. >> >> I will say more precisely when the fork of the isabelle-dev vs. >> isabelle-release repositories will happen, presumably in the next few >> days. After return from FLoC I still need to sort out many details, and >> some genuine problems (apart from inevitable last-minute additions). > > The present plan is to make the repository fork today, in approx. 6h. So > this is the last chance to finalize for the Isabelle2018 release. I am about to make the repository fork. Right now it looks like Isabelle2018-RC2 going to be current 89e05bd572c6. Pushes on the isabelle-dev repositories should be avoided in the next 1-2 hours, to avoid data races concerning the target branch: Isabelle2018 vs. post-Isabelle2018 development. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Final consolidation for Isabelle2018-RC2
On 18/07/18 12:53, Makarius wrote: > This is a reminder that we are in the final consolidation phase towards > Isabelle2018-RC2. > > I will say more precisely when the fork of the isabelle-dev vs. > isabelle-release repositories will happen, presumably in the next few > days. After return from FLoC I still need to sort out many details, and > some genuine problems (apart from inevitable last-minute additions). The present plan is to make the repository fork today, in approx. 6h. So this is the last chance to finalize for the Isabelle2018 release. Afterwards changes for significant problems will be accepted (via email). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Final consolidation for Isabelle2018-RC2
On 19/07/18 13:42, Tobias Nipkow wrote: > I have the same problem, and on my machine it is reproduceable (and it > did not go away over the past week, although I tried different versions > of the devel repository). I suspect that it is a deferred error due to lazy facts in locale interpretation. In Isabelle/5820f0f379ae, I have now added the system option "strict_facts" to avoid this. You can use it with "isabelle build -o strict_facts" or add it temporarily to $ISABELLE_HOME_USER/etc/preferences as "strict_facts = true" (notably for "isabelle jedit"). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Final consolidation for Isabelle2018-RC2
I have the same problem, and on my machine it is reproduceable (and it did not go away over the past week, although I tried different versions of the devel repository). However, I cannot reproduce the problem on testboard. Tobias On 18/07/2018 17:05, Manuel Eberl wrote: I had what seems to be a spurious failure of Probabilistic_Timed_Automata yesterday: https://ci.isabelle.systems/jenkins/job/testboard/50/consoleFull The error message is: *** exception THM 0 raised (line 1136 of "thm.ML"): generalize: bad index I am quite sure that my (purely cosmetic) changes are completely unrelated to that error and a later test run of virtually the same thing worked fine. Perhaps this should be investigated before the release. Manuel On 2018-07-18 12:53, Makarius wrote: This is a reminder that we are in the final consolidation phase towards Isabelle2018-RC2. I will say more precisely when the fork of the isabelle-dev vs. isabelle-release repositories will happen, presumably in the next few days. After return from FLoC I still need to sort out many details, and some genuine problems (apart from inevitable last-minute additions). Makarius ___ 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 smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Final consolidation for Isabelle2018-RC2
I had what seems to be a spurious failure of Probabilistic_Timed_Automata yesterday: https://ci.isabelle.systems/jenkins/job/testboard/50/consoleFull The error message is: *** exception THM 0 raised (line 1136 of "thm.ML"): generalize: bad index I am quite sure that my (purely cosmetic) changes are completely unrelated to that error and a later test run of virtually the same thing worked fine. Perhaps this should be investigated before the release. Manuel On 2018-07-18 12:53, Makarius wrote: > This is a reminder that we are in the final consolidation phase towards > Isabelle2018-RC2. > > I will say more precisely when the fork of the isabelle-dev vs. > isabelle-release repositories will happen, presumably in the next few > days. After return from FLoC I still need to sort out many details, and > some genuine problems (apart from inevitable last-minute additions). > > > Makarius > ___ > 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
