Re: [isabelle-dev] Uses of Jenkins at TUM

On 24/04/17 18:10, Lars Hupel wrote: >> In parallel (before and after Mira) we've had the older isatest. I don't >> know if Mira ever had the ambition to replace isatest, but Jenkins tried >> to do all that and failed. This was the start of my great worries about >> the Isabelle administration and

Re: [isabelle-dev] Uses of Jenkins at TUM

> In parallel (before and after Mira) we've had the older isatest. I don't > know if Mira ever had the ambition to replace isatest, but Jenkins tried > to do all that and failed. This was the start of my great worries about > the Isabelle administration and release infrastructure ... So, you're

Re: [isabelle-dev] Uses of Jenkins at TUM

> On 24 Apr 2017, at 17:12, Andreas Lochbihler > wrote: > > Sure. Whenever I have to push something to the Isabelle repository, I use the > Jenkins testboard installation to see whether something broke. It works more > reliably than the previous testboard

Re: [isabelle-dev] Uses of Jenkins at TUM

On 24/04/17 17:12, Andreas Lochbihler wrote: > Sure. Whenever I have to push something to the Isabelle repository, I > use the Jenkins testboard installation to see whether something broke. > It works more reliably than the previous testboard infrastructure, which > often ignored some commits.

Re: [isabelle-dev] Uses of Jenkins at TUM

Sure. Whenever I have to push something to the Isabelle repository, I use the Jenkins testboard installation to see whether something broke. It works more reliably than the previous testboard infrastructure, which often ignored some commits. Andreas On 24/04/17 14:46, Makarius wrote: This is

[isabelle-dev] NEWS: isabelle imports

*** System *** * Command-line tool "isabelle imports" helps to maintain theory imports wrt. session structure. Examples: isabelle imports -I -a isabelle imports -U -a isabelle imports -M -a -d '~~/src/Benchmarks' This refers to Isabelle/c556c09765dd. It is an emerging tool to help

[isabelle-dev] NEWS: GCD and Binomial in Main

*** HOL *** * Theories "GCD" and "Binomial" are already included in "Main" (instead of "Complex_Main"). This refers to Isabelle/f533820e7248: the change came up while exploring theory imports systematically. Normally, only "Main" or "Complex_Main" should be imported from the HOL session, not

Re: [isabelle-dev] Bad theory import "Main"

On 24/04/17 15:21, Lars Hupel wrote: > >> I actually offered an open dialog about it last December, and you >> rejected that. > > Because the offer consisted merely of rehashing things we already talked > about in person. To be completely frank, I'm tired of repeating myself > and others

Re: [isabelle-dev] Bad theory import "Main"

Hi Makarius, > The problem is in the HOL-Lib session from isafor. It is somewhere in > your ROOTS (or -d specifications). Ah! > Are you working with IsaFoR on purpose, or is this just an accident? That's it. I had IsaFoR as a component -- half on purpose, half by accident. Thanks for helping

Re: [isabelle-dev] Bad theory import "Main"

> This is still "blame game". If you say so. > I actually offered an open dialog about it last December, and you > rejected that. Because the offer consisted merely of rehashing things we already talked about in person. To be completely frank, I'm tired of repeating myself and others endlessly.

Re: [isabelle-dev] Bad theory import "Main"

On 24/04/17 14:36, Makarius wrote: > On 23/04/17 18:10, Blanchette, J.C. wrote: >> >> *** No such file: >> "/Users/blanchette/isabelle/src/HOL/Library/Fraction_Field.thy" >> *** The error(s) above occurred for theory "HOL-Lib.Fraction_Field" (line 17 >> of

Re: [isabelle-dev] Bad theory import "Main"

On 24/04/2017 14:24, Makarius wrote: In the past 1.5 years, I've spent a lot of time trying to explain how the Isabelle administration works. If we don't manage to overcome the "blame game", things will decline further. If you think I was trying to blame you for having forgotten to commit a

Re: [isabelle-dev] Bad theory import "Main"

On 24/04/17 14:46, Lars Hupel wrote: > Then, out of the blue, you stopped caring, > unsubscribed for strange reasons from the CI list and started calling > Jenkins a "monster" and a "waste of resources". > > It is because of that that I'm having a hard time believing that you're > willing to

[isabelle-dev] Uses of Jenkins at TUM

This is another attempt to open a discussion about Jenkins at TUM. Are there users of it outside the TUM group? What is good about it? What is bad about it? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] Bad theory import "Main"

On 23/04/17 18:10, Blanchette, J.C. wrote: > > Yes, it does both I guess. The "half-decent error message" looks like this: > > /Users/blanchette/isabelle/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar: > Cannot start: > *** No such file: >

Re: [isabelle-dev] Bad theory import "Main"

On 23/04/17 15:54, Tobias Nipkow wrote: > The Isabelle regression test system shows up a mistake in a commit of > yours and you ask what its purpose is? And tell us your rarely look there? That was a trivial mistake: easy to spot and easy to repair. We don't need a huge monster like Jenkins for