[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 <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.
>>
>> 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 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
>>>>> https://mailman46.informatik.tu-muenchen.de/mailman/listinfo/isabelle-ci
>>>>
>>>>
>>>>
>>>> _______________________________________________
>>>> isabelle-dev mailing list
>>>> isabelle-dev at in.tum.de
>>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>