Robert Soeldner (Apr 14 2022 at 05:16): Robert Soeldner (Apr 14 2022 at 05:16):Hi,
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?
Robert Soeldner (Apr 14 2022 at 06:12):... restart resolved all issues
Notification Bot (Apr 14 2022 at 06:12):Robert Soeldner has marked this topic as resolved.
Wolfgang Jeltsch (Apr 14 2022 at 11:50):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.
John Scebold (Apr 14 2022 at 18:46):How does one update a ROOT file? I'm experiencing this trying to load theories from the seL4 microkernel project.
Kevin Kappelmann (Apr 15 2022 at 08:39):do you already have a ROOT file?
John Scebold (Apr 15 2022 at 13:46):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
Kevin Kappelmann (Apr 15 2022 at 18:48):Do you start Isabelle with the right flags from the directory that contains the relevant ROOTS file?
Last updated: Apr 25 2024 at 01:08 UTC