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

[Michael Norrish]

I already have the patch you sent me offline in my history.

I will examine the remaining uses of theory_of and see if they're legitimate.

Thanks,
Michael

On 25/08/14 17:32, Lars Noschinski wrote:
> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 490 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140826/c5d34d62/attachment.sig>