search

coq-community / hydra-battles

Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
https://coq-community.org/hydra-battles/doc/hydras.pdf
MIT License
64 stars 12 forks source link

Snippets with utf8 characters #113

Open Casteran opened 2 years ago

Casteran commented 2 years ago

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 commented 2 years ago

Cc @cpitclaudel

cpitclaudel commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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

cpitclaudel commented 2 years ago

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 commented 2 years ago

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

Casteran commented 2 years ago

@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 commented 2 years ago

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

Zimmi48 commented 2 years ago

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

https://github.com/coq-community/hydra-battles/blob/8b50732058d291b03cada050d1e41a6a6061712a/.nix/coq-overlays/hydra-battles-single/default.nix#L15-L42

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 commented 2 years ago

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 commented 2 years ago

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.