Zulip Chat Archive

Stream: new members

Topic: how to write a superscript quickly?


view this post on Zulip Chris M (Jun 30 2020 at 05:33):

I want to write a^{-1}. How do I do this in lean?

view this post on Zulip Shing Tak Lam (Jun 30 2020 at 05:34):

\inv

view this post on Zulip Chris M (Jun 30 2020 at 05:34):

cool

view this post on Zulip Johan Commelin (Jun 30 2020 at 05:47):

Also \-1

view this post on Zulip Scott Morrison (Jun 30 2020 at 09:09):

Also -- if you hover the mouse over any symbol in VSCode, the tooltip will tell you how to type it.

view this post on Zulip Eric Wieser (Jun 30 2020 at 09:12):

Is there a reason vscode has no methanism to type ?

view this post on Zulip Johan Commelin (Jun 30 2020 at 09:12):

Probably because nobody wrote a PR that adds it to translations.json

view this post on Zulip Eric Wieser (Jun 30 2020 at 09:13):

Mind linking to that file on github?

view this post on Zulip Shing Tak Lam (Jun 30 2020 at 09:14):

https://github.com/leanprover/vscode-lean/blob/master/translations.json (I think)

view this post on Zulip Eric Wieser (Jun 30 2020 at 09:14):

It also puzzles me that \_ produces (\_a)

view this post on Zulip Eric Wieser (Jun 30 2020 at 09:15):

Thanks @Shing Tak Lam. Looks like @Utensil Song beat me to it: https://github.com/leanprover/vscode-lean/blame/670606ba0ab2ae668b431169aa81e8f77b1c2d78/translations.json#L1284

view this post on Zulip Mario Carneiro (Jun 30 2020 at 09:19):

When you write a prefix of a valid shortcut it uses the first one that matches

view this post on Zulip Eric Wieser (Jun 30 2020 at 09:19):

Would it be reasonable to do that only if there are not multiple tied shortest ones?

view this post on Zulip Mario Carneiro (Jun 30 2020 at 09:19):

why? It's still better than nothing

view this post on Zulip Mario Carneiro (Jun 30 2020 at 09:20):

and you can train your muscle memory to it regardless of how weird it is

view this post on Zulip Eric Wieser (Jun 30 2020 at 09:21):

Until someone adds a new shortcut that happens to be the same length as an existing one but alphabetically sooner

view this post on Zulip Eric Wieser (Jun 30 2020 at 09:22):

And then the muscle memory breaks

view this post on Zulip Mario Carneiro (Jun 30 2020 at 09:22):

sure, which is why changes to translations.json shouldn't be taken lightly

view this post on Zulip Mario Carneiro (Jun 30 2020 at 09:22):

in most common cases we also have duplicates for prefixes when we want to calibrate this behavior

view this post on Zulip Mario Carneiro (Jun 30 2020 at 09:23):

but I think if the file was closed under taking prefixes it would be about 200-300% larger

view this post on Zulip Eric Wieser (Jun 30 2020 at 09:23):

Just for context for anyone else reading, these are the lines in question that I'm worried about

https://github.com/leanprover/vscode-lean/blob/66952a2fd27b3821ef4f67ad4b55e99f6a3991ab/src/input.ts#L262-L267

view this post on Zulip Mario Carneiro (Jun 30 2020 at 09:24):

Looking at that code, it's also deterministic based on the order they appear in the file

view this post on Zulip Mario Carneiro (Jun 30 2020 at 09:24):

so you can calibrate preferences by reordering too

view this post on Zulip Eric Wieser (Jun 30 2020 at 09:25):

I'm not certain that's true - from what I can tell, keys that look like numbers are shuffled, at least in some javascript implementations

view this post on Zulip Mario Carneiro (Jun 30 2020 at 09:26):

I don't think that's a major issue since the only keys that look like numbers are \0 ...\9 which have no proper prefixes

view this post on Zulip Mario Carneiro (Jun 30 2020 at 09:28):

you might be right though if this is stored as a hashmap

view this post on Zulip Mario Carneiro (Jun 30 2020 at 09:29):

Anyway, the way I would look at it is that \_ is unassigned, so by luck it currently resolves to \_a. If that's what you wanted, great, otherwise maybe say what you mean or come up with something better that \_ should resolve to

view this post on Zulip Eric Wieser (Jun 30 2020 at 09:33):

What bugs me is I normally type \_ by accident due to hitting space too soon or something, and having it complete as a makes me squint to work out what happened.

view this post on Zulip Mario Carneiro (Jun 30 2020 at 09:36):

generally whenever you write \... it will complete to a character if and only if you write a space. If you didn't finish writing the sequence you wanted then you probably got the wrong character

view this post on Zulip Mario Carneiro (Jun 30 2020 at 09:36):

if you learn the shortest sequence then that's basically true by definition

view this post on Zulip Mario Carneiro (Jun 30 2020 at 09:37):

If the issue is that you don't realize that you typed \_a instead of \_v and can't see the difference between the characters, then that's probably overuse of unicode or a bad font

view this post on Zulip Eric Wieser (Jun 30 2020 at 09:38):

That's a fair comment

view this post on Zulip Eric Wieser (Jun 30 2020 at 09:38):

One thing I'd perhaps propose is to allow blacklisting sequences as "_": null, in that file. If the shortest sequence matches a blacklisted one, then perform no replacement.

view this post on Zulip Eric Wieser (Jun 30 2020 at 09:39):

But essentially I'm describing damage control for my own clumsy typing...

