Zulip Chat Archive

Stream: general

Topic: Vscode Translations file


view this post on Zulip 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.

view this post on Zulip Chris Hughes (Jan 10 2019 at 15:10):

It would be nice if \C was ℂ

view this post on Zulip Mario Carneiro (Jan 10 2019 at 20:35):

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

view this post on Zulip Mario Carneiro (Jan 10 2019 at 20:36):

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

view this post on Zulip Mario Carneiro (Jan 10 2019 at 20:37):

I agree that all greek should be one or two letters

view this post on Zulip Mario Carneiro (Jan 10 2019 at 20:38):

\e should be epsilon not equal

view this post on Zulip Mario Carneiro (Jan 10 2019 at 20:39):

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

view this post on Zulip Mario Carneiro (Jan 10 2019 at 20:40):

\p could be pi instead of that arrow

view this post on Zulip Edward Ayers (Jan 10 2019 at 21:13):

I use \l a lot in do notation.

view this post on Zulip Chris Hughes (Jan 10 2019 at 21:14):

I think people in general use lambda more than <-

view this post on Zulip Reid Barton (Jan 10 2019 at 21:20):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 10 2019 at 21:40):

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

view this post on Zulip 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

view this post on Zulip Edward Ayers (Jan 10 2019 at 21:52):

\c is currently which is a little useless.

view this post on Zulip Edward Ayers (Jan 10 2019 at 21:54):

Also maybe \ss for instead of ß

view this post on Zulip Mario Carneiro (Jan 10 2019 at 22:01):

\c could be chi

view this post on Zulip Edward Ayers (Jan 10 2019 at 22:03):

\i for ⁻¹ instead of ?

view this post on Zulip Mario Carneiro (Jan 10 2019 at 22:05):

\n should be ¬ not

view this post on Zulip Mario Carneiro (Jan 10 2019 at 22:06):

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

view this post on Zulip Edward Ayers (Jan 10 2019 at 22:07):

\v doesn't have a translation.

view this post on Zulip Mario Carneiro (Jan 10 2019 at 22:07):

down arrow? Then \d can be delta

view this post on Zulip Mario Carneiro (Jan 10 2019 at 22:07):

I guess down arrow doesn't really matter

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jan 10 2019 at 22:08):

\v = nu?

view this post on Zulip Mario Carneiro (Jan 10 2019 at 22:09):

kind of abusive but \n is taken

view this post on Zulip Edward Ayers (Jan 10 2019 at 22:09):

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

view this post on Zulip Edward Ayers (Jan 10 2019 at 22:09):

Was thinking \v could be \or

view this post on Zulip Mario Carneiro (Jan 10 2019 at 22:09):

aha

view this post on Zulip Mario Carneiro (Jan 10 2019 at 22:10):

\D and \G are greek capitals?

view this post on Zulip Mario Carneiro (Jan 10 2019 at 22:11):

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

view this post on Zulip Mario Carneiro (Jan 10 2019 at 22:12):

\L = Lambda

view this post on Zulip Edward Ayers (Jan 10 2019 at 22:13):

overwriting "Ł" with "Λ"

view this post on Zulip Mario Carneiro (Jan 10 2019 at 22:14):

I certainly use big lambda more than polish L in maths

view this post on Zulip Mario Carneiro (Jan 10 2019 at 22:15):

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

view this post on Zulip Mario Carneiro (Jan 10 2019 at 22:17):

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

view this post on Zulip 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...)

view this post on Zulip Kenny Lau (Jan 11 2019 at 07:48):

well \; is space :p

view this post on Zulip 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

view this post on Zulip Gabriel Ebner (Jan 11 2019 at 08:06):

Patrick just vetoed space. , needs to remain ,

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Gabriel Ebner (Jan 14 2019 at 10:51):

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

view this post on Zulip Johannes Hölzl (Jan 14 2019 at 11:03):

nice

view this post on Zulip Johan Commelin (Jan 14 2019 at 11:25):

Awesome!

view this post on Zulip 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")

view this post on Zulip Patrick Massot (Jan 14 2019 at 15:03):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 15 2019 at 00:32):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Sebastian Ullrich (Jan 15 2019 at 08:34):

I still type \lam :shrug:

view this post on Zulip Sebastian Ullrich (Jan 15 2019 at 08:34):

But I'm definitely open to unifying this

view this post on Zulip Johan Commelin (Jan 17 2019 at 17:48):

@Edward Ayers Have your changes already been merged?

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jan 17 2019 at 17:49):

The old symbol is

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jan 17 2019 at 17:50):

So now we have to create a new one.

view this post on Zulip Bryan Gin-ge Chen (Jan 17 2019 at 17:52):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jan 17 2019 at 18:08):

Exactly. Sorry if I was confusing.

view this post on Zulip Johan Commelin (Jan 17 2019 at 18:08):

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

view this post on Zulip Johan Commelin (Jan 17 2019 at 18:17):

I made a PR with this change. @Gabriel Ebner

view this post on Zulip Gabriel Ebner (Jan 17 2019 at 18:26):

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

view this post on Zulip Johan Commelin (Jan 17 2019 at 18:28):

Yes, that is probably a good idea.

view this post on Zulip Johan Commelin (Jan 17 2019 at 18:29):

How far are we from that moment?

view this post on Zulip 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.

view this post on Zulip Gabriel Ebner (Jan 17 2019 at 18:30):

We could switch to nightlies earlier, I guess.

view this post on Zulip Edward Ayers (Jan 17 2019 at 18:49):

I think so


Last updated: May 14 2021 at 21:11 UTC