Email Gateway (Aug 19 2022 at 11:31): Email Gateway (Aug 19 2022 at 11:31):From: Walther Neuper <wneuper@ist.tugraz.at>
The error message
$ ./bin/isabelle build -b isac
Bad parent session "Complex_Main" for "Isac" (file
"/usr/local/isabisac/src/Tools/isac/ROOT")
is right: "Complex_Main" is a /theory/ and not a /session/.
(and we could not circumvent the error message, when trying to run our
Test_Isac.thy)
In order to get rid of this error message, should we make "Complex_Main"
a session, or do we have to change the structure of the underlying
theories (of "Build_Isac.thy in (3) below) ?
Thank you for help,
Walther
PS: We upgrade our software to Isabelle2013 and would like to have as
little changes as possible in the first steps; from "isabelle system"
and examples in the code we extracted these changes:
(1) ~~/ROOTS
/-------------------------------
:
src/Tools/isac
\-------------------------------
and
(2) ~~/src/Tools/isac/ROOT
/-------------------------------
session Isac in "~~/src/Tools/isac" = Complex_Main +
theories Build_Isac
\-------------------------------
(?are they correct?)
and now we would like to keep the original file from Isabelle2012 as is ...
(3) ~~/src/Tools/isac/Build_Isac.thy
/-------------------------------
theory Build_Isac
imports Complex_Main
:
\-------------------------------
... with "imports Complex_Main" --- assumedly the origin of the above
error message in Isabelle2013, while in Isabelle2012 we
successfully did
(a) ~$ isabelle usedir -b HOL Isac
using
(b) ~~/src/Tools/isac/ROOT.ML
/-------------------------------
use_thys ["Build_Isac"];
\-------------------------------
Last updated: Apr 19 2024 at 08:19 UTC