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

[Michael Norrish]

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

-------------- 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/fc923daf/attachment.sig>