Email Gateway (Aug 22 2022 at 16:24): Email Gateway (Aug 22 2022 at 16:24):From: Matthew.Brecknell@data61.csiro.au
Hello,
We are having some difficulty figuring out how to update some legacy l4-verified proofs to work well with Isabelle2017 session-qualified imports.
Although all our sessions work with isabelle build, we have a session for which isabelle jedit gives a plugin error like this:
Cannot start:
*** Duplicate theory
"/path/to/isabelle/src/HOL/Word/HOL-Library.Type_Length.thy"
vs.
"/path/to/isabelle/src/HOL/Library/Type_Length.thy"
None of our theories import Type_Length directly, but we do import HOL/Word/Word using a legacy path-based import.
We've tried to diagnose this using various combinations of isabelle imports, but we're not sure how to interpret the results.
isabelle imports -D . -I -v ARMModel reports the same error as above.
isabelle imports -d . -I -v ARMModel does not report any no potential session imports.
isabelle imports -d . -U -i -v ARMModel performs some updates, but Isabelle/jEdit still produces an error, albeit relating to a different theory import.
isabelle imports -D . -U -i -v ARMModel produces the following errors:
*** No such file: "/home/matthewb/verification/mainline/isabelle/src/HOL/Word/HOL-Library.Type_Length.thy"
*** The error(s) above occurred for theory "HOL-Library.Type_Length"
*** (required by "ARMModel.arm_model" via "ARMModel.arm_model_pre" via "ARMModel.WordSetup" via "ARMModel.Word_Lemmas_32" via "ARMModel.Word_Lemmas" via "ARMModel.Aligned" via "ARMModel.Word_Lib" via "ARMModel.Word_Syntax" via "ARMModel.WordBitwise" via "ARMModel.Word") (line 9 of "/home/matthewb/verification/mainline/isabelle/src/HOL/Word/Word.thy")
*** No such file: "/home/matthewb/verification/mainline/isabelle/src/HOL/Word/HOL-Library.Boolean_Algebra.thy"
*** The error(s) above occurred for theory "HOL-Library.Boolean_Algebra"
*** (required by "ARMModel.arm_model" via "ARMModel.arm_model_pre" via "ARMModel.WordSetup" via "ARMModel.Word_Lemmas_32" via "ARMModel.Word_Lemmas" via "ARMModel.Aligned" via "ARMModel.Word_Lib" via "ARMModel.Word_Syntax" via "ARMModel.WordBitwise" via "ARMModel.Word") (line 10 of "/home/matthewb/verification/mainline/isabelle/src/HOL/Word/Word.thy")
*** No such file: "/home/matthewb/verification/mainline/isabelle/src/HOL/Word/HOL-Library.Bit.thy"
*** The error(s) above occurred for theory "HOL-Library.Bit"
*** (required by "ARMModel.arm_model" via "ARMModel.arm_model_pre" via "ARMModel.WordSetup" via "ARMModel.Word_Lemmas_32" via "ARMModel.Word_Lemmas" via "ARMModel.Aligned" via "ARMModel.Word_Lib" via "ARMModel.Word_Syntax" via "ARMModel.WordBitwise" via "ARMModel.Word" via "ARMModel.Bits_Bit") (line 8 of "/home/matthewb/verification/mainline/isabelle/src/HOL/Word/Bits_Bit.thy")
*** No such file: "/home/matthewb/verification/mainline/isabelle/src/HOL/Word/HOL-Library.Type_Length.thy"
*** No such file: "/home/matthewb/verification/mainline/isabelle/src/HOL/Word/HOL-Library.Boolean_Algebra.thy"
*** No such file: "/home/matthewb/verification/mainline/isabelle/src/HOL/Word/HOL-Library.Bit.thy"
*** The error(s) above occurred in session "ARMModel" (line 9 of "/home/matthewb/verification/mainline/l4v/internal/camkes/ROOT")
I suspect our problem is that we have a number of library theories which are included in multiple sessions (and therefore are not strongly identified with a single session), and which also include Isabelle theories using legacy path-based imports.
We would like to embrace session-qualified imports. Can anyone offer advice on how to begin disentangling a nest of legacy path-base imports?
Thanks,
Matthew
Email Gateway (Aug 22 2022 at 16:24):From: Makarius <makarius@sketis.net>
During the year I've spent many weeks disentangling theory imports in
AFP: the "isabelle imports" tool was a result of that, but it does not
cover all oddities seen in the wild.
Maybe the following Isabelle/Scala invocations help to sort out the
situation of theory files in different sessions, leading to confusion
due to different qualified names:
$ isabelle scala -J-Xmx4096m -J-Xss8m
import isabelle._
val options = Options.init
val sessions = Sessions.load(options)
val deps = Sessions.deps(sessions, global_theories =
sessions.global_theories)
deps.all_known.files.toList.filter(p => p._2.length > 1).sortBy(p =>
p._1.toString).foreach(println)
Note that Sessions.load has an argument for "dirs": it corresponds to
option -d in command-line tools.
Makarius
Email Gateway (Aug 22 2022 at 16:25):From: Matthew.Brecknell@data61.csiro.au
Thanks, Makarius. I haven't had a lot of time to look at this today, but I did find that the call to Sessions.deps threw the "Duplicate theory" exception noted in my previous email, so I didn't get as far as the final step of analysing the dependencies.
I will dig into the sessions.scala source to see if that helps me figure out what we're doing wrong.
During the year I've spent many weeks disentangling theory imports in
AFP: the "isabelle imports" tool was a result of that, but it does not
cover all oddities seen in the wild.
Maybe the following Isabelle/Scala invocations help to sort out the
situation of theory files in different sessions, leading to confusion
due to different qualified names:
$ isabelle scala -J-Xmx4096m -J-Xss8m
import isabelle._
val options = Options.init
val sessions = Sessions.load(options)
val deps = Sessions.deps(sessions, global_theories =
sessions.global_theories)
deps.all_known.files.toList.filter(p => p._2.length > 1).sortBy(p =>
p._1.toString).foreach(println)
Note that Sessions.load has an argument for "dirs": it corresponds to
option -d in command-line tools.
Makarius
Last updated: Apr 20 2024 at 04:19 UTC