Moritz R (Mar 25 2025 at 12:07): Moritz R (Mar 25 2025 at 12:07):When renaming a file, or changing the capitalization (and then of course also adapting the theory name), Isabelle will complain
`bad theory name [new name] for file [old file name.thy].
For Isabelle/jEdit it was sufficient to delete the corresponding ~ file.
For Isabelle/Vscode i still get the error, even after a restart of Isabelle/Vscode.
What can i do?
Moritz R (Mar 25 2025 at 12:08):logging out didn't help either.
Fabian Huch (Mar 25 2025 at 12:13):I think your error is somewhere else, Isabelle/VSCode doesn't try to remember a file name.
Fabian Huch (Mar 25 2025 at 12:13):perhaps you are loading a session and the name is in the ROOT file?
Moritz R (Mar 25 2025 at 12:13):Deleting the file, closing Isabelle/VsCode, opening Isabelle/Vscode, then restoring the theory (in my case i did it via git) worked
Moritz R (Mar 25 2025 at 12:15):idk what a session is, but the header of my file looks like this:
theory Chomsky_Schuetzenberger
imports "../CFG" "../CFL" "../Parse_Tree" "Finite_Automata_Not_HF" "$AFP/Regular-Sets/Regexp_Constructions"
begin
I also use Isabelle/vscodes Open folder instead of only this one file
Fabian Huch (Mar 25 2025 at 12:24):Maybe there is a problem in your file system with case sensitivity?
Fabian Huch (Mar 25 2025 at 12:25):E.g. on Macos file names are case insensitive so maybe your change didn't really work?
Moritz R (Mar 25 2025 at 12:27):I have confirmed, that this also happens, when one only opens one file via Vscode.
What works when not using the open folder feature, is to close all editors of the renamed file, and then restart vscode
Moritz R (Mar 25 2025 at 12:27):I am using macOS atm, but im pretty sure i also had such a problem on windows before.
Moritz R (Mar 25 2025 at 12:28):also i renamed the file using github, so idk what happens on macOS then
Moritz R (Mar 25 2025 at 12:28):Let me hop on windows real quick
Fabian Huch (Mar 25 2025 at 12:28):Moritz R said:
also i renamed the file using github, so idk what happens on macOS then
This might be the problem -- no idea what git does in this situation
Fabian Huch (Mar 25 2025 at 12:30):Off-topic: Usually imports are session-qualified rather than using paths with environment variables
Moritz R (Mar 25 2025 at 12:33):Off-topic: Usually imports are session-qualified rather than using paths with environment variables
i'm not sure what session-qualified means, but you mean i shouldn't use $AFP ? What is a better option?
Fabian Huch (Mar 25 2025 at 12:37):"<sessionname>.<theoryname>"
Mathias Fleury (Mar 25 2025 at 12:40):I am actually surprised that the import with $AFP still work. Isabelle is now very strict on checking that you are using the session-qualified right if you have a ROOT file (and you should have one).
Moritz R (Mar 25 2025 at 12:46):Ok, so on windows and macOS, if you use finder/explorer to rename the file everything works as expected.
On both systems, pulling a rename - e.g. someone else renamed it, pushed it into a github and you pulled it -
will get the mentioned error.
FIX:
What seems to work reliably, is to use
File -> Close Folder, then restart Isabelle/VSCode.
You might have to select the file again, as it will still have the old file in the editor panel (idk where it saves that).
Moritz R (Mar 25 2025 at 12:47):Mathias Fleury said:
I am actually surprised that the import with $AFP still work. Isabelle is now very strict on checking that you are using the session-qualified right if you have a ROOT file (and you should have one).
Well i dont know what a root file is, so i guess thats why my imports work?
Mathias Fleury (Mar 25 2025 at 12:50):https://isabelle.in.tum.de/doc/system.pdf, chapter 2; although the two slides from http://cl-informatik.uibk.ac.at/teaching/ss24/itpIsa/slides/12x1.pdf are probably as useful as the description in the system manual
Fabian Huch (Mar 25 2025 at 13:02):Moritz R said:
Ok, so on windows and macOS, if you use finder/explorer to rename the file everything works as expected.
On both systems, pulling a rename - e.g. someone else renamed it, pushed it into a github and you pulled it -
will get the mentioned error.
FIX:
What seems to work reliably, is to use
File -> Close Folder, then restart Isabelle/VSCode.
You might have to select the file again, as it will still have the old file in the editor panel (idk where it saves that).
This looks like a VSCode problem then, where it keeps the file cached when in reality it was changed on disk but only if the inode didn't change. This wouldn't have anything to do with Isabelle except that wer're still using an older version -- maybe it's fixed on newer VSCode versions
Moritz R (Mar 25 2025 at 14:54):Yes, looks a lot like this issue, that isn't fixed in our version https://github.com/microsoft/vscode/issues/161743
Last updated: Apr 03 2025 at 20:22 UTC