Stream: Beginner Questions

Topic: Implicit use of directory


view this post on Zulip 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.

view this post on Zulip 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")

view this post on Zulip 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

view this post on Zulip Mathias Fleury (Nov 12 2020 at 14:32):

Given your email on the mailing list, my guess was correct

view this post on Zulip Gergely Buday (Nov 13 2020 at 07:46):

Indeed, thanks. "~~src/bla/bla" is just outdated?

view this post on Zulip 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: Sep 25 2021 at 08:21 UTC