Email Gateway (Aug 19 2022 at 11:31): Email Gateway (Aug 19 2022 at 11:31):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Walter,
In Isabelle's build system, you specify the parent session of a session, not the entry
theory. Since the theory Complex_Main is part of the HOL session, you can use the HOL
session as the parent:
session Isac = HOL +
theories Build_Isac
I don't know of the 'in "..."' syntax, but ideally, the ROOT file is in the same directory
as your theories (or the session directory of your development). For a start, you don't
need a ROOTS file - instead, include the directory of your ROOT file in the call to
isabelle build:
isabelle build -d <path to ROOT> Isac
Add the option -b if you want to produce a image of the session (rather than just run the
session).
Hope this helps,
Andreas
Email Gateway (Aug 19 2022 at 11:31):From: Walther Neuper <wneuper@ist.tugraz.at>
thank you !
Walther
expertise induces simplicity ;-))
Last updated: Nov 21 2024 at 12:39 UTC