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
