Re: [isabelle] from thy to latex

On 28/02/17 23:28, Michel wrote:
> Le 28/02/2017 Ã 22:51, Makarius a Ãcrit :
>> On 28/02/17 22:46, Michel wrote:
>>> Now when I execute "isabelle build -D Test", I have a latex error. 
>>> ! File ended while scanning use of \next.
>>> <inserted text>
>>>                 \par
>>> l.1 \input{debut1.tex}
>>> I have tried the same thing on some archive of formal proofs.
>> Which operating system and latex installation do you have?
> My operating system is linux ubuntu 16.04 and I have the following latex
> installation ;
> michel at M1330:~/PropResPI/output/document$ latex -version
> pdfTeX 3.14159265-2.6-1.40.16 (TeX Live 2015/Debian)

The low-level latex version is usually irrelevant -- it never really
changes in its convergence towards pi.

What is important are the styles and classes.

On Ubuntu 16.04 you normally have texlive, which is fine. You merely
need to ensure that all its tiny little fragments produced by the Debian
guys are properly installed, e.g. texlive-fonts-extra,
texlive-latex-extra, texlive-math-extra.

I am using the same OS platform routinely, and it should not cause any
problems like the above.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.