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

[Gerwin Klein]

On 03/09/2012, at 10:15 PM, Makarius <makarius at sketis.net> wrote:

> 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.  

Which is precisely what I want to do. 


> 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.

Does that mean the editors need to rebuild everything from Pure for each new entry? Or is there another way to make sure that the right chain of browser_info sets is generated?

It wouldn't be hard to make sure that a few base images are on the web site already, but the -c option will only force a rebuild of leaf sessions, not of intermediate images, so if for instance HOL-Nominal (or some other not-that-standard image) has been built already and an editor is preparing html for a new entry by building a session on top of HOL-Nominal that part will be missed.


> Thus even an unidentified development snapshot like http://afp.sourceforge.net/browser_info/devel/HOL/Datatype_Order_Generator/Order_Generator.html 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 website.

Yes, that is nice and will work automatically now from what is generated in the regression test. It's more important that the release version is consistent, though, which gets built incrementally when new entries are submitted.


> 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'd have no problem with a different organisational structure there.


>  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.

It is/was part of the IsaMakefiles -- the ones that have the -P option point to the library. The others not. It wasn't perfect either, plenty of potential for getting things wrong manually.

As far as I can see this is the last bigger issue to be resolved before we can remove the IsaMakefiles from the AFP. The AFP regression test is already running on the new build system now and seems to be working fine.

Cheers,
Gerwin