On 06/10/2016 17:11, Makarius wrote:
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 t
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.
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
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
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 te
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 pre
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 experiment
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.
__
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
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, Makar
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.
___
is
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, c
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 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
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
> 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 sourc
> 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 poss
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
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 mech
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 c
20 matches
Mail list logo
