Re: [isabelle-dev] Jenkins maintenance

[Makarius]

On 06/10/16 17:03, Tobias Nipkow wrote:
> Sorry, I don't consider them useless.
> 
> Tobias
> 
> On 06/10/2016 17:00, Makarius wrote:
>> This is actually my main point of criticism for the present situation:
>> the Jenkins setup uses a lot of hardware resources, by doing too many
>> useless tests.

I need to be more specific:

  * Why is a plain "nightly build" done many times per day? (As
immediate reaction on repository pushes.)

  * Why are testboard policies intermixed with "nightly build" policies?

Add-on question:

  * Why is there a testboard at all, instead of plain ssh access?


None of this has been seriously discussed so far.


As far as I remember, the original Mira testboard was introduced in a
situation, where builds became so slow and unwieldy that the mental
model was changed to "batch-queue management" on a hypothetical
computing cluster. Luckily, David Matthews saved us from that, and made
everything small and fast again.


Makarius

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

Re: [isabelle-dev] Jenkins maintenance

[Makarius]

On 06/10/16 15:36, Lawrence Paulson wrote:
> I don’t agree with this point at all. Fixing the errors is easy but locating 
> them certainly isn’t. I’m happy as long as somebody else is willing to do 
> that.
> Larry
> 
>> On 6 Oct 2016, at 14:02, Makarius  wrote:
>>
>>  * A broken Latex document is easy to repair.

Finding latex errors is indeed a bit awkward, but that is just a matter
of brushing up document preparation a bit.

Such a small pending reform of how Isabelle latex invocation works
should not have any impact on the model of Isabelle testing.


Makarius

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

Re: [isabelle-dev] Jenkins maintenance

[Tobias Nipkow]

Sorry, I don't consider them useless.

Tobias

On 06/10/2016 17:00, Makarius wrote:

This is actually my main point of criticism for the present situation:
the Jenkins setup uses a lot of hardware resources, by doing too many
useless tests.




smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Makarius]

On 06/10/16 16:44, Tobias Nipkow wrote:
> 
>> I also prefer to have AFP working all the time, but that would require
>> much more resources, both hardware and humans.
> 
> For a growing number of Isabelle users, the AFP is just as important as
> the Isabelle repository. Hence the AFP needs to be tested and maintained
> just as much, which requires (at least) the hardware resources that we
> provide; we cannot dedicate half of it to manual testing.

This is actually my main point of criticism for the present situation:
the Jenkins setup uses a lot of hardware resources, by doing too many
useless tests. These resources are then missing for important tests, as
well as interactive sessions.

This can be easily changed by giving up these design decisions:

  * quasi real-time reactivity (of what is actually a 1.5h batch build)

  * exclusive "provisioning" of machines for Jenkins


Makarius

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

Re: [isabelle-dev] Jenkins maintenance

[Tobias Nipkow]

On 06/10/2016 14:34, Makarius wrote:

On 03/10/16 17:12, Manuel Eberl wrote:

It would also be an effective safeguard against breaking the repository (and 
possibly even the AFP),
which /does/ happen quite frequently. (cf. the current situation where
things have been broken for days)


I also prefer to have AFP working all the time, but that would require
much more resources, both hardware and humans.


For a growing number of Isabelle users, the AFP is just as important as the 
Isabelle repository. Hence the AFP needs to be tested and maintained just as 
much, which requires (at least) the hardware resources that we provide; we 
cannot dedicate half of it to manual testing.


Leaving the AFP entries broken actually increases the human resources required 
to fix them later.



A broken Isabelle repository is different: it means all wheels stand
still.


Both for the repository and the AFP, everything is selective. Most people do not 
suffer if HOL-Proofs does not build, for example. Just as many AFP entries are 
irrelevant to most of us. But in the end we want all of it to work.


Tobias


That can be easily avoided by spending about 20min with manual
tests before pushing -- on decent hardware.

When the Isabelle repository is broken, which happens about 2 times per
year, there are friendly mails on isabelle-dev about it, mostly
reminders of README_REPOSITORY. Can you point out a mail thread, where
anybody was seriously blamed for it?



