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

[Lawrence Paulson]

I’m taking care of it
Larry

> On 16 Jun 2016, at 10:44, Manuel Eberl  wrote:
> 
> Sure, I can do that later today.

___
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]

Sure, I can do that later today.

By the way, "isabelle build -o document=pdf HOL-Multivariate_Analysis" 
builds the session with document processing enabled. If it fails, it 
tells you both the location of the document directory (with all the 
generated LaTeX files) and the build log.


In my experience, the build log is often too long for me to find the 
errors in it, so I usually just go to the document directory, run 
"pdflatex root.tex" and see where it gets stuck.


Cheers,

Manuel



On 16/06/16 00:13, Lawrence Paulson wrote:

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