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

[Gerwin Klein]

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.norrish at 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-dev at in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
>
>
>
>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at 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.