LaTeX: avoiding type 3 fonts

Stream: general

[Siddhartha Gadgil]

We are using lstlisting to include Lean code in LaTeX. Unfortunately this seems to generate Type 3 fonts, and CPP does not allow these. Does anyone know a solution (I assume others have bumped into this issue)?

[Kevin Buzzard]

Use minted?

[Siddhartha Gadgil]

Kevin Buzzard said:

Use minted?

Thanks. Let me try this.

[Utensil Song]

For minted, check here for a still working Lean 3 syntax highlight. For Lean 4, the current solution on the community page has some issues discussed in the thread, hope you have better luck with it.

[Siddhartha Gadgil]

In case someone runs into the same problem, it turns out that code in backticks in comments inside lstlisting blocks was generating the type 3 fonts (we had a long journey of overcorrecting before narrowing to this and restoring).