Another improvement I can think of is
that it would be good to have a little more control over testing:
aborting tests when they are not necessary anymore, testing only the
repository (and not the AFP) etc. All of this we can talk about and find
a solution in time.


Yes. I read it as: ssh access to a proper test machine. That is the
traditional Isabelle development model.

When the Prover IDE learns to use remote machines eventually, that will
also use ssh for direct interaction with jobs.



The reality of it all is that our testing infrastructure was in shambles for
quite some time. Then Lars came along and put in a lot of effort to get
things up and running again. The main response on this mailing list were
vague insinuations that he does not understand how to do tests, or does
not care about doing it properly, which could hardly be farther removed
from the truth.


I had many private discussions with Lars in the past few months. I even
pointed out important requirements before the start of the Jenkins project.

The present situation is that we have no proper test environment after
isatest was shutdown prematurely. This is what I have called "flying
blind", because vital performance measurements are missing.

I need to improvise something for the coming release -- which is the
reason why I have been off-line for some days, and also postponed the
start of the hot phase for Isabelle2016-1.


Makarius

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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Makarius]

On 06/10/16 15:22, Lawrence Paulson wrote:
> I have a Mac Pro, and I just use “isabelle build -a”.  Maybe I could use 
> multithreading more (the machine supports 12 cores).

There is a certain art to combine build options -j N and -o threads=M,
depending on the hardware (based on manual experiments).

On my own 2 * 6 core machine, I usually use this:

  isabelle build -j4 -a -o threads=6

and settings as follows:

  ML_OPTIONS="-H 1500 --gcthreads 6"


> If I know that my changes affect specific AFP entries, I run
> them manually.

I've also found myself doing the prediction in my head. Some tool
support for that would be nice, but I have no concrete ideas right now.


> A full test takes a couple of hours, and it is a pain.

What I often do is

  isabelle build -j4 -a -d '$AFP' -X slow

It takes approx. 1h, but is changing quickly recently, due to massive
inflow of new AFP entries (which is a very good thing).


Makarius

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

Re: [isabelle-dev] Jenkins maintenance

[Lawrence Paulson]

I don’t agree with this point at all. Fixing the errors is easy but locating 
them certainly isn’t. I’m happy as long as somebody else is willing to do that.
Larry

> On 6 Oct 2016, at 14:02, Makarius  wrote:
> 
>  * A broken Latex document is easy to repair.

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

Re: [isabelle-dev] Jenkins maintenance

[Lawrence Paulson]

I have wanted to keep out of this rather fraught discussion, but I agree on 
this issue. How dangerous it is depends on how critical those secrets are. And 
I’m perfectly aware that key management can be difficult and maybe there is 
little point if only one instance of this thing is running. Still, it isn’t 
ideal.

Larry

> On 6 Oct 2016, at 13:00, Makarius  wrote:
> 
> Putting secrets into a repository is a bad idea -- they stay there
> forever, even if they are "deleted" in some versions. When it is clone
> eventually, secrets will leak.

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

Re: [isabelle-dev] Jenkins maintenance

[Lawrence Paulson]

I have a Mac Pro, and I just use “isabelle build -a”. If I know that my changes 
affect specific AFP entries, I run them manually. A full test takes a couple of 
hours, and it is a pain. Maybe I could use multithreading more (the machine 
supports 12 cores).

Larry

> On 6 Oct 2016, at 13:05, Makarius  wrote:
> 
> Larry, can you describe your own build/test process?
> 
> 
> I have just used the new Jenkins testboard for the first time, and was a
> bit disappointed by the very long runtimes: about 1.5h each for Isabelle
> and AFP.
> 
> Mira set out to deliver Isabelle tests "In 10min!" (Bavarians need to
> think of the famous Stoiber speech here).
> 
> 
> I am doing manual Isabelle tests on my own machin in approx. 30min,
> which is already a bit painful. 20min is OK, 10min would be delightful.
> 
> At some point I need to convene with David Matthews again, to see if and
> how we manage another jump forward in general performance.

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

