[isabelle] "isabelle usedir" --> "isabelle build"



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 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.