lean Unicode shortcuts in Android's gboard

Stream: lean4

[Joachim Breitner]

It seems that Android'a default keyboard allows abbreviations to be configured: https://github.com/DenverCoder1/latex-gboard-dictionary?tab=readme-ov-file can be used to get common latex abbreviations.

Has someone tried to put lean's abbreviations into this format and use it? Might be handy

[Damiano Testa]

Back in the lean3 days, Eric posted some instructions to get something similar. I have it working on my phone, but let me try to find the instructions!

[Damiano Testa]

#general > Unicode input on android

[Eric Wieser]

I've also toyed with the idea of making a custom gboard layout for Lean, since I have access to its source...

[Yaël Dillies]

Please please please :folded_hands: In return I will review all your future PRs in under a day

[Joachim Breitner]

Is that offer also valid for having \a abbreviations in gboard, without changing the layout? Because then I’ll quickly whip out sed before someone else takes up that very attractive offer :)

[Eric Wieser]

Joachim Breitner said:

Is that offer also valid for having \a abbreviations in gboard, without changing the layout? Because then I’ll quickly whip out sed before someone else takes up that very attractive offer :)

I think that's already covered by Damiano's link above?

[Joachim Breitner]

Indeed, that’s true. I was first confused because that link suggests installing an extra app, but that look optional.

[Damiano Testa]

α

[Damiano Testa]

The previous message was typed on my phone, using \a.

[Eric Wieser]

Joachim Breitner said:

Indeed, that’s true. I was first confused because that link suggests installing an extra app, but that look optional.

Whats the mechanism for installating shortcuts from a file without that extra app?

[Joachim Breitner]

Run the code , generate the zip, copy it to your mobile and import from Gboard settings>Dictionary>Personal Dictionary>All Languages>then choose import option from the drop-down menu

according to https://github.com/realKarthikNair/GBoard-Dictionary-Maker. Did not try it though. And a manager might be advisable in any case.