ucsd-progsys / liquidhaskell

Liquid Types For Haskell
BSD 3-Clause "New" or "Revised" License
1.19k stars 137 forks source link

POC haskell-ide-engine integration #1352

Closed alanz closed 6 years ago

alanz commented 6 years ago

I am experimenting with an initial proof of concept integration of LH into hie.

My first intention is to run the liquid executable externally, and to present the contents of the .liquid directory via the hie UI, as a combination of hover annotations and diagnostics.

This avoids the issue of getting LH to compile with all the versions of GHC that hie supports.

It seems I have a choice of files to choose from to get the info. My initial investigation shows that I can get the hover information from the xxx.vim.annot file, and the error information from the errors key in the xxxx,json file.

The xxxx.err file seems to have the most comprehensive information, but to read it properly I need to include the LH source as a library, which potentially introduces compilation problems.

Is this an appropriate way to do it? An alternative seems to be to run the liquid --json but that only returns the error information.

ranjitjhala commented 6 years ago

Wow, that’s terrific! Yes, using the .liquid folder is indeed easiest.

The hover information is also there in the .json file, see this description of the format

https://github.com/ucsd-progsys/liquid-server#json-format

(We use the json output for the web based demo which essentially returns the generated json file to the js browser client)

On Tue, Jul 31, 2018 at 4:28 AM Alan Zimmerman notifications@github.com wrote:

I am experimenting with an initial proof of concept integration of LH into hie.

My first intention is to run the liquid executable externally, and to present the contents of the .liquid directory via the hie UI, as a combination of hover annotations and diagnostics.

This avoids the issue of getting LH to compile with all the versions of GHC that hie supports.

It seems I have a choice of files to choose from to get the info. My initial investigation shows that I can get the hover information from the xxx.vim.annot file, and the error information from the errors key in the xxxx,json file.

The xxxx.err file seems to have the most comprehensive information, but to read it properly I need to include the LH source as a library, which potentially introduces compilation problems.

Is this an appropriate way to do it? An alternative seems to be to run the liquid --json but that only returns the error information.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1352, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOEu-kfl5IA5r5Wq2FyVNg07XC1w9ks5uMD9kgaJpZM4VoE8g .

alanz commented 6 years ago

My problem is that the types in the .json file only give the starting point, not the end as well. Which is why I plan on using the vim annotations, which has both.

ranjitjhala commented 6 years ago

Did you mean the start and end of the source-spans, or something else?

Rather than parse the custom vim format, it may be easier for me to extend

the JSON file with whatever extra information you want?

On Tue, Jul 31, 2018 at 8:21 AM Alan Zimmerman notifications@github.com wrote:

My problem is that the types in the .json file only give the starting point, not the end as well. Which is why I plan on using the vim annotations, which has both.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1352#issuecomment-409259306, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOAIEctDkBOdwS7DpggpKHQLECSTXks5uMHX2gaJpZM4VoE8g .

ranjitjhala commented 6 years ago

It looks like the action happens here:

https://github.com/ucsd-progsys/liquidhaskell/blob/develop/src/Language/Haskell/Liquid/UX/Annotate.hs#L91-L120

alanz commented 6 years ago

Yes, I have been looking at that code.

Having the JSON emit the end point of the span, not just the start for the types is the missing bit, that is pushing me to the vim side.

And I can see in future managing synchronisation by running liquid under control of hie, using the --json option. But at the moment that only returns the errors, not the types as well. So having an additional flag to spit that out would help.

ranjitjhala commented 6 years ago

Ok, I'll add an "end" field that looks like:

{ ...,  "end" : { "row" : int, "col" : int } } 

?

alanz commented 6 years ago

That sounds fine. The errors do

  "errors": [
    {
      "start": {
        "line": 9,
        "column": 1
      },
      "stop": {
        "line": 9,
        "column": 8
      },
      "message": "Error: Liquid Type Mismatch\n  Inferred type\n    VV : {v : Int | v == (7 : int)}\n \n  not a subtype of Required type\n    VV : {VV : Int | VV mod 2 == 0}\n \n  In Context"
    }

so maybe use the same position format?

alanz commented 6 years ago

This is using the .json file in the .liquid directory, if it exists

screenshot from 2018-07-31 23-06-00

You will notice the error in the pane at the bottom, as well as the red squiggle on line 9.

alanz commented 6 years ago

I just merged https://github.com/haskell/haskell-ide-engine/pull/732 which means haskell-ide-engine current master can now show errors and types for liquid haskell projects.

It only looks for them when the file is saved though.

And it currently uses the json file and the vim annotations.

ranjitjhala commented 6 years ago

Awesome thanks!!!! will try this out ASAP!!

On Sat, Aug 4, 2018 at 6:20 AM Alan Zimmerman notifications@github.com wrote:

I just merged haskell/haskell-ide-engine#732 https://github.com/haskell/haskell-ide-engine/pull/732 which means haskell-ide-engine current master can now show errors and types for liquid haskell projects.

It only looks for them when the file is saved though.

And it currently uses the json file and the vim annotations.

— You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1352#issuecomment-410449094, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOPw9QUdKfA4lMS2TeiuLwnUHbGcQks5uNZ-XgaJpZM4VoE8g .

alanz commented 6 years ago

haskell-ide-engine from https://github.com/haskell/haskell-ide-engine/pull/802 supports running the liquid exe when a file is saved, and then returning the diagnostics from it.

Version 0.0.22 of the vscode "Haskell Language Server" plugin has a configuration item to enable this feature. It is disabled by default.

alanz commented 6 years ago

It only runs liquid on save, as it is potentially a long-running process.

And it makes sure there is only one running at a time, if a new save happens, any existing process is killed.

Is that safe?

ranjitjhala commented 6 years ago

Yup that should be safe!

On Wed, Sep 5, 2018 at 11:41 AM Alan Zimmerman notifications@github.com wrote:

It only runs liquid on save, as it is potentially a long-running process.

And it makes sure there is only one running at a time, if a new save happens, any existing process is killed.

Is that safe?

— You are receiving this because you modified the open/close state.

Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1352#issuecomment-418837177, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOHVVQXXCTdnv7odgP0zf3bt_9bfjks5uYBrVgaJpZM4VoE8g .