leanprover-community
move Webeditor to a separate github package
Ideally, all projects should import the Webeditor package, so they get access to #package_version. For this, it needs to be a separate repo.
I know our infrastructure does not support this well yet but especially for # commands that are not supposed to "functionally" be part of a package, it would make more sense to inject them dynamically via --plugin instead of making all packages import them statically.
I have to read up on --plugin, that's the first time I hear of it, but it sounds like the right thing!
Infrastructure might support it now after this weekend's changes
To my knowledge the current state is that, using --plugin isn't as easy as anticipated and I'm not aware of any demo or doc that would explain how to do this.
If anybody knows how to dynamically load a command #my_command dynamically via --plugin, I'd be happy to see a short demo!