[isabelle-dev] porting code to isabelle2014 and getting "unfinished linear change" errors

[Lars Noschinski]

On 25.08.2014 09:04, Michael Norrish wrote:

> I'm based off RC0 (at 9e0c62d of the *git* mirror at github.com/seL4/isabelle;
> this is tagged Isabelle2014-RC0 and certainly seems to be the same as
> 251ef0202e71 in the Mercurial world).
>
> I am running code that seemed to be legitimate in 2013-2, but which is now
> giving me errors such as
>
>     *** exception Fail raised (line 169 of "sign.ML"): Unfinished linear change
> of theory content
>     *** At command "end" (line 142 of
> "~/ver2014/l4v/tools/c-parser/testfiles/fncall.thy")
This is related to never leaving the local theories properly. If I
remember correctly, you use Proof_Context.theory_of in places where it
really should have been Named_Theory.exit(_global).

> One annoying thing about this is that it is happening at theory end rather than
> directly after or during the execution of my code.  What would be the easiest
> way to debug this problem?  Or is there an obvious fix I can apply?
The way I debugged this was commenting out large parts of the code until
the error disappeared.

David Greenaway already has some patches I used to get autocorres
(including the c-parser) running on 2014 -- I'll send them to you privately.

  -- Lars