view this post on Zulip Mario Carneiro (Jun 30 2020 at 09:40):

An easy way to accomplish that would be "_": "\_"

view this post on Zulip Mario Carneiro (Jun 30 2020 at 09:41):

It would be nice if users could add their own translations via vscode settings

view this post on Zulip Mario Carneiro (Jun 30 2020 at 09:41):

maybe they already can, I'm not sure

view this post on Zulip Eric Wieser (Jun 30 2020 at 09:41):

Allowing customization sounds hard given we just decided they were ordered

view this post on Zulip Eric Wieser (Jun 30 2020 at 09:41):

Your approach feels like a (effective) hack, changing the typescript to allow null would be fairly trivial

view this post on Zulip Mario Carneiro (Jun 30 2020 at 09:42):

On startup it would read the settings and overwrite all the global translations as directed

view this post on Zulip Mario Carneiro (Jun 30 2020 at 09:42):

I don't deny it is a hack

view this post on Zulip Eric Wieser (Jun 30 2020 at 09:42):

Ah, so tell users to start by copying the entire translations.json, rather than attempting to merge user translation settings with upstream ones

view this post on Zulip Mario Carneiro (Jun 30 2020 at 09:42):

If you want to support that in vscode, PR's are welcome

view this post on Zulip Mario Carneiro (Jun 30 2020 at 09:43):

No, I'm saying merge settings

view this post on Zulip Eric Wieser (Jun 30 2020 at 09:43):

Just thought I'd float the idea before bothering with a PR. If it keeps bugging me, I'll make one :)

view this post on Zulip Mario Carneiro (Jun 30 2020 at 09:45):

like if translations.json has {"a": "A", "b": "B", "d": "D"} and settings.json has "lean.translations_override": {"a": "C", "b": null, "c": "C"} then it behaves as though it was given {"a": "C", "b": null, "c": "C", "d": "D"}

view this post on Zulip Mario Carneiro (Jun 30 2020 at 09:46):

so if the underscore thing bothers you then you can add {"_": null} to your local settings and translations.json doesn't have to change

view this post on Zulip Mario Carneiro (Jun 30 2020 at 09:46):

and you still get the benefit of future changes to translations.json

view this post on Zulip Eric Wieser (Jun 30 2020 at 09:49):

How does your merger decide at what position to insert c?

view this post on Zulip Edward Ayers (Jun 30 2020 at 10:21):

This already exists in vscode: eg

    "lean.input.customTranslations": {
        "a": "α",
        "al": "α", "be": "β", "ga": "γ", "de": "δ", "ep": "ε", "ze": "ζ",
        "et": "η", "th": "θ", "io": "ι", "ka": "κ", "la": "λ", "mu": "μ",
        "nu": "ν", "xi": "ξ", "pi": "π", "rh": "ρ", "si": "σ",
        "ta": "τ", "ph": "φ", "ch": "χ", "ps": "ψ", "om": "ω",
    ...
    }

view this post on Zulip Edward Ayers (Jun 30 2020 at 10:21):

then vscode will merge the translation files, with the ones in customTranslations clobbering the other

view this post on Zulip Edward Ayers (Jun 30 2020 at 10:26):

although there is no null support as of yet

view this post on Zulip Eric Wieser (Jun 30 2020 at 10:34):

To be clear with my point about clobbering - javascript objects are ordered dictionaries, so there's not a unique definition of what merging looks like

view this post on Zulip Edward Ayers (Jun 30 2020 at 10:38):

I think in the sourcecode it is just {...globalTranslations, ...customTranslations}, so they are treated as unordered here.

view this post on Zulip Eric Wieser (Jun 30 2020 at 10:40):

That results in the order being (assuming VScode matches chrome):

  • Existing keys keep their order
  • custom keys are added last (so will never win ties)

view this post on Zulip Eric Wieser (Jun 30 2020 at 10:41):

Edward Ayers said:

although there is no null support as of yet

Reading the source, it looks like it is implicitly already supported.

view this post on Zulip Edward Ayers (Jun 30 2020 at 10:43):

No custom keys always win ties.

view this post on Zulip Eric Wieser (Jun 30 2020 at 10:44):

{...{d: 1, c:2, b:3}, ...{c:3, a:5}} results in {d: 1, c: 3, b: 3, a: 5} with the key a being last. The lines I link to above show the earliest element is used to break ties.

view this post on Zulip Edward Ayers (Jun 30 2020 at 10:52):

I believe Javascript objects are unordered dictionaries so it doesn't matter where a appears in the resulting object. The important thing is that in your example c:3 clobbers c:2 .

view this post on Zulip Eric Wieser (Jun 30 2020 at 10:53):

If that were true there would be bigger problems for breaking ties, since the completer is affected by their iteration order.

view this post on Zulip Edward Ayers (Jun 30 2020 at 10:57):

Ah I see what you mean, in the case that the string is not an exact match it iterates through the object so the iteration order matters. In the implementation, it takes the shortest completion so there is only iteration-order-dependence if there are two completions with the same length and the same prefix.

view this post on Zulip Eric Wieser (Jun 30 2020 at 10:58):

Yes, and that case is what this conversation started as :)

view this post on Zulip Mario Carneiro (Jun 30 2020 at 11:24):

But if you add your own custom translation for a prefix then you don't have to worry about tiebreak behavior

view this post on Zulip Edward Ayers (Jun 30 2020 at 11:28):

Custom translations supports null with this PR: https://github.com/leanprover/vscode-lean/pull/197


Last updated: May 13 2021 at 21:12 UTC