feat: abbreviate average: ⨍, -int: ⨍, oiint: ∯, tint: ∯, pd: ∂

[girving]

Zulip discussion

[girving]

Unfortunately I am unsure how to test this. I followed these instructions, but npm run test eventually produced

lean4:   Lean4 Bootstrap Test Suite
lean4: 22:36:27.017 - executeWithProgress lean +leanprover/lean4:nightly-2022-10-26,--version
lean4: 22:36:27.018 - =================== Install elan on demand ===================
lean4: 22:36:27.037 - child process exited with code 0
lean4: 22:36:27.048 - Loaded document untitled:Untitled-1
lean4: 22:36:27.048 - Setting lean4 language on untitled doc
lean4: 22:36:27.106 - child process exited with code 0
lean4: 22:36:27.117 - child process exited with code 0
lean4: 22:36:27.117 - executeWithProgress lean +nightly,--version
lean4: 22:36:27.133 - Waiting for extension leanprover.lean4 to be loaded...
lean4: 22:36:27.133 - Found extension: leanprover.lean4
lean4: 22:36:27.133 - Waiting for extension leanprover.lean4 activation...
lean4: 22:36:27.133 - Extension leanprover.lean4 isActive=true
lean4: 22:36:27.134 - Found lean package version: 0.0.123
lean4: 22:36:27.134 - Waiting for InfoView...
lean4: 22:36:27.134 - InfoView is open.
lean4: 22:36:27.134 - Wait for elan install of Lean nightly build...
lean4: 22:36:27.134 - Waiting for active client ...
lean4: 22:36:27.219 - child process exited with code 0
lean4: 22:36:27.219 - [ClientProvider] Creating LeanClient for untitled:
lean4: 22:36:27.219 - [ClientProvider] firing clientAddedEmitter event
lean4: 22:36:27.219 - [InfoProvider] Adding client for workspace: untitled:
lean4: 22:36:27.219 - [LeanClient] Restarting Lean Server
lean4: 22:36:27.225 - [LeanClient] starting
lean4: [main 2024-01-12T22:36:27.302Z] CodeWindow: failed to load (reason: <unknown>, code: -3)
lean4: 22:36:27.407 - [InfoProvider] initInfoView got null client.
lean4: 22:36:27.686 - [LeanClient] running, started in 466 ms
lean4: 22:36:27.689 - [InfoProvider] got client restarted event
lean4: 22:36:27.692 - [InfoProvider] initInfoView!
lean4: 22:36:28.134 - Waiting for active client to enter running state...

at which point the tests hung.

[mhuisi]

I'm not sure why the tests are broken for you. They can be somewhat non-deterministic, but should always time out eventually. Additionally, there are no tests related to the abbreviations feature.

Do you still want to add the other abbreviations suggested in the thread before merging?

[girving]

I added the other abbreviations from Zulip.

[girving]

In terms of tests, not sure what to do. It still runs through a few tests and then hangs, but as you say this is likely not related to abbreviations.json.