Hi all,
the latest failures of the isabelle test of the form:
/tmp/isabelle-isatest25132/Quickcheck_Narrowing6407933/Generated_Code.hs::XX:
Conflicting definitions for `ad'
Bound at:
/tmp/isabelle-isatest25132/Quickcheck_Narrowing6407933/Generated_Code.hs::XX-XX
On Wed, 11 Jan 2012, Makarius wrote:
On Wed, 11 Jan 2012, Lukas Bulwahn wrote:
I bisected the failure further on my local machine and it turns out it is
related to the changeset
changeset: 46143:463b594e186a
user:wenzelm
date:Fri Jan 06 20:18:49 2012 +0100
summary:
Just another fine point concerning the 'a set business in current
Isabelle/7f6668317e24: when remaking doc-src/TutorialI there is a change
in doc-src/TutorialI/Inductive/document/Advanced.tex due to lists_Int_eq.
Its name indicates set operations, but it is now more general:
listsp (inf
On 01/05/2012 10:22 AM, Makarius wrote:
I think one could publish ~isabelle/contrib_devel via HTTP, although
it would require some clean up and tuning, say to expand symlinks.
Another question is how to export the actual directory structure,
without maintaining explicit index.html and tar.gz
On 01/11/2012 09:29 PM, Alexander Krauss wrote:
The real problem is in fact JinjaThreads. AFAIK, the only machine at
TUM where it can still build (in principle) is lxbroy10, but as Lukas
pointed out there are still some failures, cf.
