Discussion: Annals of Formalized Mathematics

Stream: general

[Floris van Doorn]

Very nice to see the first issue!

[Floris van Doorn]

Tiny comment: there seems to be an issue with Joel's affiliation
image.png

[Riccardo Brasca]

I would like to thank the editors for the amazing work! Something particularly painful in writing a paper in formalized math is how to cite/write code in LaTeX. Having a specialized journal seems a good opportunity to fix a standard way of using LaTeX for Lean!

[Johan Commelin]

Link to first issue: https://afm.episciences.org/volume/view/id/1046

[Rob Lewis]

Floris van Doorn said:

Tiny comment: there seems to be an issue with Joel's affiliation
image.png

Oops, thanks for catching this. I think the Episciences platform pulls this metadata straight from HAL/arxiv and it must have gotten confused. We'll sort this out!

[Rob Lewis]

Riccardo Brasca said:

I would like to thank the editors for the amazing work! Something particularly painful in writing a paper in formalized math is how to cite/write code in LaTeX. Having a specialized journal seems a good opportunity to fix a standard way of using LaTeX for Lean!

I fully agree, and after various typesetting nightmares with this first issue, I'm terrified to take this on :scared:

[Riccardo Brasca]

It should be a community effort. Of course you have the last word for everything related to the journal, but for example solving the horrible issue with our paper is probably useful to everybody.

[Riccardo Brasca]

I am on mobile now, but if some latex guru wants to try I can describe it tomorrow.

[Sébastien Gouëzel]

Yes, please describe it, I am curious enough to have a look.

[Martin Dvořák]

BTW, if I want to upload a minor revision, can I do it directly on the Episciences webpage, or do I have to upload it to arXiv (assuming the first version was done via arXiv) first, and then link it to the revision request?

[Rémy Degenne]

Great first issue!
The instructions for authors state that there will be an "AFM LaTeX class (coming soon)". Any idea of when that file will be available?

[Riccardo Brasca]

So, unfortunately it is a nightmare to minimize, but here is the source code of our paper (the idea was to upload the source to HAL but their LaTeX didn't work). If I try pdflatex main.tex I get the error

! Argument of � has an extra }.
<inserted text>
                \par
l.351
          [IsSplittingField K L (X ^ (p : ℕ) - C (u : K))] : IsUnramified ...

Now, adding newpage on line 349, before the lstlisting that gives the error allows compilation to move on. The new error is

! Argument of � has an extra }.
<inserted text>
                \par
