[isabelle-dev] usedir -P P "http://isabelle.in.tum.de/library/"

Makarius makarius at sketis.net
Mon Sep 3 14:15:47 CEST 2012

On Sat, 1 Sep 2012, Gerwin Klein wrote:

> How do I do the equivalent of "isabelle usedir -P URL" in the new build 
> system?
> I'm trying to make sure that generated HTML for AFP entries doesn't 
> contain dangling links of the form "up to index of HOL/HOLCF"
> Basically, only the HTML for AFP entries should be on the AFP site, the 
> rest should link back to the distribution. I'm not sure where/how to say 
> which sessions should generate back links and which not and I couldn't 
> find anything enlightening in isabelle options.

The -P option never worked out beyond the situation where some body of 
Isabelle applications points back to some background distribution.  There 
was a lack of version-awareness and further add-ons in the hierarchy of 
applications (longer chains of back-references).

Before not upgrading the old -P feature to the current build tool, I 
actually spent some thoughts how AFP would manage without it.  You 
basically just need to do the normal build including the "base sessions", 
so the browser_info for these will accumulate in the right spot to be 
linked correctly.

Thus even an unidentified development snapshot like 
would point to the correct version of Main -- the one that was used to 
build it -- not the one that happens to be on the official Isabelle 

Apart from nostalgy about discontinued options, there is actually a an 
oddity left in the way browser_info is organized: its directory structure 
follows the tree of session images, but that leads to a slightly 
unorganized situation in practice.  I still did not find the spot in the 
AFP scripts where the location of the generated HTML files is guessed. 
This might be a starting point for further reforms that clarify the 
situation further, say with some explicit sectioning within AFP, and in 
contrast to what it uses from the background.


More information about the isabelle-dev mailing list