[isabelle-dev] Final consolidation for Isabelle2018-RC2

[Makarius]

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