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 browser_info already?

Looking briefly over src/Pure/Thy/present.scala (and .ML) I don't see anything suspicous. The index is produced once after processing all sessions.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.