weird LaTeX bug: fullpage + hyperref + listings on NixOS

Stream: general

[Johan Commelin]

Does the following LaTeX produce an error on your machine?

\documentclass{article}
\usepackage{lipsum}

\usepackage{amsmath,amssymb}
\usepackage{xcolor}

\definecolor{keywordcolor}{rgb}{0.7, 0.1, 0.1}   % red
\definecolor{tacticcolor}{rgb}{0.0, 0.1, 0.3}    % dark blue
\definecolor{commentcolor}{rgb}{0.4, 0.4, 0.4}   % grey
\definecolor{stringcolor}{rgb}{0.5, 0.3, 0.2}    % brown
\definecolor{symbolcolor}{rgb}{0.1, 0.2, 0.7}    % blue
\definecolor{sortcolor}{rgb}{0.1, 0.5, 0.1}      % green
\definecolor{attributecolor}{rgb}{0.7, 0.1, 0.1} % red
\definecolor{errorcolor}{rgb}{1, 0, 0}           % bright red

\usepackage{listings}
\def\lstlanguagefiles{lstlean.tex}
\lstloadlanguages{lean}
\lstset{language=lean}
\usepackage{scalefnt}




% When commenting out `fullpage', also change the filler text below.
\usepackage{fullpage}
\usepackage[unicode,colorlinks=true,linkcolor=blue,urlcolor=magenta, citecolor=blue]{hyperref}


\begin{document}

% Use the following filler text for testing without `\usepackage{fullpage}'

% \lipsum[1-4]
% \lipsum[2]
%
% Now we just need a tiny bit more filler text.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Use the following filler text for testing with `\usepackage{fullpage}'

\lipsum[1-7]

Now we just need a tiny bit more filler text.

Now we just need a tiny bit more filler text.

Now we just need a tiny bit more filler text.

Now we just need a tiny bit more filler text.

\begin{lstlisting}
  inductive Nat
  | zero : Nat
  | succ : Nat -> Nat
\end{lstlisting}

\end{document}

[Johan Commelin]

Without the fullpage + hyperref combo, I do not get an error. And the error occurs when there is a code block in a pagebreak.

[Johan Commelin]

Patrick Massot didn't have problems with this code. So it seems to depend on the precise versions of the packages involved.

[Johan Commelin]

• listings 2020/03/24 1.8d
• fullpage 1999/02/23 1.1
• hyperref 2023-02-07 v7.00v

[Yaël Dillies]

I get

Package Listings: Couldn't load requested language.

[Christian Merten]

Both with and without fullpage compile fine for me.

[Mauricio Collares]

Yaël Dillies said:

I get

Package Listings: Couldn't load requested language.

You need to save https://raw.githubusercontent.com/leanprover/lean4/master/doc/latex/lstlean.tex in the same directory as the above TeX file.

[Mauricio Collares]

I get

! Argument of � has an extra }.
<inserted text>
                \par
l.56
       | succ : Nat -> Nat

both with and without the fullpage package (with the appropriate fillers) when compiling with pdflatex. xelatex works fine in both cases.

[Kevin Buzzard]

Is there a reason you're not using minted instead?

[Eric Wieser]

The latest minted is a pain to use with Lean 4 until lean4#3125 can be merged (which is waiting on an upstream release)

[Shreyas Srinivas]

Can minted be used in overleaf?

[Eric Wieser]

(old versions of minted are ok)

[Eric Wieser]

Yes, it works fine in overleaf

[Eric Wieser]

Overleaf makes it easy to use old minted too (use TeXLive 2022 or maybe it was 2021)

[Mauricio Collares]

Just upgraded to TeXLive 2023.20240114 on NixOS, and I still see the same problem. Package versions:

listings 1.9 (2023/02/27)
fullpage 1.1 (1999/02/23)
hyperref v7.01g (2023-11-26)