Re: [isabelle-dev] The HOL Light library

[Lawrence Paulson]

And now that I have managed to prove “invariance of domain”, a significant if 
not especially famous result.
Larry

> On 6 Oct 2016, at 14:08, Makarius  wrote:
> 
> Definitely. It is probably worth a line to the ANNOUNCE file for
> Isabelle2016-1.

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

Re: [isabelle-dev] Jenkins maintenance

[Makarius]

On 06/10/16 15:07, Lars Hupel wrote:
> In fact, the situation was even worse back then: Various Isabelle
> developers have told me that they're using "macbroy2" which would
> otherwise be used for isatest/afptest for private experiments. Since a
> full test run would sometimes take some 10 hours, collisions were pretty
> much guaranteed.
> 
> There cannot be useful performance measurements unless the environment
> is controlled, i.e. free of other accesses.

The general policies are rather simple:

  * automated tests are run during the night

  * humans use the same hardware during the day

  * everybody understands the difference, and takes care to avoid conflicts


For the new hardware, it could be done slightly differently:

  * CPU 0 is exclusive for automated tests

  * CPU 1 is exclusive for manual tests

>From the hardware architecture, such a clear separation of the two CPU
sockets with their local memory modules could work, but it requires
proper physical experiments prove that.

Splitting a single CPU socket into logical parts (as done now) is likely
to cause conflicts via caches. It might be one of the reasons, why the
current Jenkins measurements are still quite erratic.

Moreover, enabling hyperthreading on the CPU for manual testing would
give another factor of 1.2.


Makarius

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

Re: [isabelle-dev] The HOL Light library

[Makarius]

On 03/10/16 15:16, Lawrence Paulson wrote:
> I’ve just added a lot more advanced material from HOL Light. There isn't much 
> about this in the NEWS file; unfortunately there is no headline result to 
> mention or even a dominant theme. Nor can we say that the entire library has 
> been ported. But I still think it’s a significant development for the next 
> release.

Definitely. It is probably worth a line to the ANNOUNCE file for
Isabelle2016-1.


Makarius

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

Re: [isabelle-dev] Jenkins maintenance

[Lars Hupel]

> I had many private discussions with Lars in the past few months. I even
> pointed out important requirements before the start of the Jenkins project.

I am aware of that (I keep notes), and also of the relevant email
threads dating back to 2014.

> The present situation is that we have no proper test environment after
> isatest was shutdown prematurely. This is what I have called "flying
> blind", because vital performance measurements are missing.

This was already your criticism in 2014, because the performance
measurements weren't even that good when I took over. At some point, you
showed me the "/devel" graphs and explained to me that we need something
better for serious measurements. I fail to see how the situation is now
somehow worse than what we had with isatest.

In fact, the situation was even worse back then: Various Isabelle
developers have told me that they're using "macbroy2" which would
otherwise be used for isatest/afptest for private experiments. Since a
full test run would sometimes take some 10 hours, collisions were pretty
much guaranteed.

There cannot be useful performance measurements unless the environment
is controlled, i.e. free of other accesses.

> I need to improvise something for the coming release -- which is the
> reason why I have been off-line for some days, and also postponed the
> start of the hot phase for Isabelle2016-1.

What exactly do you have to improvise?

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

Re: [isabelle-dev] Jenkins maintenance

[Makarius]

On 05/10/16 18:07, Lars Hupel wrote:

>> 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
>  (including documents) is being produced by
> Jenkins. Failure to produce a document in that sense is also a failure
> to present an entry.

"Continous delivery" seems to be one of the Jenkins defaults that
suddenly intrude the Isabelle development process.

The reasons, why generated PDFs for the Isabelle repository should not
be required:

  * It demands precious additional minutes in the main build (with its
target for 10-20min, but presently going slightly beyond 30min on my
machine).

  * A broken Latex document is easy to repair.

So if nobody tests PDFs seriously, that is a gain for everyone. There
could be a weekly or monthly test to point out latex problems automatically.


For AFP, with its focus on PDF articles, the situation is certainly
different. But AFP is not the Isabelle repository.

