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



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

On 16/07/13 08:26, Walther Neuper wrote:
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"];
     \-------------------------------







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.