[isabelle-dev] usedir -P P "http://isabelle.in.tum.de/library/"
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
> 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
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