On Mon, 3 Sep 2012, Christian Sternagel wrote:
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.
You could populate your $ISABELLE_HOME_USER/ROOTS file by some directories
that you want to have in the session name space by default, lets say all
of $AFP or the specific AFP/thys that you usually include in your work.
I was reluctant to do this by default, due to the massive impact of the
AFP name space on the overall session layout. This becomes even more
relevant as AFP will hopefully grow much larger in the near future.
A downside of such hardwiring in ROOTS is that overlapping ROOT inclusions
lead to a name conflict at the moment. I need to rethink this -- it just
came out in a this strict sense by default. Probably because it we were
still on Java 6 some weeks ago, where physical file-system locations
cannot be compared reliably; this works in Java 7 according to the
official documents.
- 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?
I tried hard to rule out any implicit system state influencing the session
name space. This includes current working directory (which is not
well-defined in many situations, especially on Windows and Mac OS X).
Moreover, I always try to avoid situations where accidental file-system
content affects the meaning of what you do -- like *.thy in old-style GNU
Makefiles. Just last week I was trying out some Netbeans project by
someone else, and its build process broke down immediately because it was
picking up accidental junk from my local directory.
- 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?
I can't say much on the spot. It appears to mix logical names and
physical locations in the same manner as theory imports, but that was just
a historical accident (it will become obsolete once there are is a proper
theory name spaces with session prefix).
Generally, the second half of the build tool is still missing: a proper
GUI panel that can be either started separately or within the Prover IDE.
Such a panel has its own persistent state of defaults (e.g. like the
"Search and Replace" dialog in jEdit). So much of the "saving of
keystrokes" will become obsolete.
There is in fact a built-in penalty for starting from the command line,
which happens to be the only way at the moment. Scala/JVM has rather long
startup times, and the running application becomes only gradually slower
as the JIT compiler improves the code. This can costs about 5-10s for a
small build job like a paper or slides based on HOL. Within the IDE it
should come out better.
One could even go as far as generating documents on the spot
interactively, without going through build at all. It is just an accident
of the old Proof General interaction mode that this did not work in the
past.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
