Re: [isabelle] afp_build in RC2



Dear Makarius,

it is not real non-determinism (it just seemed to me like it, since I didn't know the "raise" conditions ;)).

Incidentally, I always get the error when running.

  isabelle build -d -nc '$AFP' <session-name>

followed by

  isabelle afp_build <session-name>

Then, running

  isabelle afp_build <session-name>

a second time succeeds.

Another thing. After manually deleting ~/.isabelle/Isabelle2013-RC2/heaps and ~/.isabelle/Isabelle2013-RC2/browser_info and then running

  isabelle afp_build <afp-session-name>

I get the output:
Building Pure ...
Finished Pure (0:00:08 elapsed time, 0:00:08 cpu time, factor 1.00)
Building HOL ...
rmdir: failed to remove ‘/tmp/isabelle-griff14182’: Directory not empty
HOL FAILED

Why do I get this error (and why so late, it seems to approximately take the same time as HOL usually needs to build)? This error does not go away when issuing afp_build another time. But with

  isabelle build -b HOL

it is not triggered.

cheers

chris

PS: Isn't it odd that I have to write -nc if I only want to clean. I would have suspected -c to do exactly that... but then again, there is this difference between just "running" a session (and probably generating some document) and "building" a logic image, which I have not quite internalized yet.

On 02/04/2013 11:40 PM, Makarius wrote:
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.