[isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

[Makarius]

On 09/08/16 23:51, Makarius wrote:
> On 08/08/16 14:44, Lars Hupel wrote:
>>
>> For HOL-Proofs, the relevant job is "isabelle-repo-makeall". A catalog
>> of all builds and all archived logs can be found under the following URL:
>>
>>
>> <https://ci.isabelle.systems/jenkins/job/isabelle-repo-makeall/api/json?pretty=true&tree=builds[url,number,timestamp,artifacts[*]]>
> 
> I did not know of this JSON API yet. In Isabelle/74604a9fc4c8 there are
> Isabelle/Scala operations to access that information. (It is an
> interesting experience to work with these untyped JSON things; reminds
> me of LISP expressions.)
> 
> I will later work out, if this is going to be a batch tool (like former
> isatest-stats) or a PIDE GUI panel. It might be actually easier to make
> proper a GUI application than a web application from it.

For now I've made a batch tool, see Isabelle/b7aab1a6cf0d. Here is an
example invocation:

  build_stats -S HOL,HOL-Proofs -s 1024x768 isabelle-repo-makeall
isabelle-nightly-benchmark

Resulting PNGs are attached (the actual result contains some HTML around
that).


Now we see that we see nothing: the repo-makeall test data looks as
messy as a climate change diagram!

This is probably a consequence of running the regular test against
itself with option -j. The nightly-benchmark does not do that for main
HOL, so it is much better. There might be also a problem from the
virtualization of the machine, meaning that the nightly-benchmark is
only clean as long as no other virtual slice is active: this needs to be
practically verified.


Note that the isatest runs were carefully crafted not to conflict with
anything else, using -j1 and threads=1,2,4,8 for meaningful
measurements. (Threads=2 is actually relatively uninteresting.)

Is it possible to let Jenkins redo the changes from the last 4 weeks
with a setup that produces good physical measurements?


	Makarius

-------------- next part --------------
A non-text attachment was scrubbed...
Name: HOL-Proofs_isabelle-repo-makeall.png
Type: image/png
Size: 13129 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160816/30459af1/attachment-0006.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: HOL_isabelle-repo-makeall.png
Type: image/png
Size: 13598 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160816/30459af1/attachment-0007.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: HOL_isabelle-nightly-benchmark.png
Type: image/png
Size: 11434 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160816/30459af1/attachment-0008.png>