Re: [isabelle] using AFP



Curious. I’m assuming your theory file starts like this:

----
theory Scratch
imports "$AFP/LatticeProperties/Complete_Lattice_Prop"
begin
----

If I open this file by running “isabelle jedit” on the command line, I get a theory import dialog where it says it needs to load Complete_Lattice_Prop and another theory. After clicking Ok, it does so without errors.

What happens when you say

isabelle build -d /Applications/Isabelle2013-2.app/Isabelle/afp-2014-06-12/thys LatticeProperties

on the command line?

Does anything change when you run jedit like this?

isabelle jedit -d /Applications/Isabelle2013-2.app/Isabelle/afp-2014-06-12/thys

Also, just to make sure it’s picking up the right Isabelle version, what is the output of the following?

isabelle version

Cheers,
Gerwin



On 17.06.2014, at 4:04 am, Viorel Preoteasa <viorel.preoteasa at aalto.fi> wrote:

> Isabelle opens Complete_Lattice_Prop.thy, and this file does not have
> errors. Only the test file has the error. I tried some other random
> theory from AFP, and I get exactly the same behavior.
>
> In the theory panel the the Test file is marked with red. When
> opening the test file Isabelle asks to open the files on which Test dependents,
> However after opening them it asks again about opening one of these
> files.
>
> Viorel
>
>
> On 6/16/2014 7:07 PM, Lars Noschinski wrote:
>> On 16.06.2014 15:58, Viorel Preoteasa wrote:
>>> This is in Isabelle/jEdit. I tried to save the file. I also
>>> tried to close Isabelle and open it again, but I get the
>>> same error.
>> Does I/jEdit open the Complete_Lattice_Prop.thy file? If yes, is there
>> any error in this file (have a look at the theories panel)?
>>
>>   -- Lars
>>
>
>


________________________________

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.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.