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

Michael Norrish michael.norrish at nicta.com.au
Mon Aug 25 09:04:09 CEST 2014


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")

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?

Thanks,
Michael

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 490 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140825/bc4fbc45/attachment.asc>


More information about the isabelle-dev mailing list