Spellchecking in `set.mm` (and `iset.mm`)

[tirix]

As shown in metamath-knife#186, and the resulting #4867, it's possible to add spell checking for comments in set.mm.
The first question is whether we want to develop those tools to e.g. have a goal of including spell checking in CI.

If we agree on this goal, we could discuss on the method. The "hunspell dictionary" I've used in metamath-knife seems to be a pretty common approach, with english dictionaries available in the public domain.

In metamath-knife, I'm importing and statically linking such a public domain english dictionary, https://github.com/wooorm/dictionaries/tree/main/dictionaries/en, however words like "adjoint", "orthomodular" or "morphism" weren't included, so it does not seem to be complete with regard to many mathematical terms. I have not found a dictionary covering mathematical words, maybe you could help with that.. Depending on what we find, we could have to enhance or extend the dictionary.

Either way there will be some terms specific to the database, like wff, setvar, which we will want to use in the comments and pass spell checking.

So overall a solution could be to:

• add the possibility in metamath-knife to use custom dictionaries,
• store in the metamath/set.mm GitHub repository a dictionary with additional math entries, which we could add using the option above,
• add in set.mm and iset.mm a list of custom entries specific to the database, using a special $j command.

What's your opinion?

[tirix]

For reference : I found https://github.com/emareg/acamedic, which seems to be more complete with math words (e.g. it does include several "morphism" variants like "automorphism", but not "morphism" itself).

Dictionary options so far:

• https://github.com/emareg/acamedic (10k words)
• https://github.com/wooorm/dictionaries/tree/main/dictionaries/en (50k words)
• https://github.com/ropensci/hunspell/tree/master/inst/dict (50k words)
• https://github.com/elastic/hunspell/blob/master/dicts/en_US (62k words)

[wlammen]

however words like "adjoint", "orthomodular" or "morphism" weren't included

What about adding a small Metamath dictionary containing specialized words like those above? Adding a new item requires approvals from others and/or pointers to literature where it was used before.

Edit: You already suggested something similar here
we could have to enhance or extend the dictionary.

[wlammen]

Typos are not really a problem, in my eyes, occasionally a bit annoying, but otherwise without great negative effect (Searching? I had no difficulty, so far.). Creating a consistent vocabulary is more valuable, I think.

[tirix]

Creating a consistent vocabulary is more valuable, I think

Spellchecking might also help somehow for that.

[jkingdon]

I guess I don't have much of an opinion. I suppose putting in tooling might reduce flexibility a bit, but probably not in ways that are especially important (provided we can add to the dictionary as we coin terms or, more likely, bring them in from specialties not yet formalized).

So I don't have a strong desire for spellchecking, but I don't object either.