Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Latex problem on the AFP

view this post on Zulip Email Gateway (Aug 25 2023 at 09:29):

From: "Achim D. Brucker" <adbrucker@0x5f.org>
Hi Anders,
Only a vague idea to help you debugging the issues:

To the best of my knowledge, the current AFP build infrastructure uses
TexLive 2019 on Ubuntu 20.04. This might be older than what you have
on your machine (I had some troubles with an entry currently in the
submission queue).

If you are familar with containers (e.g., docker, podman) or VMs, it
might be an idea to try to build the PDF by running latex in a TexLive 2019
container (e.g., docker HUB provides "listx/texlive:2019"). You can
use LaTeX files generated by Isabelle on your development machine.
No need to install Isabelle in a container ...

Best,
Achim

view this post on Zulip Email Gateway (Sep 01 2023 at 08:36):

From: Makarius <makarius@sketis.net>
The underscore package is rubbish.

When you have formal text inside informal text, the proper way is to use
formal markup (via suitable antiquotation). For example:

text
‹
Theorem ‹valid_in_valid› is a kind of the reverse of valid_valid_in (or its
transfer variant).
›

Here the antiquotation is called "cartouche" and its argument is a single
cartouche. Thus the rather short and concise notation with a pair of French
single quotes.

Makarius

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (Sep 01 2023 at 09:48):

From: Lawrence Paulson <lp15@cam.ac.uk>
Please don’t do this! Don’t be afraid to type \_ if you have to.

Larry

Last updated: Apr 27 2024 at 16:16 UTC