recently, I encountered
Bad theory import "Draft.*" for my theories. What is the reason for it; this setup has worked for many days. It sounds like an invalid cache?
... restart resolved all issues
Robert Soeldner has marked this topic as resolved.
I got at least similar messages sometimes, and, from what I can remember, they typically came from a
ROOT file that was not up to date.
How does one update a ROOT file? I'm experiencing this trying to load theories from the seL4 microkernel project.
do you already have a ROOT file?
I have a ROOTS file in /Applications/Isabelle2021-1.app/ which points to all the lower ROOT files. I also have a repo in a separate directory with its own ROOTS file that points to lower ROOT files. When I load a thy file from this repo I often get "bad theory import" on some other theory inside the repo.
For example l4v/proof/crefine/RISCV64/Refine_c.thy imports CtoCRefine but Isabelle says that's a bad import. However I can find l4v/proof/crefine/lib/CToCRefine.thy
Do you start Isabelle with the right flags from the directory that contains the relevant ROOTS file?
Last updated: Jul 15 2022 at 23:21 UTC