Re: [isabelle] afp_build in RC2
On Sat, 2 Feb 2013, Gerwin Klein wrote:
This probably just depends on if you have built HOL with browser_info on
before or not, i.e. if the session file exists or not.
(afp_build just sets browser_info and document options)
I've hit this as well today, but I'm not sure which way is better:
failing the build or not. If HOL has not been built with browser_info
before, it doesn't really make sense to generate html that links to it.
I have made some refinements here just before starting the Isabelle2013-RC
phase. It should mostly work as in Isabelle2012, but with deterministic
order of the HTML index and without certain race conditions from the past.
On 02.02.2013, at 8:50 PM, Christian Sternagel <c.sternagel at gmail.com> wrote:
### I/O error: /home/griff/.isabelle/Isabelle2013-RC2/browser_info/HOL/.session/entries (No such file or directory)
### Browser info: failed to update session index of "$ISABELLE_BROWSER_INFO/HOL"
when starting "isabelle afp_build some-session". But this error is
nondeterministic. Both times, when issuing the command again, it
succeeded (and most of the time when I use afp_build, I do not get this
error at all).
Is it really non-deterministic due to parallel processing of sessions, or
just as Gerwin pointed out that you happen to have HOL with or without
Looking briefly over src/Pure/Thy/present.scala (and .ML) I don't see
anything suspicous. The index is produced once after processing all
This archive was generated by a fusion of
Pipermail (Mailman edition) and