Gergely Buday (Nov 12 2020 at 12:43): Gergely Buday (Nov 12 2020 at 12:43):On
isabelle build -D .
I get
*** Implicit use of directory "/cygdrive/d/isabelle/Isabelle2020/src/HOL/IMP" for theory "induction.AExp"
Should I edit the ROOT file? How? I tried to add IMP/Big_Step to theories but it did not work.
Gergely Buday (Nov 12 2020 at 12:58):I tried
directories
"~~/src/HOL/IMP"
in ROOT but that got me into
*** Duplicate use of directory "/cygdrive/c/Users/gbuday/doctoral/papers/proofsand/topics/induction/$ISABELLE_HOME/src/HOL/IMP"
*** for session "HOL-IMP" (line 182 of "/cygdrive/d/isabelle/Isabelle2020/src/HOL/ROOT")
*** vs. session "induction" (line 1 of "/cygdrive/c/Users/gbuday/doctoral/papers/proofsand/topics/induction/ROOT")
Mathias Fleury (Nov 12 2020 at 13:09):Wild guess: somewhere in your development, you have a "~~src/HOL/IMP/Some_Theory.thy". Replace it by "HOL-IMP.Some_Theory" (with quotes) and add HOL-IMP to the session in the ROOT file
Mathias Fleury (Nov 12 2020 at 14:32):Given your email on the mailing list, my guess was correct
Gergely Buday (Nov 13 2020 at 07:46):Indeed, thanks. "~~src/bla/bla" is just outdated?
Gergely Buday (Nov 13 2020 at 07:51):And, I didn't know this "sessions" clause, that's why I could not fix it reading your guess.
Last updated: Apr 19 2024 at 16:20 UTC