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

[Makarius]

On Tue, 4 Sep 2012, Gerwin Klein wrote:

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

Standard questions: Why do you want to do it?  Do you really need to do 
it? Is there a better (simpler, more robust) way?


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

> It's more important that the release version is consistent, though, 
> which gets built incrementally when new entries are submitted.

I still have now proper mental images, how this incremental editing 
process of AFP works.  Are you doing this on "the" single Isabelle version 
that happens to be on your laptop, that you use for other things as well, 
and then there are some AFP entries coming to be handled with it?

Then it is easy to have heap images around that were build with the wrong 
options for AFP, without browser_info etc.

But you could easily separate things: have one Isabelle configuration just 
for AFP submissions, where you add things incrementally, and the 
browser_info for the base sessions are there in the proper place all the 
time.


As of Isabelle/c15a7123605c there are a variety of possibilities to 
achieve clearly separated "build beds" for AFP entries with well-defined
options maintained over a longer timespan:

   * isabelle build -R to refer to the requirements of some session (this
     is brand new, and makes build now use more than half of the alphabet
     of option letters)

   * isabelle build -s (the "Haftmann" option for separate heaps +
     browser_info within ISABELLE_HOME)

   * env ISABELLE_IDENTIFIER=xxx before "booting" some isabelle scripts,
     to provide an alternative location of ISABELLE_HOME_USER for
     repository snapshots in particular.

The latter is intended for some Mira reforms, that are still not there 
yet.


 	Makarius