l.401
          (hKL' : finrank K L ≠ 2) :

So we put a \newpage also on line 397 and the file works. Now, the crazy part is that is I remove the first \newpage I get a new error

Runaway argument?
{\contentsline {section}{\numberline {6}Hilbert's Theorem 94}{117}{se\ETC.
! File ended while scanning use of \@writefile.
<inserted text>
                \par
l.70 \begin{document}

But if I then recompile everything is OK.

[Riccardo Brasca]

The errors are totally OS dependent and also depend on the LaTeX version you have, so they're very difficult to replicate.

[Riccardo Brasca]

If I understand correctly, the error Argument of � has an extra is related to lstlisting at the end of the page that LaTeX doesn't know how to break (or something like that), so newpage allows to move on. The fact that sometimes you can remove the new page is, I think because after the first compilation the citations work, and move slightly all the text, so the newpage is not needed anymore.

[Eric Wieser]

Riccardo Brasca said:

If I try pdflatex main.tex

I claim that pdflatex and its lack of unicode support is the source of all the evil here

[Riccardo Brasca]

Well, it may be. But on overleaf everything works out of the box, and it uses pdflatex

[Riccardo Brasca]

but on a newer LaTeX than what I have

[Riccardo Brasca]

I mean, it works without the newpage, so it is very possible that if you try on your computer it just works.

[Sébastien Gouëzel]

Here is a fix that works on my computer: in the lstlean.sty file, replace extendedchars=false with extendedchars=true. Does it work for you?

Also, there are several differences between the files lstlean.tex and lstlean.sty. Do you know why we have these two files, and which one should be the reference one?

[Gavin Zhao]

maybe this would be a good opportunity to start accepting Typst submissions :P

[Weiyi Wang]

:blown: TIL the junk value of Riemann zeta function

[Riccardo Brasca]

Sébastien Gouëzel said:

Here is a fix that works on my computer: in the lstlean.sty file, replace extendedchars=false with extendedchars=true. Does it work for you?

Also, there are several differences between the files lstlean.tex and lstlean.sty. Do you know why we have these two files, and which one should be the reference one?

It does, fantastic!

IIRC lstlean.sty was given to me by @Rob Lewis for the journal, I don't know the technical details.

[Filippo A. E. Nuccio]

Rémy Degenne said:

Great first issue!
The instructions for authors state that there will be an "AFM LaTeX class (coming soon)". Any idea of when that file will be available?

We already have one, but it is in a non-finalized state (as the discussion shows), so we prefer to wait before publishing it on the website. If you want a copy, don't hesitate to DM me and/or @Rob Lewis .

[Filippo A. E. Nuccio]

Floris van Doorn said:

Tiny comment: there seems to be an issue with Joel's affiliation
image.png

Fixed

[Filippo A. E. Nuccio]

Martin Dvořák said:

BTW, if I want to upload a minor revision, can I do it directly on the Episciences webpage, or do I have to upload it to arXiv (assuming the first version was done via arXiv) first, and then link it to the revision request?

First upload on arXiv, and then link the revision request.

[Rob Lewis]

Sébastien Gouëzel said:

Here is a fix that works on my computer: in the lstlean.sty file, replace extendedchars=false with extendedchars=true. Does it work for you?

Amazing, thanks!!

[Rob Lewis]

Sébastien Gouëzel said:

Also, there are several differences between the files lstlean.tex and lstlean.sty. Do you know why we have these two files, and which one should be the reference one?

There are probably hundreds of versions of this file floating around by now. Episciences had hired a TeX developer to do a bit of work on the AFM class, and I think the developer took some mix of the official listings file and mine and changed the extension to .sty. Couldn't tell you why. After dealing with this first AFM issue, I'm losing any hope of having an in-house custom listings file.

[Rob Lewis]

For the AFM specifically, we need a way to format code that's consistent over lots of authors' tex installations and arxiv and HAL.

[Rob Lewis]

arxiv especially resists any new-fangled technology, and we couldn't manage to duplicate the behavior of HAL's installation when we were trying to debug Riccardo's paper.

[Sébastien Gouëzel]

I think it's fine to just ship the lstlean.sty with the class (the lstlean.tex is unused). There is something missing in the class, though, which is why Riccardo needs to add the lines

\def\lstlanguagefiles{lstlean.sty}
\lstset{language=lean}

in his preamble: In the class file, the lines

\ifdefined\options@lean
\lstnewenvironment{lean}{\lstset{language=lean}}{} %%%Attention basicstyle=\ttfamily
\def\leaninline{\lstinline[language=lean, basicstyle=\lst@ifdisplaystyle\scriptsize\fi]}

should be replaced with

\ifdefined\options@lean
\AtBeginDocument{\lstset{language=lean}}
\lstnewenvironment{lean}{\lstset{language=lean}}{} %%%Attention basicstyle=\ttfamily
\def\leaninline{\lstinline[language=lean, basicstyle=\lst@ifdisplaystyle\scriptsize\fi]}

to make sure that the language is set to Lean. (It's not clear to me why the \AtBeginDocument is needed here, but it's needed -- probably some loading order issue). (I would also add the AtBeginDocument for rocq, by the way, because it seems to be missing there also).

I have a long train trip tomorrow, and I need something to do there. If you want, I can have a look to try to craft a version of the class which works out of the box for all the papers in the first issue -- I would just need the source of the papers for that. Unless someone at Episciences is currently working on it, in which case it's probably not a good idea to step on their toes.

[Filippo A. E. Nuccio]

Thanks! I propose we continue the discussion in DM

[Eric Wieser]

Rob Lewis said:

arxiv especially resists any new-fangled technology,

I've heard that you can email them a polite version of "your tech stack sucks just accept my modern XeTeX/LuaLaTeX PDF", and maybe enough such emails would steer them towards upgrading their system...

[Alex Kontorovich]

Just yesterday, I needed to typeset something with Lean, and (thanks to Claude) all I had to do was add these marcos to my TeX file:

\usepackage{listings}
\usepackage{xcolor}

\lstdefinelanguage{lean4}{
keywords={theorem, lemma, def, example, axiom, inductive, structure,
         class, instance, namespace, section, variable, universe,
         import, export, open, private, protected, partial, mutual,
         if, then, else, match, with, fun, let, in, by, have, show,
         sorry, admit, Prop},
         sensitive=true,
  comment=[l]{--},
  morecomment=[s]{/-}{-/},
  string=[b]",
  keywordstyle=\color{blue}\bfseries,
  commentstyle=\color{green!60!black},
  stringstyle=\color{red}
}

\lstset{language=lean4}

\usepackage{listings}
\usepackage[utf8]{inputenc}
\lstset{
backgroundcolor=\color{yellow!10},
  inputencoding=utf8,
  extendedchars=true,
  literate=
    {ℕ}{{$\mathbb{N}$}}1
    {ℤ}{{$\mathbb{Z}$}}1
    {ℝ}{{$\mathbb{R}$}}1
    {λ}{{$\lambda$}}1
    {α}{{$\alpha$}}1
    {β}{{$\beta$}}1
    {γ}{{$\gamma$}}1
    {≤}{{$\leq$}}1
    {≥}{{$\geq$}}1
    {≠}{{$\neq$}}1
    {∧}{{$\land$}}1
    {∨}{{$\lor$}}1
    {¬}{{$\lnot$}}1
{⊢}{{{\color{orange!70!red}$\boldsymbol{\vdash}$}}}1
{∃}{{{\color{orange!70!red}$\boldsymbol{\exists}$}}}1
{∀}{{{\color{orange!70!red}$\boldsymbol{\forall}$}}}1
{→}{{{\color{orange!70!red}$\boldsymbol{\to}$}}}1
{↔}{{{\color{orange!70!red}$\boldsymbol{\leftrightarrow}$}}}1
}

Then in the body, I used it like this:

Suppose that your current goal state looks like this:
\begin{lstlisting}
DeanDziuba : Person
PlaysSoccer : Person → Prop
⊢ ∃ (somebody : Person), PlaysSoccer somebody
\end{lstlisting}
and you give the command
\begin{lstlisting}
use DeanDziuba
\end{lstlisting}
Then what will the new goal be?
\begin{lstlisting}
⊢ ???
\end{lstlisting}

(This was a quiz, on paper, for high school kids learning Lean + Euclidean Geometry...)

[Jireh Loreaux]

Eric Wieser said:

Rob Lewis said:

arxiv especially resists any new-fangled technology,

I've heard that you can email them a polite version of "your tech stack sucks just accept my modern XeTeX/LuaLaTeX PDF", and maybe enough such emails would steer them towards upgrading their system...

I can verify that the arXiv moderators can provide waivers to the requirement that you provide the TeX source for pdfs generated by XeTeX/LuaLaTeX. You need to provide them with some sort of reason though (e.g., using minted and unicode).

[Yaël Dillies]

Looking at the PDFs online, the title of the PDF in https://afm.episciences.org/15978/pdf is "pdf", while the title of https://afm.episciences.org/15945/pdf is "Derandomization with pseudorandomness", as expected

[Yaël Dillies]

Spotted thanks to image.png