Email Gateway (Aug 22 2022 at 15:09): Email Gateway (Aug 22 2022 at 15:09):From: Michel via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
How to obtain a tex file from a thy file ?
Under JEdit, I have tried "Plugins>Code2HTML>Latex current buffer" but
the tex file obtained contains many definitions of the same commands.
Email Gateway (Aug 22 2022 at 15:09):From: Makarius <makarius@sketis.net>
Isabelle document preparation is done on the command-line, without the
Prover IDE.
Short version:
isabelle mkroot -d Test && isabelle build -D Test
Long version: read chapter 3 of the "system" manual (e.g. from
Documentation panel).
Makarius
Email Gateway (Aug 22 2022 at 15:10):From: Makarius <makarius@sketis.net>
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.
Makarius
Email Gateway (Aug 22 2022 at 15:12):From: Michel via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
I forgot to send this mail to the list of Isabelle user and I hope that
Makarius will excuse me for this. But this history can interest everyone
who has problem with the use of latex.
Thank you really much, Makarius, for attracting my attention on the
package comment.sty and for your patience.
Actually I have many files comment.sty. One was in a directory
referenced by the bash variable TEXINPUTS. As soon as I have suppressed
this comment.sty, my problem was solved.
Sincerely yours
Last updated: Apr 20 2024 at 08:16 UTC