Re: [isabelle] afp_build in RC2



On Tue, 5 Feb 2013, Christian Sternagel wrote:

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

I have experimented a bit, but without any clear conclusion. There might be some remaining problems (and not just confusions) somewhere, but we need to pin them down precisely.


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.

The second time it will not build anything again, because it was already finished in the first run. When insisting in a second build like this

  isabelle afp_build -- -c <session-name>

you should see the same behaviour again.


Recall that "### I/O error" is just a warning, about an internal error that was ignored. IIRC, this non-strict behaviour has been there all the time: the idea is that browser_info is not fully formally managed, so you could have too little or too much lying around in that directory, and the system fails gracefully.

In the next big reform of browser_info, I shall probably make all the information part of the log file, and merely have a tool to pull it from there to get actual HTML.


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 also looks very odd to me, but I didn't get there. It would help to see the log file of the failed HOL session, or the result of it running with "isabelle build -v", which gives some progress report. And what is in /tmp/isabelle-griff14182 after breakdown?

(Better show me this privately off-list.)


	Makarius


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