[isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle
lp15 at cam.ac.uk
Thu Jun 16 00:13:56 CEST 2016
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.
> On 15 Jun 2016, at 21:17, Manuel Eberl <eberlm at in.tum.de> 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.
>> 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?
>>> Begin forwarded message:
>>> From: Isabelle/Jenkins <ci at isabelle.systems>
>>> Subject: [Isabelle-ci] Build failure in Isabelle
>>> Date: 15 June 2016 at 17:14:27 BST
>>> To: isabelle-ci at 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-ci at mail46.informatik.tu-muenchen.de
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev