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
On 24/04/17 14:46, Makarius wrote:
>
> Are there users of it outside the TUM group?
>
> What is good about it? What is bad about it?
(1) To follow the line of Mira vs. Jenkins:
* My main use of Mira was to figure out which Isabelle version
corresponds to which AFP version, when something was
> 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 ju
> 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 infrastructure, which often ignored s
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.
Tha
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
*** 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
sorting
*** 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 any
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 endlessl
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 m
> 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.
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 "/Users/blanchette/hgs/isafor/thys/ROOT"
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 fi
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 engag
> 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.
You yourself proposed investigating Jenkins (then Hudson) some while
ago, pointing out that e.g. the Scala te
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
https://mailmanbroy.info
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:
> "/Users/blanchette/isabelle/src/HOL/Library/Fraction_Fiel
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 th
18 matches
Mail list logo