Vscode Translations file

Stream: general

[Edward Ayers]

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]

It would be nice if \C was ℂ

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

I agree that all greek should be one or two letters

[Mario Carneiro]

\e should be epsilon not equal

[Mario Carneiro]

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

[Mario Carneiro]

\p could be pi instead of that arrow

[Edward Ayers]

I use \l a lot in do notation.

[Chris Hughes]

I think people in general use lambda more than <-

[Reid Barton]

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

[Reid Barton]

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]

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]

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

[Mario Carneiro]

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

[Edward Ayers]

\c is currently ⌜ which is a little useless.

[Edward Ayers]

Also maybe \ss for ⊆ instead of ß

[Mario Carneiro]

\c could be chi

[Edward Ayers]

\i for ⁻¹ instead of ∩?

[Mario Carneiro]

\n should be ¬ not ∋

[Mario Carneiro]

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

[Edward Ayers]

\v doesn't have a translation.

[Mario Carneiro]

down arrow? Then \d can be delta

[Mario Carneiro]

I guess down arrow doesn't really matter

[Edward Ayers]

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

[Mario Carneiro]

\v = nu?

[Mario Carneiro]

kind of abusive but \n is taken

[Edward Ayers]

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

[Edward Ayers]

Was thinking \v could be \or

[Mario Carneiro]

aha

[Mario Carneiro]

\D and \G are greek capitals?

[Mario Carneiro]

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

[Mario Carneiro]

\L = Lambda

[Edward Ayers]

overwriting "Ł" with "Λ"

[Mario Carneiro]

I certainly use big lambda more than polish L in maths

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Kenny Lau]

well \; is space :p

[Johan Commelin]

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]

Patrick just vetoed space. , needs to remain ,

[Johan Commelin]

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

[matt rice]

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]

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]

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

[Johannes Hölzl]

nice

[Johan Commelin]

Awesome!

[Edward Ayers]

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]

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

[Rob Lewis]

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

[Patrick Massot]

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]

\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]

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]

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

[Mario Carneiro]

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

[Patrick Massot]

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

[Gabriel Ebner]

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]

I still type \lam :shrug:

[Sebastian Ullrich]

But I'm definitely open to unifying this

[Johan Commelin]

@Edward Ayers Have your changes already been merged?

[Johan Commelin]

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

[Johan Commelin]

The old symbol is ⇒

[Bryan Gin-ge Chen]

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

[Johan Commelin]

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

[Johan Commelin]

So now we have to create a new one.

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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]

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]

Exactly. Sorry if I was confusing.

[Johan Commelin]

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

[Johan Commelin]

I made a PR with this change. @Gabriel Ebner

[Gabriel Ebner]

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

[Johan Commelin]

Yes, that is probably a good idea.

[Johan Commelin]

How far are we from that moment?

[Bryan Gin-ge Chen]

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]

We could switch to nightlies earlier, I guess.

[Edward Ayers]

I think so