Snippets with utf8 characters

[Casteran]

On branch utf8 I added a snippet utf8tryat the end of gaia/T1Bridge.v with the utf8 character for omega. The file movies/snippets/T1Bridge.tex looks to be OK,
but in hydras.pdf all the occurrences of the greek letter are missing (page 206).

Is there a standard way to use utf8 characters all along the toolchain ?

[Zimmi48]

Cc @cpitclaudel

[cpitclaudel]

Probably a font issue? The log will say something like this:

Missing character: There is no λ (U+03BB) in font [lmmono10-regular]:!
{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}
Missing character: There is no α (U+03B1) in font [lmmono10-regular]:!
] (./test.aux))

Can you check?

[Casteran]

Yes !
Missing character: There is no ω (U+03C9) in font [lmmono10-regular]:!

I've got also some similar messages in the addition-chains chapter:
(./movies/snippets/Addition_Chains/parametricDef.tex) [249
Missing character: There is no ₁ (U+2081) in font [lmmono9-regular]:!
Missing character: There is no ₂ (U+2082) in font [lmmono9-regular]:!
Missing character: There is no ₁ (U+2081) in font [lmmono9-regular]:!
Missing character: There is no ₂ (U+2082) in font [lmmono9-regular]:!

I desperately looked for a tutorial on "how to simply select a font with enough utf8 characters (with lualatex) "

[Casteran]

@cpitclaudel
Indeed, the issue happens only inside the snippets. If I type an utf8 omega in the
main tex, it is correctly displayed.

[cpitclaudel]

If you're OK with changing the font, it could be as simple as \setmonofont{Fira Code}[Scale=MatchLowercase] after the line that loads fontspec (you can install that font from https://github.com/tonsky/FiraCode).

[cpitclaudel]

IIRC \setmonofont{Liberation Mono} would work as well.

[Casteran]

@cpitclaudel Thanks a lot !
I installed FiraCode on my machine, at least "Check ω." works!
@Zimmi48 @palmskog Do we have to install this font somewhere for the CI/CD?

Indeed, if we include snippets with Coq+utf8 in the documentation, we would also have to update the INSTALL directives in the README.

[Casteran]

\setmonofont{DejaVu Sans Mono}[Scale=MatchLowercase] looks good too.
And it doesn't cause errors on CI !

[Zimmi48]

Sorry for not responding earlier. I have done a precise listing of the LaTeX packages that are needed to compile the book in:

hydra-battles/.nix/coq-overlays/hydra-battles-single/default.nix

Lines 15 to 42 in 8b50732

	(if withTex then
	[ (texlive.combine {
	inherit (texlive)
	# With lualatex
	scheme-small
	# Extra packages
	caption
	doublestroke
	draftwatermark
	environ
	fancyvrb
	float
	fontspec
	lkproof
	mathdots
	mathtools
	mdframed
	needspace
	newunicodechar
	placeins
	synttree
	tcolorbox
	texments
	threeparttable
	tikzsymbols
	xcolor
	zref;
	}) ]

The advantage is that this represents less to download in CI, but the drawback of course is that this list needs to be kept up-to-date if we add dependencies on new LaTeX packages...

[Casteran]

Thanks @Zimmi48 !
Do we have to include this list in the installation directives for the users (as well as the specific fonts needed for compiling the utf8 snippets) ?

[Zimmi48]

Do we have to include this list in the installation directives for the users (as well as the specific fonts needed for compiling the utf8 snippets) ?

Sure, that could make sense, although lots of users will just have a "full TeXLive" distribution, which is always sufficient.