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 <ebe...@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.
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 <ci@isabelle.systems>
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
