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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
