Email Gateway (Aug 18 2022 at 11:33): Email Gateway (Aug 18 2022 at 11:33):From: Nicole Rauch <rauch@informatik.uni-kl.de>
Dear all,
today I ran into a problem of how to add a search path and to import a
theory that is to be found in the search path.
In order to make a search path available, I define a theory:
theory Test1
imports Main
begin
ML {*
add_path "$ISABELLE_HOME/src/HOL/Word";
*}
end
I then import that theory and simultaneously the theory that I
actually want to import:
theory Test2
imports Test1 Num_Lemmas
begin
end
If I first load Test1 in Proof General and evaluate it, and afterwards
load Test2 in Proof General and evaluate it, everything works fine.
But if I start off with Test2, I get an error message that Num_Lemmas
cannot be found because Isabelle (being strict) obviously first tries
to locate all imports before evaluating them.
I've also tried to add the ML command to the very top of Test2 (before
the theory definition), and this works fine for Test2, but then I get
an error message when I try to import Test2 into some other theory
(the import mechanism expects the imported theories to start with
"theory").
Is there any solution to this conflict? How can I make Isabelle first
load the first imported theory before loading the second one?
Thanks in advance for any help
Nicole
Email Gateway (Aug 18 2022 at 11:33):From: Makarius <makarius@sketis.net>
This is correct. The load path cannot be changed during loading.
Luckily there is no need to change it at all, just specify the import as
follows:
theory Test
imports Main "~~/src/HOL/Word/Num_Lemmas"
begin
...
Makarius
Last updated: May 03 2024 at 08:18 UTC