Re: [isabelle] Trouble loading theories on windows (Isabelle2013-1-RC3)



There's no problem. I misspelled "FSet" as "Fset".

Actually, I guess there is a problem that leads to confusion.

Because Windows filenames aren't case sensitive, the "imports" command will load the file "FSet.thy" when importing "~~/src/HOL/Library/Fset", though jEdit loads it with the wrong case, "Fset.thy", and the error stays.

The import of "../../../../../../E_2/binp/Isabelle2013-1-RC3/src/HOL/Library/Fset" will load the file with the right case into jEdit, "FSet.thy", and it works.

I discovered all that after importing "~~/src/HOL/Library/Code_Target_Nat" to get the pretty printing of natural numbers, mentioned by Andreas in this email:

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-October/msg00033.html

That's very useful.

Regards,
GB



On 10/30/2013 6:02 PM, Gottfried Barrow wrote:
Hi,

This is a continuation of this thread: "[isabelle] Trouble loading theories on windows":

http://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-August/msg00050.html

It's not specific to Isabelle2013-1, but I go ahead and associate it with Isabelle2013-1-RC3.

The suggestions are to save and reload the theory, but that doesn't work for me when I use this:

theory c
imports Complex_Main  "~~/src/HOL/Library/Fset"

The file Fset.thy gets loaded into jEdit, but I still get this error:

Bad theory (file "E:\E_2\binp\Isabelle2013-1-RC3\src\HOL\Library\Fset.thy")

So, I use a relative path:

theory c
imports Complex_Main
"../../../../../../E_2/binp/Isabelle2013-1-RC3/src/HOL/Library/Fset"

The file Fset.thy gets loaded, I get no errors, and I don't have to do anything special.

Regards,
GB















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