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

[Makarius]

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