Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Extract abbreviation part of plugin into own package. #278

Open
Invisible-Rabbit-Hunter opened this issue Jul 30, 2021 · 4 comments
Open

Comments

@Invisible-Rabbit-Hunter

Hi, I'm wondering whether it'd be worth extracting the abbreviation part of the plugin into it's own packages, since it's useful in other languages, e.g. Agda, too. The current situation for abbreviations in Agda is not nearly as nice as Lean, and my current workaround has been to "activate" Lean abbreviation for Agda too. This works, but since the Lean plugin only loads in specific circumstances, it's quite annoying.

@gebner
Copy link
Member

gebner commented Jul 30, 2021

You can already use the abbreviation part in other languages, by adding agda to the lean.input.languages configuration option. But you've already figured that out. It's also unergonomic for another reason (see #277).

My main concern with making the abbreviations a separate plugin is how this impacts the installation UX. The user should only need to click install on a single extension in vscode. This also applies to upgrades: existing users of the extension must automatically get the new abbreviation extension. There are no technical issues with separating the extensions as far as I can tell. (We'd also need to update the bundle script.)

@PatrickMassot
Copy link
Contributor

I really really don't think we should make the Lean extension harder to install only to please Agda users.

@Invisible-Rabbit-Hunter
Copy link
Author

Would it not be possible to make the abbreviation part a separate git repository, then include it as a submodule here as well as upload it as a separate plugin? Then new users to Lean would have it no harder to install the plugin, and people who want to use ergonomic unicode input can install it as a separate plugin and use it in whatever language the choose.

@hediet
Copy link
Contributor

hediet commented Aug 6, 2021

You could also deploy it via npm. Alternatively, vscode extensions can have dependencies that are installed automatically.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

4 participants