## Stream: general

### Topic: Vscode Translations file

#### Edward Ayers (Jan 10 2019 at 14:46):

Dear all I am cleaning up the vscode translations file. I've removed all of the accents which are rejected by Lean. Are there any shortcuts that people find they mistype frequently or which stop a useful character from being corrected?
Eg I often write "\de" and have it corrected to "\dei" = "ϯ" instead of "\delta". Would people also be interested in having two letter shortcuts for all of the lower case greek letters? Ie "\ta" corrects to tau and so on.

#### Chris Hughes (Jan 10 2019 at 15:10):

It would be nice if \C was ℂ

#### Mario Carneiro (Jan 10 2019 at 20:35):

lambda should have a one letter command (other than G which makes no sense), any suggestions?

#### Mario Carneiro (Jan 10 2019 at 20:36):

maybe \l for lambda and \<- for left arrow

#### Mario Carneiro (Jan 10 2019 at 20:37):

I agree that all greek should be one or two letters

#### Mario Carneiro (Jan 10 2019 at 20:38):

\e should be epsilon not equal

#### Mario Carneiro (Jan 10 2019 at 20:39):

\q is theta in mathematica, and a black box in lean (not so useful)

#### Mario Carneiro (Jan 10 2019 at 20:40):

\p could be pi instead of that arrow

#### Edward Ayers (Jan 10 2019 at 21:13):

I use \l a lot in do notation.

#### Chris Hughes (Jan 10 2019 at 21:14):

I think people in general use lambda more than <-

#### Reid Barton (Jan 10 2019 at 21:20):

there's also rw \l which might be more common than lambda depending on style

#### Reid Barton (Jan 10 2019 at 21:22):

Another consideration though is ending the abbreviation. I'm not sure whether VSCode works the same way but if I want to rewrite with the reverse of a hypothesis with name that happens to start with e, I would like to type rw \le..., but that gets processed as the less-than-or-equal operator

#### Reid Barton (Jan 10 2019 at 21:23):

usually I put a space after a lambda but not necessarily after a <-, so switching them would be an improvement in that case

#### Mario Carneiro (Jan 10 2019 at 21:40):

mathlib style puts a space between <- and the lemma anyway

#### Mario Carneiro (Jan 10 2019 at 21:41):

if left arrow is so important, any votes for \- for left arrow? Currently it looks like it makes a nbsp

#### Edward Ayers (Jan 10 2019 at 21:52):

\c is currently ⌜ which is a little useless.

#### Edward Ayers (Jan 10 2019 at 21:54):

Also maybe \ss for ⊆ instead of ß

#### Mario Carneiro (Jan 10 2019 at 22:01):

\c could be chi

#### Edward Ayers (Jan 10 2019 at 22:03):

\i for ⁻¹ instead of ∩?

#### Mario Carneiro (Jan 10 2019 at 22:05):

\n should be ¬  not ∋

#### Mario Carneiro (Jan 10 2019 at 22:06):

\/ could be \or, is that too tricky?

#### Edward Ayers (Jan 10 2019 at 22:07):

\v doesn't have a translation.

#### Mario Carneiro (Jan 10 2019 at 22:07):

down arrow? Then \d can be delta

#### Mario Carneiro (Jan 10 2019 at 22:07):

I guess down arrow doesn't really matter

#### Edward Ayers (Jan 10 2019 at 22:08):

I don't want to change too many of the ones that are in use but already assigned.

\v = nu?

#### Mario Carneiro (Jan 10 2019 at 22:09):

kind of abusive but \n is taken

#### Edward Ayers (Jan 10 2019 at 22:09):

I've added 2 letter translations for each of the greek letters

#### Edward Ayers (Jan 10 2019 at 22:09):

Was thinking \v could be \or

aha

#### Mario Carneiro (Jan 10 2019 at 22:10):

\D and \G are greek capitals?

#### Mario Carneiro (Jan 10 2019 at 22:11):

The current \GD and \Gd etc is annoying to type

\L = Lambda

#### Edward Ayers (Jan 10 2019 at 22:13):

overwriting "Ł" with "Λ"

#### Mario Carneiro (Jan 10 2019 at 22:14):

I certainly use big lambda more than polish L in maths

#### Mario Carneiro (Jan 10 2019 at 22:15):

I see that's the only abbrev for polish L, maybe it can relocate to \L/

#### Mario Carneiro (Jan 10 2019 at 22:17):

\m = mu, I don't know what that m-eq thing is

#### Johan Commelin (Jan 11 2019 at 07:16):

Can we have \  = lambda? Or is \-space impossible to assign in VScode? (It is even sort of mnemonic...)

#### Kenny Lau (Jan 11 2019 at 07:48):

well \; is space :p

#### Johan Commelin (Jan 11 2019 at 07:50):

