[isabelle-dev] isabelle build (was: Isabelle manuals as regular session documents)
c-sterna at jaist.ac.jp
Mon Sep 3 04:54:31 CEST 2012
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.
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"]
# 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?
More information about the isabelle-dev