344 resolve lean auto complete symbol aliases

[GitLuckier]

Description

Fixes cluttered autocomplete by consolidating symbol aliases. Instead of showing every Lean alias as a separate entry, the script now uses LaTeX as a filter: only Lean aliases that also appear in LaTeX are added, bridging Waterproof commands with standard LaTeX. For symbols with no LaTeX match, only the longest alias is kept. The detail field on each entry lists all other known aliases, so users can still discover them.

There are still 22 symbols with aliases that share a common prefix, meaning they can still appear together in the autocomplete when a user types the first few characters. Fixing this properly would require coalescing same-symbol entries in CodeMirror itself, which may be worth raising with the CodeMirror maintainer (Marijn). The remaining problematic pairs are:

⊊  [+9]  \subsetneqq, \subsetneq
⊋  [+9]  \supsetneqq, \supsetneq
⊇  [+8]  \supseteqq, \supseteq, \supset
⇒  [+7]  \implies, \implies-right
⋚  [+6]  \lesseqgtr, \lesseqqgtr
⋨  [+5]  \precnapprox, \precnsim
⋛  [+5]  \gtreqless, \gtreqqless
⋩  [+5]  \succnapprox, \succnsim
≾  [+4]  \precapprox, \precsim
≲  [+4]  \lessapprox, \lesssim
≨  [+4]  \lneqq, \lneq
≩  [+4]  \gneqq, \gneq
≿  [+4]  \succapprox, \succsim
≽  [+4]  \succcurlyeq, \succeq
≳  [+3]  \gtrapprox, \gtrsim
≤  [+2]  \less-or-equal, \leq
⋦  [+2]  \lnapprox, \lnsim
⋧  [+2]  \gnapprox, \gnsim
≥  [+1]  \greater-or-equal, \geq
≠  [+1]  \not-equal, \neq
∘  [+1]  \circ, \compose
√  [+1]  \surd, \sqrt

In the worst case, it can look like this:

Here, two symbols have their alias show up in the same window. This is rare enough that I am not sure if it is worth the trouble to go to Marijn.

Changes

completions/symbols.json

• Renamed \ksi, \Ksi, and \omikron to \xi, \Xi, and \omicron to align with LaTeX conventions. Note that \omicron and \Omicron were previously using inconsistent spelling conventions; they now both follow LaTeX.
• Added \vee (∨) and \. (·) as entries.

scripts/

• Migrated generate-symbols.mjs to TypeScript as generate-symbols.mts.
• Split the script into a generate-symbols-helpers/ folder with separate files for config, types, utilities, reporting, and tests. The key file for reviewers to check is generate-symbols.config.mts, which contains all tunable settings: which symbol groups are shown in the panel, boost values, merge strategy, and the label deduplication strategy.
• Added latex2unicode.json, a LaTeX-to-unicode mapping derived from the unicode-math package (LPPL 1.3c), used as the primary filter for Lean aliases.
• Added tsconfig.json for the scripts folder.
• Updated package.json to point to the new .mts script.

Testing this PR

Please run the script with --test before approving. The main reason is not the 13 validation checks at the end, but the detailed report it prints: what aliases were dropped, what symbols were added via LaTeX, what was added via Lean fallback, and which labels were removed by the deduplication strategy. This is the main way to audit what ended up in the output file and why.

node generate-symbols.mts --test

You can also add --verbose to see additional detail, such as the full lean-fallback list and labels skipped because they contain {}, but the report from --test alone covers the most important information.

Companion PR: impermeable/waterproof-editor#94

Closes #344