Zulip Chat Archive

Stream: new members

Topic: how to write a superscript quickly?


Chris M (Jun 30 2020 at 05:33):

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

Shing Tak Lam (Jun 30 2020 at 05:34):

\inv

Chris M (Jun 30 2020 at 05:34):

cool

Johan Commelin (Jun 30 2020 at 05:47):

Also \-1

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.

Eric Wieser (Jun 30 2020 at 09:12):

Is there a reason vscode has no methanism to type ?

Johan Commelin (Jun 30 2020 at 09:12):

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

Eric Wieser (Jun 30 2020 at 09:13):

Mind linking to that file on github?

Shing Tak Lam (Jun 30 2020 at 09:14):

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

Eric Wieser (Jun 30 2020 at 09:14):

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

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

Mario Carneiro (Jun 30 2020 at 09:19):

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

Eric Wieser (Jun 30 2020 at 09:19):

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

Mario Carneiro (Jun 30 2020 at 09:19):

why? It's still better than nothing

Mario Carneiro (Jun 30 2020 at 09:20):

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

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

Eric Wieser (Jun 30 2020 at 09:22):

And then the muscle memory breaks

Mario Carneiro (Jun 30 2020 at 09:22):

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

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

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

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

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

Mario Carneiro (Jun 30 2020 at 09:24):

so you can calibrate preferences by reordering too

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

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

Mario Carneiro (Jun 30 2020 at 09:28):

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

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

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.

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

Mario Carneiro (Jun 30 2020 at 09:36):

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

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

Eric Wieser (Jun 30 2020 at 09:38):

That's a fair comment

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.

Eric Wieser (Jun 30 2020 at 09:39):

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

Mario Carneiro (Jun 30 2020 at 09:40):

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

Mario Carneiro (Jun 30 2020 at 09:41):

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

Mario Carneiro (Jun 30 2020 at 09:41):

maybe they already can, I'm not sure

Eric Wieser (Jun 30 2020 at 09:41):

Allowing customization sounds hard given we just decided they were ordered

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

Mario Carneiro (Jun 30 2020 at 09:42):

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

Mario Carneiro (Jun 30 2020 at 09:42):

I don't deny it is a hack

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

Mario Carneiro (Jun 30 2020 at 09:42):

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

Mario Carneiro (Jun 30 2020 at 09:43):

No, I'm saying merge settings

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 :)

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"}

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

Mario Carneiro (Jun 30 2020 at 09:46):

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

Eric Wieser (Jun 30 2020 at 09:49):

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

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": "ω",
    ...
    }

Edward Ayers (Jun 30 2020 at 10:21):

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

Edward Ayers (Jun 30 2020 at 10:26):

although there is no null support as of yet

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

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.

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)

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.

Edward Ayers (Jun 30 2020 at 10:43):

No custom keys always win ties.

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.

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 .

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.

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.

Eric Wieser (Jun 30 2020 at 10:58):

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

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

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: Dec 20 2023 at 11:08 UTC