Email Gateway (Aug 19 2022 at 10:05): Email Gateway (Aug 19 2022 at 10:05):From: Christian Sternagel <c.sternagel@gmail.com>
Dear list,
it is now the second time that I got
/home/griff/.isabelle/Isabelle2013-RC2/browser_info/HOL/.session/entries
(No such file or directory)
"$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).
Just reporting something odd.
cheers
chris
PS: It might be just a coincidence that I got this with afp_build, maybe
it can also happen with plain build.
Email Gateway (Aug 19 2022 at 10:06):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
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.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 19 2022 at 10:16):From: Makarius <makarius@sketis.net>
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@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
Email Gateway (Aug 19 2022 at 10:23):From: Christian Sternagel <c.sternagel@gmail.com>
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.
Email Gateway (Aug 19 2022 at 10:25):From: Makarius <makarius@sketis.net>
The isabelle build tool is controlled by "letter soups", a bit like Unix
tar. Certain combinations achieve certain things that you might want to
do, but there is quite a lot what one could want. So far isabelle build
options cover only half of the alphabet, a bit less than its predecessor
usedir.
The system manual explains the meaning of the build options, and gives
various examples for real-life situations.
Also note that when you just need a certain session image to work with it,
you do it via "isabelle build_dialog -l My_Session", or rather "isabelle
jedit -l My_Session" which then invokes build_dialog.
Makarius
Email Gateway (Aug 19 2022 at 10:26):From: Makarius <makarius@sketis.net>
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 runningisabelle 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 FAILEDWhy 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
Last updated: Apr 23 2024 at 20:15 UTC