Many of the open problems are caused by putting everything in one pot:
Isabelle, AFP, testboard, nightly builds with serious measurements.


> 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.

There is already "isabelle build_doc -a". It could be included in a
separate build job.

Even more, there could be a nightly job to run "Admin/Release/build" and
publish the resulting mini website, as a rplacement of
http://isabelle.in.tum.de/devel with its "Download".


>> 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.

I pointed out the importance of the threads=1 test several times. A
proper test setup needs to provide a "mostly flat line" as reference for
anything else. That has been Isabelle standard for almost 10 years, and
was only recently lost.

Without that, performance tuning becomes very difficult. It is one of
the reasons, why no serious tuning has happened recently.


> As always, I first need to figure out how long this takes on our
> hardware and if necessary, provision an appropriate machine.

I don't like this idea of exclusive "provisioning" of machines for the
Jenkins monster. It is the main reason why test hardware is lacking.

It is a paradoxical situation of both wasting a lot of CPU resources,
and of scarcity and austerity.


> It would also be great if, as we discussed, there was a possibility to
control
> "ML_OPTIONS" via options instead of environment variables.

This is now addressed by the new Admin/build_history tool (presently
2c5039363ea3), but that is a different story for a different thread.


> 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.

I have already started to think about the problem of integrating test
data into Isabelle history myself.

Presently there are two main questions:

  * Is it feasible to have a standard database server hosted at TUM
(that can run the next 10 years), and be publicly accessible by some
standard protocol and standard authentication?

  * What are the prospects for generally available test hardware --
non-exclusive as in the past?


> 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.

Such discussions always need to true sources at hand. Where are the
Isabelle/Jenkins sources?


Makarius

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

Re: [isabelle-dev] Jenkins maintenance

[Lars Hupel]

> I have often wondered how certain details are done by Jenkins, e.g.
> logging into a remote machine, controlling the job and getting its results.

Your use of the term "Isabelle/Jenkins" led me to believe that you're
interested in the Ansible scripts. If you're instead interested in
Jenkins sources in general, that's an easy question to answer:

  

And more specifically, the "remote machine" part:

  

There aren't any custom plugins running in our Jenkins instance.

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

Re: [isabelle-dev] Jenkins maintenance

[Lars Hupel]

> I have just used the new Jenkins testboard for the first time, and was a
> bit disappointed by the very long runtimes: about 1.5h each for Isabelle
> and AFP.

This is slightly misleading, because the total time spent waiting for
both is typically 1:30 hours; Jenkins runs them in parallel if possible.
The last three or so testboard runs didn't spend time waiting in the queue.

> Mira set out to deliver Isabelle tests "In 10min!" (Bavarians need to
> think of the famous Stoiber speech here).
> 
> I am doing manual Isabelle tests on my own machin in approx. 30min,
> which is already a bit painful. 20min is OK, 10min would be delightful.

Here's my quick back-of-the-envelope calculation:

Our current testboard setup runs AFP with -j8 -o threads=2, that is, on
16 cores. It requires an elapsed time of 1:30 and 20:30 CPU hours.

Isabelle "build -a" runs with -j3 -o thread=2 (total 6 cores), with an
elapsed time of 1:20 and 6:45 CPU hours.

Let's just discount multithreading overhead for a bit here (it's two
threads per process anyway). We're getting a total of about 27 CPU
hours, give or take.

In order to process that full workload in 30 minutes, that would require
in the order of 50 cores with full load. We're close with a total of 44
cores. But for fairness, we're running the workload not on the full
number of cores, but rather just half.

In any case, I don't see how anything less than 30 minutes can be done
with reasonable hardware. And if at some point there are enough
improvements that it can be done on hardware, it's orthogonal to
Mira/Jenkins/whatever ...

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

Re: [isabelle-dev] Jenkins maintenance

[Makarius]

On 03/10/16 17:12, Manuel Eberl wrote:
> 
> 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.

When we introduced Mercurial in 2008, this was one idea to aim at
eventually. Today, I would refrain from any automatic daemon producing
changesets.

