Email Gateway (Aug 22 2022 at 18:06): Email Gateway (Aug 22 2022 at 18:06):From: Walther Neuper <wneuper@ist.tugraz.at>
while updating Isac [1] from Isabelle2017 to Isabelle2018, we see that
handling of sessions became more supportive but also more rigorous.
We suppose an error in theory imports, indicated by importing a session,
but we cannot find the error:
As shown in the attached "Screenshot-Isac18-ERROR.png", the session
"Isac" is built with "theories Build_Isac" (without any error). But if
we "import Isac.Build_Isac", we get the error
Unfinished theory⌂
exception THEORY raised (line 233 of "context.ML"):
Duplicate theory name
{..., HOL.Transcendental, HOL.Complex, HOL.MacLaurin, Complex_Main, Draft.KEStore}
{..., HOL.Transcendental, HOL.Complex, HOL.MacLaurin, Complex_Main, Isac.KEStore}
where "KEStore.thy" [2] is the first theory in Isac.
What kind of error should we search for?
Many thanks in advance !
Walther
[1] http://www.ist.tugraz.at/isac/History
[2]
https://intra.ist.tugraz.at/hg/isa/file/ddba76eec47e/src/Tools/isac/KEStore.thy
Screenshot-Isac17-OK.png
Screenshot-Isac18-ERROR.png
Email Gateway (Aug 22 2022 at 18:06):From: Dominique Unruh <unruh@ut.ee>
This error means that you have imported KEStore in two different ways:
Once, as part of the session Isac (either because your wrote Isac.KEStore,
or because you imported it from a theory in Isac).
Second, from a theory Y that is not in your session (and thus automatically
in Draft).
You have to either include Y in Isac (by editing ROOT, or by importing it
from another theory in Isac), or to import KEStore from Y as Isac.KEStore.
To find out whether a theory is in Isac or Draft, however on the name of
the theory in the panel on the right to read the tooltip.
You have to find a theory in Draft that imports KEStore unqualified.
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 18:07):From: Walther Neuper <wneuper@ist.tugraz.at>
thanks a lot for your help, to find out how to adopt advances while
updating from Isabelle2017 to Isabelle2018 ..
On 2018-08-27 18:20, Dominique Unruh wrote:
This error means that you have imported KEStore in two different ways:
Once, as part of the session Isac (either because your wrote Isac.KEStore, or because you imported it from a theory in Isac).
Second, from a theory Y that is not in your session (and thus automatically
in Draft).
indeed, that was the case, see
https://intra.ist.tugraz.at/hg/isa/rev/b33dc41f4350
and the following hint was very helpful:
To find out whether a theory is in Isac or Draft, hover on the name of the theory in the panel on the right to read the tooltip.
Best wishes,
Dominique.On Mon, 27 Aug 2018 at 23:33, Walther Neuper <wneuper@ist.tugraz.at> wrote:
while updating Isac [1] from Isabelle2017 to Isabelle2018, we see that
handling of sessions became more supportive but also more rigorous.We suppose an error in theory imports, indicated by importing a session,
but we cannot find the error:As shown in the attached "Screenshot-Isac18-ERROR.png", the session
"Isac" is built with "theories Build_Isac" (without any error). But if
we "import Isac.Build_Isac", we get the errorUnfinished theory⌂
exception THEORY raised (line 233 of "context.ML"):
Duplicate theory name
{..., HOL.Transcendental, HOL.Complex, HOL.MacLaurin, Complex_Main,
Draft.KEStore}
{..., HOL.Transcendental, HOL.Complex, HOL.MacLaurin, Complex_Main,
Isac.KEStore}where "KEStore.thy" [2] is the first theory in Isac.
What kind of error should we search for?
Many thanks in advance !
Walther
[1] http://www.ist.tugraz.at/isac/History
[2] https://intra.ist.tugraz.at/hg/isa/file/ddba76eec47e/src/Tools/isac/KEStore.thy
Last updated: Nov 21 2024 at 12:39 UTC