The book's prose is in Portuguese, but several reader-facing labels that
CSwLMeta generates around that prose are still in English, inherited
verbatim from sf-in-lean. They are not Lean identifiers and not code
comments — CLAUDE.md's English rule covers those — they are book text that
happens to be rendered as -- comments or as HTML chrome. Today they are
localized inconsistently.
In the generated .lean (CSwLMeta/Save/Extract.lean), every label is in
English:
### Exercise (3 stars): frm-eval ⭐⭐⭐ — Block.exercise_Quiz:_ — Block.quizTHE FOLLOWING DETAILS CAN BE SKIPPED (…) / END DETAILS —
Block.details
In the HTML, the same material is localized, but only partly:
Exercício — CSwLMeta/Exercise.lean, in both toHtml and toTeXNota editorial — CSwLMeta/Comment.lean- but the exercise designation stays English on both sides, since
exerciseDesignation is shared: (Advanced, manually graded), and the
TeX output reads Exercício (3 stars).
This matters most for the terse variant, which is the .lean opened in
VS Code during class — the student sees THE FOLLOWING DETAILS CAN BE SKIPPED above a paragraph in Portuguese.
The details markers were added in the port of SFLMeta/Details.lean and
were deliberately left in English, to match their neighbours rather than
localize one of three in isolation.
To settle: whether these labels are localized at all (the alternative is to
declare all generated labels English on purpose, and make the HTML side
match, which would mean reverting Exercício and Nota editorial); and, if
they are, whether exerciseDesignation is split so the HTML/TeX and the
saver can differ, or whether the whole set moves to Portuguese at once.
Whatever is decided belongs in STYLE-CODE.md next to the directive
vocabulary, so the next ported directive does not have to guess.
The book's prose is in Portuguese, but several reader-facing labels that
CSwLMetagenerates around that prose are still in English, inheritedverbatim from
sf-in-lean. They are not Lean identifiers and not codecomments —
CLAUDE.md's English rule covers those — they are book text thathappens to be rendered as
--comments or as HTML chrome. Today they arelocalized inconsistently.
In the generated
.lean(CSwLMeta/Save/Extract.lean), every label is inEnglish:
### Exercise (3 stars): frm-eval ⭐⭐⭐—Block.exercise_Quiz:_—Block.quizTHE FOLLOWING DETAILS CAN BE SKIPPED (…)/END DETAILS—Block.detailsIn the HTML, the same material is localized, but only partly:
Exercício—CSwLMeta/Exercise.lean, in bothtoHtmlandtoTeXNota editorial—CSwLMeta/Comment.leanexerciseDesignationis shared:(Advanced, manually graded), and theTeX output reads
Exercício (3 stars).This matters most for the
tersevariant, which is the.leanopened inVS Code during class — the student sees
THE FOLLOWING DETAILS CAN BE SKIPPEDabove a paragraph in Portuguese.The
detailsmarkers were added in the port ofSFLMeta/Details.leanandwere deliberately left in English, to match their neighbours rather than
localize one of three in isolation.
To settle: whether these labels are localized at all (the alternative is to
declare all generated labels English on purpose, and make the HTML side
match, which would mean reverting
ExercícioandNota editorial); and, ifthey are, whether
exerciseDesignationis split so the HTML/TeX and thesaver can differ, or whether the whole set moves to Portuguese at once.
Whatever is decided belongs in
STYLE-CODE.mdnext to the directivevocabulary, so the next ported directive does not have to guess.