I would expect that to be unicode THIN SPACE, if that exists (-; Which I think it does. But that is just my LaTeX intuition ported to VScode. And that port might not be lawful

#### Gabriel Ebner (Jan 11 2019 at 08:06):

Patrick just vetoed space. ,  needs to remain ,

#### Johan Commelin (Jan 11 2019 at 08:06):

Fair enough... but just like others need to fix their OS, he ought to fix his keyboard layout :stuck_out_tongue_wink:

#### matt rice (Jan 12 2019 at 22:19):

One thing i found accidentally, was \<> will do the same as: \< \>, but that neither \f<> nor \f<f> will do the same as \f< \f>, I looked a bit through the translations but didn't find where the \<> magic was coming from

#### Johan Commelin (Jan 14 2019 at 10:41):

I don't know if this belongs in the translations file... but I wouldn't mind if I could type \copyright and this would expand to the header that goes to the top of every Lean file. (If possible with the correct year filled in.)
Of course I can just copy it from another file... but this would be a nice little feature.
Priority: very low

#### Gabriel Ebner (Jan 14 2019 at 10:51):

@Johan Commelin Something like this? https://github.com/leanprover/mathlib/pull/589

nice

Awesome!

#### Edward Ayers (Jan 14 2019 at 12:58):

Summary of my proposed changes:
- \L is Λ instead of Ł
- \G is Γ
- \pis Π
- \C is ℂ instead of ∁
- \c is χ
- \v is ∨
- \- is ⁻¹ instead of a space.
- \n is ¬
- \ss is ⊆
- \m is μ
All greek letters have a 2-space shortcut. Eg sigma is \si, omega is \om etc.

All accented characters have been removed except

À Á Â Ã Ä Å Æ Ç È É Ê Ë Ì Í Î Ï
Ð Ñ Ò Ó Ô Õ Ö    Ø Ù Ú Û Ü Ý Þ
à á â ã ä å æ ç è é ê ë ì í î ï
ð ñ ò ó ô õ ö   ø ù ú û ü ý þ ÿ
Ł


(so we can still use important keywords like "Hölzl")

#### Patrick Massot (Jan 14 2019 at 15:03):

Did we decide something for \l giving lambda or left arrow?

#### Rob Lewis (Jan 14 2019 at 15:06):

I'd prefer not to change it from left arrow, since presumably anyone who writes tactics uses it a lot.

#### Patrick Massot (Jan 14 2019 at 15:07):

everybody use left arrow a lot, it's also used in rewrite. If we change we also need a nice shortcut for left arrow

#### Edward Ayers (Jan 14 2019 at 15:13):

\lfor lambda is contentious so I just kept it as is. In this PR I don't want to change the translations file in such a way that could potentially make things worse for some users.

#### Thales (Jan 14 2019 at 23:51):

Some unsupported notations I have considered using in the future are
ˇ caron, ␣ vispace, ˅ down , ˄ up, ⅅ Dd, ⅆ dd, ⅇ ee, ⅈ ii, ⅉ jj.
The intended use is that ⅈ designates the complex number i, ⅇ designates the
base of the natural log, ⅆ is the binder for integration, etc.

I have experimented with using accents as operators. For example, the U+0304 bar accent is particularly useful.

Will Lean-emacs remain compatible with VSCode for those of us that switch back and forth?

#### Mario Carneiro (Jan 15 2019 at 00:31):

The emacs and VSCode lean modes use the same translations file, so any change to translations.json should affect both

#### Mario Carneiro (Jan 15 2019 at 00:32):

I'm not sure if the cocalc version uses the same file

#### Patrick Massot (Jan 15 2019 at 07:58):

We should also make sure to PR modifications to TPIL and the reference manual (and mathlib doc)

#### Gabriel Ebner (Jan 15 2019 at 08:33):

The emacs and VSCode lean modes use the same translations file, so any change to translations.json should affect both

Unfortunately this is not at all the case. The vscode extension, the emacs mode, cocalc, the javascript version, they all use their own copy of the translations. The translations.json file was originally exported from the emacs mode two years ago. To my knowledge, none of the improvements in the vscode extension have been propagated to the other editor plugins.

#### Sebastian Ullrich (Jan 15 2019 at 08:34):

I still type \lam :shrug:

#### Sebastian Ullrich (Jan 15 2019 at 08:34):

But I'm definitely open to unifying this

#### Johan Commelin (Jan 17 2019 at 17:49):

If not, could you change the translation of \functor (and prefixes of that) back to the old symbol?

#### Johan Commelin (Jan 17 2019 at 17:49):

The old symbol is ⇒

#### Bryan Gin-ge Chen (Jan 17 2019 at 17:50):

His changes have already been merged in #107, but your suggestion wouldn't be hard to implement.

#### Johan Commelin (Jan 17 2019 at 17:50):

Sure, I just wasn't aware what the status was. Otherwise it could go into that PR.

#### Johan Commelin (Jan 17 2019 at 17:50):

So now we have to create a new one.

#### Bryan Gin-ge Chen (Jan 17 2019 at 17:52):

I'm not seeing anything related to \functor changed in the diff though?

#### Bryan Gin-ge Chen (Jan 17 2019 at 17:53):

Here's the diff. In the current version of the extension, if I complete \functor I get ⥤. If I search the diff for that symbol, I see it both in the old version and the new version.

#### Bryan Gin-ge Chen (Jan 17 2019 at 17:54):

The symbol you pasted above as the "old symbol" ⇒ is currently \Longrightarrow.

I guess this also used to be under \functor but that was changed by your commit in August.

OK, so I think I finally understand. You want to revert that change from August, not anything done by Ed.

#### Johan Commelin (Jan 17 2019 at 18:08):

Exactly. Sorry if I was confusing.

#### Johan Commelin (Jan 17 2019 at 18:08):

Because that symbol was locked into core, but was recently liberated.

#### Johan Commelin (Jan 17 2019 at 18:17):

I made a PR with this change. @Gabriel Ebner

#### Gabriel Ebner (Jan 17 2019 at 18:26):

Should we maybe wait until mathlib works with that Lean version?

#### Johan Commelin (Jan 17 2019 at 18:28):

Yes, that is probably a good idea.

#### Johan Commelin (Jan 17 2019 at 18:29):

How far are we from that moment?

#### Bryan Gin-ge Chen (Jan 17 2019 at 18:30):

As far as I can tell we're just waiting on 3.4.2 to be officially released. Then I'll PR the 3.4.2 branch in community mathlib which currently works with nightly.

#### Gabriel Ebner (Jan 17 2019 at 18:30):

We could switch to nightlies earlier, I guess.

#### Edward Ayers (Jan 17 2019 at 18:49):

I think so

Last updated: May 14 2021 at 21:11 UTC