[isabelle-dev] Maintenance work on Jenkins VM

Lars Hupel hupel at in.tum.de
Sat Jan 30 21:48:58 CET 2016


Update:

> - running makeall and AFP (without "slow" sessions) on every push to
> Isabelle
> - running slow sessions nightly
> - utilize 4 workers (8 cores, 64 GB each) from the LRZ
> - running AFP (without "slow" sessions) on every push to AFP
> - running everything on every push to testboard

All of that should be working now. See the full glory here:

  <https://ci.isabelle.systems/jenkins/>

There are four major jobs, each of which may have minor jobs:

  - isabelle-repo-checkin
    - isabelle-repo-makeall
    - isabelle-repo-afp
  - isabelle-repo-nightly-slow
  - testboard-checkin
    - testboard-makeall
    - testboard-afp
  - afp-repo-checkin
    - afp-repo-afp

The first name part is the name of the "master" repository. Major jobs
containing "-checkin" get triggered on every push; those containing
"-nightly" get triggered once daily. "-slow" means building only the
sessions tagged "slow". All other jobs exclude those sessions. (In the
current setup, that means that testboard doesn't run slow sessions at all.)

Example: Someone pushes to the Isabelle repository. The
"isabelle-repo-checkin" detects this and kicks off a build with ID #5.
It then runs the minor jobs "isabelle-repo-makeall" and
"isabelle-repo-afp" in parallel, both with ID #5 as well. If either of
the minor jobs fails, the major job fails, too.

About the hardware: There are currently 4 worker machines. Each job can
take from 1-6 hours there (slowest: "isabelle-repo-nightly-slow" with
5h20m, fastest: "isabelle-repo-makeall" with 1h09m). There's currently a
problem with LRZ' VM management interface, but once that's fixed, I'll
add 4 more workers.

(NB: We don't have better hardware just yet, but I figured to better get
this running in time for post-release mode.)

Still missing in the setup:
* cross-platform/cross-parameter testing
* archival of the build logs
* time series

In any case, we can start thinking seriously about sunsetting isatest
and afptest now.

Cheers
Lars




More information about the isabelle-dev mailing list