Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

[Lawrence Paulson]

Many thanks for getting to the bottom of these problems!

All of these texts were copied from HOL Light. I can fix them sometime 
tomorrow, or feel free to do it yourself if you prefer.

--lcp

> On 15 Jun 2016, at 21:17, Manuel Eberl  wrote:
> 
> There is one instance in Extension.thy where you wrote "real ^ n" in a 
> subsection heading about Urysohn's lemma. That causes an error when 
> interpreted as LaTeX code. I suggest replacing it with "Euclidean space", 
> which is more apt in Isabelle anyway, I should think.
> 
> There are two more instances in Brouwer_Fixpoint.thy where you wrote 
> something like "R^n" in text, causing the same error.
> 
> Cheers,
> 
> Manuel
> 
> 
>> On 15/06/16 18:19, Lawrence Paulson wrote:
>> No idea what’s going on here. I did commit a lot of stuff but it works on my 
>> machine. I added a theory, but the addition was committed and I have no 
>> untracked files. If anybody can figure out what’s going on I'd be grateful. 
>> I see it is a document preparation failure, presumably that isn’t being 
>> checked locally for some reason?
>> 
>> Larry
>> 
>>> Begin forwarded message:
>>> 
>>> From: Isabelle/Jenkins 
>>> Subject: [Isabelle-ci] Build failure in Isabelle
>>> Date: 15 June 2016 at 17:14:27 BST
>>> To: isabelle...@mail46.informatik.tu-muenchen.de
>>> 
>>> The Isabelle build failed. See the log at: 
>>> https://ci.isabelle.systems/jenkins/job/isabelle-repo-makeall/249/
>>> 
>>> 
 ___
 Isabelle-ci mailing list
 isabelle...@mail46.informatik.tu-muenchen.de
 https://mailman46.informatik.tu-muenchen.de/mailman/listinfo/isabelle-ci
>>> 
>>> 
>>> 
>>> ___
>>> isabelle-dev mailing list
>>> isabelle-...@in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

[Manuel Eberl]

There is one instance in Extension.thy where you wrote "real ^ n" in a 
subsection heading about Urysohn's lemma. That causes an error when 
interpreted as LaTeX code. I suggest replacing it with "Euclidean 
space", which is more apt in Isabelle anyway, I should think.


There are two more instances in Brouwer_Fixpoint.thy where you wrote 
something like "R^n" in text, causing the same error.


Cheers,

Manuel


On 15/06/16 18:19, Lawrence Paulson wrote:

No idea what’s going on here. I did commit a lot of stuff but it works on my 
machine. I added a theory, but the addition was committed and I have no 
untracked files. If anybody can figure out what’s going on I'd be grateful. I 
see it is a document preparation failure, presumably that isn’t being checked 
locally for some reason?

Larry


Begin forwarded message:

From: Isabelle/Jenkins 
Subject: [Isabelle-ci] Build failure in Isabelle
Date: 15 June 2016 at 17:14:27 BST
To: isabelle...@mail46.informatik.tu-muenchen.de

The Isabelle build failed. See the log at: 
https://ci.isabelle.systems/jenkins/job/isabelle-repo-makeall/249/



___
Isabelle-ci mailing list
isabelle...@mail46.informatik.tu-muenchen.de
https://mailman46.informatik.tu-muenchen.de/mailman/listinfo/isabelle-ci




___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

[Lawrence Paulson]

No idea what’s going on here. I did commit a lot of stuff but it works on my 
machine. I added a theory, but the addition was committed and I have no 
untracked files. If anybody can figure out what’s going on I'd be grateful. I 
see it is a document preparation failure, presumably that isn’t being checked 
locally for some reason?

Larry

> Begin forwarded message:
> 
> From: Isabelle/Jenkins 
> Subject: [Isabelle-ci] Build failure in Isabelle
> Date: 15 June 2016 at 17:14:27 BST
> To: isabelle...@mail46.informatik.tu-muenchen.de
> 
> The Isabelle build failed. See the log at: 
> https://ci.isabelle.systems/jenkins/job/isabelle-repo-makeall/249/

build.log
Description: Binary data
> ___
> Isabelle-ci mailing list
> isabelle...@mail46.informatik.tu-muenchen.de
> https://mailman46.informatik.tu-muenchen.de/mailman/listinfo/isabelle-ci

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev