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