[isabelle-dev] isabelle build (was: Isabelle manuals as regular session documents)

[Christian Sternagel]

On 08/30/2012 10:57 PM, Makarius wrote:
> I did not move forward yet, because my impression is that the early
> adopters on this mailing list have difficulties to catch up.
indeed ...

I have some questions/comments:

When preparing a document upon an Isabelle formalization (or to be more 
specific, let's say an AFP entry) its obvious to base the corresponding 
session on the available AFP sessions. To achieve this, I did:

   # create a directory 'dir'
   # change into that directory
   isabelle mkroot -d -n SessionName
   # now in the generated ROOT file I put
   session "SessionName" = "Name-of-AFP-session" +
     options [document = pdf, document_output = "generated"]
     theories Test
     files "document/root.tex"
   # to build a PDF, I have to run (at least I think so)
   isabelle build -D . -d '$AFP'

I believe for a user this is the common use-case. Thus, why not minimize 
the necessary typing by setting defaults appropriately? What seems 
inconvenient to me is that I have to put "-D ." and "-d '$AFP'" manually 
every time I want to build (or "-d ." and the full session name). I'd 
rather like that just 'isabelle build' achieves exactly this.

- How about making "-D ." the default (as long as a ROOT file exists in 
the current directory). Would this cause any problems? If so, at least 
"-d ." by default would be convenient. Plus the possibility to mark a 
session as default build target in a ROOT file (such that it does not 
have to be given explicitly on the command line). What do you think?

- Moreover, a persistent way (e.g., as part of the ROOT file) to set 
dependent directories would be nice, e.g.,

   session "SessionName" = "$AFP/Name-of-AFP-session" + ...

having the effect of "-d '$AFP'".

Maybe there is already a way to do what I want and I just didn't see it?

cheers

chris