It’s entirely possible that the tests for Simpl in the AFP need improvement - the current VCG examples may not be using the full range of commands it provides.
Greetings from Kununurra somewhere in WA, Gerwin On 26 Aug 2014, at 1:51 pm, Michael Norrish <michael.norr...@nicta.com.au> wrote: > Apart from one of my own that I found, there are also a number of possibly bad > uses in hoare-package/hoare.ML, such as > > fun add_declaration name decl thy = > thy > |> Named_Target.init name > |> Local_Theory.declaration {syntax = false, pervasive = false} decl > |> Local_Theory.exit > |> Proof_Context.theory_of; > > I assume this should have the last two lines replaced by > > |> Local_Theory.exit_global; > > I will certainly test this out. > > I see that the Simpl entry in the current AFP still has this code too, and in > the version on SourceForge tagged with Isabelle2014. > > Do the regression tests for this package need improving, or are uses such as > the > above sometimes alright after all? > > Best, > Michael > > > On 26/08/14 13:12, Michael Norrish wrote: >> 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 > > > > > >> _______________________________________________ >> isabelle-dev mailing list >> isabelle-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev