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

2018-05-16 Thread 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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


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

2018-05-16 Thread Lars Hupel

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:


https://ci.isabelle.systems/jenkins/job/afp-repo-afp/1592/consoleFull

Of note are these warnings:

15:37:27 ### Ignoring bad database: 
"/media/data/jenkins/workspace/afp-repo-afp/heaps/polyml-5.7.1_x86_64-linux/log/Fishburn_Impossibility.db"
15:37:27 ### Ignoring bad database: 
"/media/data/jenkins/workspace/afp-repo-afp/heaps/polyml-5.7.1_x86_64-linux/log/FocusStreamsCaseStudies.db"
15:37:27 ### Ignoring bad database: 
"/media/data/jenkins/workspace/afp-repo-afp/heaps/polyml-5.7.1_x86_64-linux/log/HLDE.db"
15:37:27 ### Ignoring bad database: 
"/media/data/jenkins/workspace/afp-repo-afp/heaps/polyml-5.7.1_x86_64-linux/log/IEEE_Floating_Point.db"
15:37:27 ### Ignoring bad database: 
"/media/data/jenkins/workspace/afp-repo-afp/heaps/polyml-5.7.1_x86_64-linux/log/Program-Conflict-Analysis.db"
15:37:28 ### Ignoring bad database: 
"/media/data/jenkins/workspace/afp-repo-afp/heaps/polyml-5.7.1_x86_64-linux/log/Residuated_Lattices.db"
15:37:28 ### Ignoring bad database: 
"/media/data/jenkins/workspace/afp-repo-afp/heaps/polyml-5.7.1_x86_64-linux/log/Rewriting_Z.db"
15:37:28 ### Ignoring bad database: 
"/media/data/jenkins/workspace/afp-repo-afp/heaps/polyml-5.7.1_x86_64-linux/log/Shivers-CFA.db"


It also happened with the previous build on the same machine:

https://ci.isabelle.systems/jenkins/job/afp-repo-afp/1588/consoleFull

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev