Email Gateway (Aug 19 2022 at 14:47): Email Gateway (Aug 19 2022 at 14:47):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
I am trying to import some theory from AFP, but I get the following error:
Bad theory (file "/Applications/Isabelle2013-2.app/Isabelle/afp-2014-06-12/thys/LatticeProperties/Complete_Lattice_Prop.thy”)
I setup the path for afp in ~/.isabelle/Isabelle2013-2/etc/components:
/Applications/Isabelle2013-2.app/Isabelle/afp-2014-06-12/
and I installed AFP in /Applications/Isabelle2013-2.app/Isabelle/afp-2014-06-12/
I can access the path
/Applications/Isabelle2013-2.app/Isabelle/afp-2014-06-12/thys/LatticeProperties/Complete_Lattice_Prop.thy
and Isabelle manages to load this file when loading the file which imports it.
Best regards,
Viorel Preoteasa
Email Gateway (Aug 19 2022 at 14:47):From: Lars Noschinski <noschinl@in.tum.de>
Is this in Isabelle/jEdit? Have you tried saving the file after adding
the import?
Email Gateway (Aug 19 2022 at 14:47):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
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.
Viorel
Email Gateway (Aug 19 2022 at 14:48):From: Lars Noschinski <noschinl@in.tum.de>
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
Email Gateway (Aug 19 2022 at 14:48):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
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
Email Gateway (Aug 19 2022 at 14:48):From: Lars Noschinski <noschinl@in.tum.de>
On 16.06.2014 20:04, Viorel Preoteasa 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.
The AFP is nothing special from Isabelle's point of view. Does this
behaviour occur also with other imports (which are not in the same
directory as your theory)?
Does this behaviour occur if you specify the full path to the AFP-entry
instead of using $AFP (if you used $AFP before)?
Does this behaviour occur if you copy the files to another directory?
I am pretty sure your problem has a simple solution, but it is hard to
debug such things remotely ;)
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.
This happens sometimes for me, too. This seems to be a minor race
condition, but I never saw any negative consequences (except seeing the
dialog multiple times).
-- Lars
Email Gateway (Aug 19 2022 at 14:49):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
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
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.
Last updated: Nov 21 2024 at 12:39 UTC