Email Gateway (Aug 19 2022 at 11:40): Email Gateway (Aug 19 2022 at 11:40):From: Jason Dagit <dagitj@gmail.com>
Hello,
I installed Isabelle 2013 for windows (windows 7). If I put this into jEdit:
theory Scratch
imports Complex_Main "~~/src/HOL/Number_Theory/Primes"
begin
It gives me this error: Bad theory (file
"C:\Users\dagit\Desktop\Isabelle2013\src\HOL\Number_Theory\Primes.thy")
If I copy the path from that error message and try to use it with some
other program it works just fine.
I've also tried this with the isabelle eclipse IDE. I get the same error
but a slightly different formatting for the path.
Any ideas how to fix this?
Thanks,
Jason
Email Gateway (Aug 19 2022 at 11:40):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Jason,
if I do what you describe (on linux though) I get the same error until I
save the new theory file (which causes jEdit to actually process the
imports). (The same thing does not occur when just importing "Main", I
guess the difference is that "Main" is part of the default logic image
"HOL", but "Primes" isn't.)
hope this helps,
chris
Email Gateway (Aug 19 2022 at 11:40):From: Jason Dagit <dagitj@gmail.com>
I hadn't thought of that. I'll will try that tonight (I'm not near that
computer at the moment).
Thanks for the suggestion!
Jason
Email Gateway (Aug 19 2022 at 11:41):From: Dominic Mulligan <dominic.p.mulligan@googlemail.com>
I have also received a similar error on Linux in the recent past whilst
trying to load the Nominal.thy from Nominal Isabelle. Similarly, the
problem disappears when the theory file is saved, suddenly loading
correctly.
Thanks,
Dom
Email Gateway (Aug 19 2022 at 11:41):From: Jason Dagit <dagitj@gmail.com>
And I can confirm that saving it fixed the problem I was having on windows.
Last updated: Apr 25 2024 at 20:15 UTC