hls-hectare-plugin #3159
hls-hectare-plugin #3159
Conversation
|
Correction: ECTAs are a new data structure and constraint solver for enumerative program synthesis, available from https://hackage.haskell.org/package/ecta . The tool is Hectare. I failed one of the goals of the presentation if some people think it was just a tool. |
|
I think then that the plugin I published might be misnamed. Since the package on Hackage is called |
|
The plan here is to launch |
|
What's blocking this from getting merged? |
pepeiborra
requested review from
Anton-Latukha,
Ailrun and
michaelpj
as code owners
|
|
||
| descriptor :: PluginId -> PluginDescriptor s | ||
| descriptor pluginId = (defaultPluginDescriptor pluginId) | ||
| { pluginModifyDynflags = staticPlugin |
There was a problem hiding this comment.
So all this does is enable the Hectare plugin? I'm a bit confused by this. I would expect that if users want a GHC plugin then they can just add it to their project themselves. It seems a a bit roundabout (and extra work for us) to have HLS plugin for every GHC plugin like that?
There was a problem hiding this comment.
This is a good question. The Hectare GHC plugin doesn't make programs type check, it does not add a static analysis pass, nor does it rewrite your program to make it faster. It is an IDE plugin, designed to help you write programs faster.
Why is it packaged as a GHC plugin instead of as an HLS plugin then? Well, I guess a GHC plugin is more reusable - anyone can import it in their project, not just HLS users.
Why repackage it as an HLS plugin?
- For convenience, just as we repackage code formatters and linters.
- For discoverability, although that is a weaker argument since the plugin is disabled by default.
There was a problem hiding this comment.
I think the comparison with formatters and linters is interesting:
- For formatters, you get a new way of interacting with the tool, including things like convenient range formatting
- For linters you get the diagnostics integrated with HLS
If we needed this plugin in order for the Hectare diagnostics to work I'd definitely be in favour - it's just that the Hectare developers have been so clever in getting their diagnostics into hole fit suggestions that we don't actually need to do anything if the user turns on the plugin themselves. In no other case is the plugin actually unnecessary.
But I do take your argument about it being a pure IDE plugin. There wouldn't be much point enabling it in your cabal file, really!
All of which is to say: I don't know 🤷 so I guess if you're willing to maintain it we can include it!
| LICENSE | ||
|
|
||
| library | ||
| if impl(ghc >= 8.10) && impl(ghc < 9.0) |
There was a problem hiding this comment.
Given that we might drop support for 8.10.7 after the next major release, do we want to add plugins that only work on 8.10?
|
rebased the PR, ready to get merged now? |
Hectare is a type-driven code synthesis tool presented at ICFP by @jkoppel. @Tritlo packaged it in a GHC plugin that packages the results as typed hole suggestions, and this is a simple HLS plugin that conveniently packages the GHC plugin. Paper
The plugin is opt-in as it is disabled by default. This is because the Hectare search is triggered automatically for all typed holes as part of type checking, which means no diagnostics until the search is finished. To enable the plugin, you can set the following LSP property:
This will enable the Plugin immediately, no restart needed. However, Hectare seems to be quite buggy at the moment, check the HLS logs where exceptions will be dumped.