Instead, it should be easy and painless for human users to do that
themselves. At some point, builds could be integrated nicely into the
Prover IDE, together with regular Mercurial repository operations.


> It would also be an effective safeguard against breaking the repository (and 
> possibly even the AFP),
> which /does/ happen quite frequently. (cf. the current situation where
> things have been broken for days)

I also prefer to have AFP working all the time, but that would require
much more resources, both hardware and humans.

A broken Isabelle repository is different: it means all wheels stand
still. That can be easily avoided by spending about 20min with manual
tests before pushing -- on decent hardware.

When the Isabelle repository is broken, which happens about 2 times per
year, there are friendly mails on isabelle-dev about it, mostly
reminders of README_REPOSITORY. Can you point out a mail thread, where
anybody was seriously blamed for it?


> Another improvement I can think of is
> that it would be good to have a little more control over testing:
> aborting tests when they are not necessary anymore, testing only the
> repository (and not the AFP) etc. All of this we can talk about and find
> a solution in time.

Yes. I read it as: ssh access to a proper test machine. That is the
traditional Isabelle development model.

When the Prover IDE learns to use remote machines eventually, that will
also use ssh for direct interaction with jobs.


> The reality of it all is that our testing infrastructure was in shambles for
> quite some time. Then Lars came along and put in a lot of effort to get
> things up and running again. The main response on this mailing list were
> vague insinuations that he does not understand how to do tests, or does
> not care about doing it properly, which could hardly be farther removed
> from the truth.

I had many private discussions with Lars in the past few months. I even
pointed out important requirements before the start of the Jenkins project.

The present situation is that we have no proper test environment after
isatest was shutdown prematurely. This is what I have called "flying
blind", because vital performance measurements are missing.

I need to improvise something for the coming release -- which is the
reason why I have been off-line for some days, and also postponed the
start of the hot phase for Isabelle2016-1.


Makarius

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

Re: [isabelle-dev] Jenkins maintenance

[Makarius]

On 03/10/16 17:31, Lawrence Paulson wrote:
> I’d be happy with this, if it’s achievable.
> 
> I’ve only tried the testboard once or twice; I find it too easy to do the 
> wrong thing when you have a choice of targets to push to, and I have a 
> powerful machine so I prefer to test there. But a mechanism of the sort you 
> describe (provided it’s easy to use) would be ideal.

Larry, can you describe your own build/test process?


I have just used the new Jenkins testboard for the first time, and was a
bit disappointed by the very long runtimes: about 1.5h each for Isabelle
and AFP.

Mira set out to deliver Isabelle tests "In 10min!" (Bavarians need to
think of the famous Stoiber speech here).


I am doing manual Isabelle tests on my own machin in approx. 30min,
which is already a bit painful. 20min is OK, 10min would be delightful.

At some point I need to convene with David Matthews again, to see if and
how we manage another jump forward in general performance.


Makarius

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

Re: [isabelle-dev] Jenkins maintenance

[Makarius]

On 01/10/16 22:38, Lars Hupel wrote:
>> And where are the public sources of Isabelle/Jenkins?
> 
> I feel like the other readers on this thread should know that you have
> asked me exactly the same question when you last visited Garching. I
> explained to you that some parts of the infrastructure cannot be public
> because they contain passwords and private keys. As for the public bits,
> you have already found and changed them.
> 
> Given the apparent "rhetoric" nature of this question I can no longer
> assume that you are arguing in good faith.

I have asked this question several times privately, and always got the
same answer.

Putting secrets into a repository is a bad idea -- they stay there
forever, even if they are "deleted" in some versions. When it is clone
eventually, secrets will leak.


The reasons why I am asking for public sources are manifold, including
general "open-source" reasons: work can be inspected, discussed, reused etc.

I have often wondered how certain details are done by Jenkins, e.g.
logging into a remote machine, controlling the job and getting its results.

Moreover, just empirically from what I have seen in the last 10-15
years: Isabelle infrastructure that is not easily accessible does not
survive very long. (Mira was an example for that.)


Makarius

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