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-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
