Quoting Alexander Krauss :
- Missing email notification
Here is some room for discussion: What would be a good notification
scheme? Since tests are now run continuously, sending an email after
each run is not really an option. Should we simply go for a daily
summary? More sophisticated
Excellent – we're roaring ahead…
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_
On 05/30/2011 12:33 PM, Andreas Lochbihler wrote:
Hi Lukas,
here is an example that I would have expected to work. However,
congruences seem to work other than I expected. Du you know what I am
missing here?
theory Scratch imports Main begin
definition test where "test xs = (last xs = 0)"
de
There were broken index entries in most of the old documentation. For some
reason, the | symbol didn't cause a problem in the tutorial. One index entry
here was fixed to use ?? (as opposed to !) as the sort key.
Larry
On 30 May 2011, at 15:28, Lawrence Paulson wrote:
> It seems it can be fixed
It seems it can be fixed by
(a) using ! rather than | as the sort key (the sorting of special symbols is
arbitrary anyway)
(b) using \char124 to denote the | symbol
I would expect to see this problem in any index entry involving the | symbol.
Larry
On 30 May 2011, at 14:58, Lawrence Paulson wr
My impression from fooling around a little is that this is a bug that has been
around for a year and a half. The comment seems to suggest that | no longer
works as an index item (even when protected using"), so we have to give up
index entries for the symbols | and |-|. I wonder whether there is
hg push -f testboard
I use queues a lot and usually do all testing before I "qfinish" the queued
patches. Is there a Mercurial trick to push all the applied queues without qfinishing
them first?
hg push -f actually does push applied mq patches as normal changesets,
so it should do exactly
Hi Alex,
> In the past weeks, there has been some progress with our new testing
> infrastructure, which I would like to summarize here. Please give
> feedback, ask questions, and discuss.
Great!! Thanks for the update. I just have one question related to testboard:
> Then, local changes can be p
Done now, I hope
Larry
On 30 May 2011, at 08:10, Andreas Lochbihler wrote:
> This fix solves the problem with the exception. I tried it with 574613b47583.
> Can you add it to the repository as I do not have wirte access to that.
___
isabelle-dev maili
Hi Lukas,
here is an example that I would have expected to work. However, congruences seem
to work other than I expected. Du you know what I am missing here?
theory Scratch imports Main begin
definition test where "test xs = (last xs = 0)"
definition test2 where "test2 xs = (xs ~= [] & test (r
On 05/30/2011 10:31 AM, Andreas Lochbihler wrote:
Thanks Lukas and Florian.
I guess that it *is* a corner case in my specifications, because I
have a conditional code equation that implements one constant x in
terms of another y. However, I use x only in the equation of another
constant z whi
Hi all,
The nightly isatest stopped working after the tex distribution on our
servers was updated to Tex Live 2010 (at least we suspect that this is
the cause of the problem).
This seems to be an obscure latex problem that arises when buliding
doc-src/Logics. It seems that the (generated!) f
Thanks Lukas and Florian.
I guess that it *is* a corner case in my specifications, because I have a
conditional code equation that implements one constant x in terms of another y.
However, I use x only in the equation of another constant z which tests for the
precondition first. At the moment,
Hi Andreas,
the following ML line should do the job of adding the congruence rule in
your case:
setup {* Code_Preproc.map_pre (fn ss => ss addcongs [@{thm conj_cong}]) *}
Before we add yet another feature to the code generation setup in Isar,
we would like to understand your scenario.
Does
Awesome! It looks positively industrial in scale.
Larry
On 30 May 2011, at 08:54, Alexander Krauss wrote:
> Hi all,
>
> In the past weeks, there has been some progress with our new testing
> infrastructure, which I would like to summarize here. Please give
> feedback, ask questions, and discuss.
Hi all,
In the past weeks, there has been some progress with our new testing
infrastructure, which I would like to summarize here. Please give
feedback, ask questions, and discuss.
Really fast status for "isabelle makeall"
=
Thanks to a new fat server wi
This fix solves the problem with the exception. I tried it with 574613b47583.
Can you add it to the repository as I do not have wirte access to that.
Thanks,
Andreas
Lawrence Paulson schrieb:
Thank you for looking there! This is the most plausible culprit. But it is
strange that this problem
17 matches
Mail list logo
