search

espanso / hub

The official Espanso's package repository
MIT License
55 stars 141 forks source link

Add lean style math symbol completions #107

Closed johannesCmayer closed 5 months ago

johannesCmayer commented 8 months ago

Add math symbol completions based on the VScode lean extension.

AucaCoyan commented 8 months ago

Hello! The CI found an error

Validating package: lean-symbols... Found 1 errors: Check: incoherent_path ->: package name mismatch in package lean-symbols: the path indicates that the name is lean-symbols, but the manifest calls it espanso-lean-symbols

Would you kindly fix it? It's almost there 😄

johannesCmayer commented 5 months ago

I have now updated the package to incorporate all of the fixes. I will make another pull request because I actually regenerated all completions to the latest completions, and also removed all my custom modifications such that it is actually exactly the lean completions.

My main question is whether it makes sense to put the 30-line Python script that generates the completions in the package. It's not required, and it's not ever used, but it also seems like the natural place to put it.

smeech commented 5 months ago

I have now updated the package to incorporate all of the fixes. I will make another pull request because I actually regenerated all completions to the latest completions, and also removed all my custom modifications such that it is actually exactly the lean completions.

My main question is whether it makes sense to put the 30-line Python script that generates the completions in the package. It's not required, and it's not ever used, but it also seems like the natural place to put it.

That seems reasonable. 30 lines isn't large, it may be of interest, and I suppose it would enable users to update the list if it changed, although you might update the package with a new version if that occurred. Include some explanatory text in your new README.md, perhaps.