Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] "isabelle usedir" --> "isabelle build" +


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

view this post on Zulip Email Gateway (Aug 19 2022 at 11:31):

From: Walther Neuper <wneuper@ist.tugraz.at>
thank you !
Walther

expertise induces simplicity ;-))


Last updated: Mar 29 2024 at 12:28 UTC