Thank you for bringing the discussion back on track. Let me try to address the remaining points.
> I for one think that a big improvement would be a system where no one > pushes to the repository directly: every push goes to a testing server, > and if the test is successful, the changes can then automatically be > merged into the repository without an additional test. This avoids the > current duplication of tests where one first pushes to the testboard, > waits for everything to run through, and then pushes to the repository > where everything is tested again. This is definitely achievable; however, it needs broad developer consensus first, because it's a change in the usual workflow. Consider this a call for opinions. Granted, the duplication of tests is an issue, but unfortunately, hard to avoid under the current circumstances. By changing the workflow to make breaking changes (except possibly AFP) "syntactically impossible", many things can be simplified. Bitbucket, for example, has facilities to enable such a workflow. However, before we do that, we need to think carefully about formalising the connection between Isabelle and the AFP. I'll let others take the lead on this – Florian, maybe? Also note that the status page now includes a load diagram. While the interpolation is somewhat strange, it shows a clear trend: the infrastructure is operating below 50% capacity. > According to the official README_REPOSITORY > (http://isabelle.in.tum.de/repos/isabelle/file/ec0fb01c6d50/README_REPOSITORY#l282) > there is > > * no need to test pdf documents This is arguable. In fact, it is very convenient to have documents in a continually working state, because Jenkins also serves a "continuous delivery" purpose: The AFP statistics page, and also everything else on <https://devel.isa-afp.org/> (including documents) is being produced by Jenkins. Failure to produce a document in that sense is also a failure to present an entry. In the long term, it could also make sense to present the official Isabelle documentation (i.e. everything in "~~/src/Doc") in a similar fashion. Currently users have to build documents themselves. > The 1 thread test is the base of all other tests. Without that it > becomes very difficult to see anything concerning performance changes. This is not a problem; I have it on my list anyway. Makarius, last time we spoke I didn't get the impression that this is crucial for performance analysis, which is why I didn't prioritize it. As always, I first need to figure out how long this takes on our hardware and if necessary, provision an appropriate machine. It would also be great if, as we discussed, there was a possibility to control "ML_OPTIONS" via options instead of environment variables. > I am still hoping for October (which is actually now). I have explained > many times privately, what the purpose of "platform tests" is: a > portfolio of officially supported platforms -- some of them unusual for > most isabelle-dev users -- need to be continuously tested (meaning once > per day, or even once per week). Together with Thomas Fritz I have already provisioned a native (i.e. non-virtualized) El Capitan worker a week ago [0]. It runs a nightly "build -a" job [1], 32 bit, 2 threads. It requires approx. 5 h for that. It also doesn't send messages on failure (currently). Makarius, if you'd like to be subscribed to build mails, please tell me. Otherwise it'll stay silent. > Mira was actually quite good in adjoining information to the repository > history views of the two repositories. Over a few years, that was the > main tool for me to figure out what works and what not, and to see when > it stopped working etc. Right now, it requires much more clicking, and I > am still unsure where the information is actually hidden. The reason why it was "quite good" is that it was tightly coupled to the Mercurial API; this is also the reason for its eventual demise. There are two possible proper solutions for this, "push" and "pull". Pull: Implement a loosely-coupled extension for hgweb to fetch information from Jenkins. All changesets and their statuses are recorded in there and can be retrieved from the API, not unlike the statistics page. This can be done with Javascript and implemented without changing anything in Jenkins. Push: Embrace Bitbucket and use their "Build Status" API [2]. This information is displayed in the "Builds" column in the "Commits" view. Of course, this only works for repositories hosted on Bitbucket. This likely requires some Scala code to work (i.e. performing an authenticated HTTP request). I'd be happy if someone other than me could take the lead on this. > Also note that the Mira architects were actually looking at Jenkins at > that time, and pointed out that it was a bit old-fashioned in focusing > on "latest" versions by default and lacking proper changeset identification. I don't understand what that means. "Changeset identification" works perfectly fine. In fact, many of the jobs in our current setup are triggered with explicit changeset ids. > This means, any Isabelle tools built on top of Jenkins need to try hard > to do it the proper way, e.g. working over timeless / stateless > Mercurial history in a monotonic fashion. Views should make it easy to > see "into the history", without requiring a lot of clicking. The Jenkins build history is also monotonic. Some additional glue code is required to connect that history to the Mercurial history. But as sketched above, that requires much less than Mira, which used an additional database to store this information. > 2) Further, »keep it simple, stupid« came to its limits with all the > involved technicalities: issues jobs on remote machines, exception > handling, proper daemonizing – it is surely easy to extend that list. > The Jenkins universe, as fas as I can tell, embodies significant > expertise in that area which you don't want to reimplement. In software engineering, this is known as "Not Invented Here" syndrome :-) > * How much efforts are required to make proper use of it? I.e. what is > the "payload" of it as a "carrier system" for an actual application. The advantages, as outlined by Florian, by far outweigh the efforts. > * Which policies and attitudes of the platform are forced on the > application? How easy (or difficult) is it to reshape it for our the > requirements. This – of course – greatly depends on the requirements. Jenkins itself is infinitely malleable through plugins and configuration. But one needs to carefully evaluate which requirements are inherent and which are incidental based on the past. Outside of Isabelle, I've already gathered a lot of experience with setting up and maintaining build systems (not just Jenkins) and the usual insight is that if it's complicated to implement in the build system, it's worth looking closely how to simplify the underlying structure. Of course, that's nothing new for Isabelle users: the simpler the definition, the easier the proof. > And where are the public sources of Isabelle/Jenkins? I have thought about this again and decided that it's not worth separating the private from the public parts. There are three reasons: 1) It needlessly complicates the setup. This is not an insurmountable obstacle, but it requires some additional effort from my end. 2) Changes in the infrastructure can only be done by someone who is familiar with how the whole setup works and has root access to the underlying machines and configuration interfaces. Even if the sources were public and could be changed, there'd still be the manual step of deploying them. 3) When we're talking about what actually gets executed by Jenkins, it's rather boring: it runs a single script which resides in "~~/Admin". The rest of the sources is responsible for painstakingly creating a uniform environment (from scratch or incrementally) on all three kinds of machines we have currently; i.e. not interesting outside TUM. Despite that, I don't want to leave the impression of a lack of transparency, which is why I will take two measures in the near future: 1) Publish the private documentation of how the system works, which I have made available so far to anyone who asked. If anyone else is interested in reading the other parts of the sources, please ask. 2) Open a public tracker for issues and proposals about the infrastructure. This will also make it easier to track changes. Cheers Lars [0] <https://ci.isabelle.systems/jenkins/computer/workermac1/> [1] <https://ci.isabelle.systems/jenkins/job/isabelle-nightly-mac/> [2] <https://developer.atlassian.com/bitbucket/api/2/reference/resource/repositories/%7Busername%7D/%7Brepo_slug%7D/commit/%7Bnode%7D/statuses/build> _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev