search

ucsd-progsys / liquidhaskell

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

update to latest liquid-fixpoint #2282

Closed clayrat closed 6 months ago

clayrat commented 6 months ago

Don't merge yet (before https://github.com/ucsd-progsys/liquid-fixpoint/pull/688), the LF submodule currently points to a branch.

Fixes #2272

@ranjitjhala I had to remove two things to make LH work with the develop version of LF:

  1. fTyConP as a parser with the same name was made public at https://github.com/ucsd-progsys/liquid-fixpoint/pull/683
  2. conflicting JSON instances for SourcePos which were added at https://github.com/ucsd-progsys/liquid-fixpoint/pull/680

The tests pass without those, but I'm unsure if we should remove them in favor of liquid-fixpoint implementations (as done currently), or if we need to de-duplicate somehow.

ranjitjhala commented 6 months ago

@clayrat -- I couldn't follow, I would suggest using the LF versions (which is the current setup?) if possible? Is that the path of least resistance?

clayrat commented 6 months ago

@clayrat -- I couldn't follow, I would suggest using the LF versions (which is the current setup?) if possible? Is that the path of least resistance?

Indeed, the simplest solution is just to delete the conflicting LH code, I was just worried there might be some non-obvious consequences not covered by the test suite, e.g. the code for fTyConP in LF has clauses for num and Str which are missing in LH version - not sure how important it is that LiquidHaskell will also start accepting those.

nikivazou commented 6 months ago

The latest fixpoint is not compatible with the latest liquid haskell, that is why these changes were required. It looks good to me (esp since the tests pass).

So, let's merge both pull requests!

nikivazou commented 6 months ago

@clayrat this is WIP only because fixpoint was not fixed yet?

clayrat commented 6 months ago

Yes, I'll point the LF submodule to the latest commit and drop the WIP prefix.

clayrat commented 6 months ago

@nikivazou done