[isabelle-dev] I/O error in isabelle build

[Makarius]

On 16/05/18 20:48, Lars Hupel wrote:
> I'm seeing some spurious (?) errors in "isabelle build":
> 
> 17:15:13 Finished List-Index (0:00:08 elapsed time, 0:00:11 cpu time,
> factor 1.37)
> 17:15:13 *** I/O error:
> /tmp/isabelle-jenkins/process478460358635901180/export2631876 (No such
> file or directory)
> 
> I don't understand where these are coming from. One instance can be
> found here:

These are relatively rare race conditions. I have now made it more
robust as follows:

changeset:   68198:6710167e17af
tag:         tip
user:        wenzelm
date:        Wed May 16 21:36:59 2018 +0200
files:       src/Pure/Tools/build.ML src/Pure/Tools/build.scala
description:
avoid race condition wrt. ISABELLE_TMP, which is removed in
Bash.cleanup() before Bash.result(progress_stdout);


The export that happens here is document.tex for each theory: it is
presently only for testing the new mechanism. A bit later, it will help
to move the "isabelle document" process from Isabelle/ML to
Isabelle/Scala, and do it also without the ML process from the build db.


	Makarius