isabelle build -D .
*** 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.
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")
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
Given your email on the mailing list, my guess was correct
Indeed, thanks. "~~src/bla/bla" is just outdated?
And, I didn't know this "sessions" clause, that's why I could not fix it reading your guess.
Last updated: Aug 10 2022 at 19:17 UTC