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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
