leanchecker should print french quotes

[fpvandoorn]

... if a component of a name contains a period. See isabelle-prover/proving-contest-backends#27

[fpvandoorn]

Ideally the code snippet in isabelle-prover/proving-contest-backends#27 (comment) should result in

«quot.sound» : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → «quot.mk» r a = «quot.mk» r b

with French quotes both around the name and around the type.

Note that #print and #print axioms in Lean put french quotes around ambiguous names in the type, but not around the name of the declaration you're printing. That could be improved, too.

[kappelmann]

Having no clue about any of the Lean cpp infrastructure, is this something that should be fixed globally in declaration.cpp or locally in checker.cpp?

[Kha]

Locally in pp_name -- compare with https://github.com/leanprover/lean/blob/master/src/util/name.cpp#L58

[kappelmann]

@gebner Thanks for dealing with this. I just wanted to adapt our proving contest backend and think that there is still some issue.
The program

axiom «quot.sound : a» : false
theorem my_proof : false := «quot.sound : a»

and

axiom «quot.sound» : false
theorem my_proof : false := «quot.sound»

return the same warning, i.e. "WARNING: Unknown axiom '«quot.sound»' used to prove theorem....
Seems like : <string> will be chopped off from quoted names?

[gebner]

Seems like : <string> will be chopped off from quoted names?

This is a bug in the text export parser of leanchecker.