Pierre Castéran

Anyway, It may be interesting to document both definitions and chose one (for instance the unbundled one), using the module system to mask the other. > Le 31 août 2021...

When we add more stuff in hydra-gaia, it will be interesting to comment and compare both styles, and choose a style for writing bridge lemmas and their proofs.

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 ₁...

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

@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,...

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

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) ?

Looks to be an issue specific to Latex output generation. The `html` file generated by the same snippet is OK w.r.t. the display of local definitions `x:= A: t`, whilst...

Cc: @cpitclaudel Here is a simpler example: ``` (* begin snippet LProof *) Lemma L: exists z: bool, negb z = true. Proof. pose (z := false). exists z. (*...

This issue seems to be solved if one replaces in `latex.py` the method `gen_hyp` with ``` def gen_hyp(self, hyp): names = self.gen_names(hyp.names) hbody = [self.gen_code(hyp.body)] if hyp.body else [] with...