update to latest liquid-fixpoint#2282
Conversation
|
@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 |
|
The latest fixpoint is not compatible with the latest liquid haskell, that is why these changes were required. So, let's merge both pull requests! |
|
@clayrat this is WIP only because fixpoint was not fixed yet? |
|
Yes, I'll point the LF submodule to the latest commit and drop the WIP prefix. |
|
@nikivazou done |
Don't merge yet (before ucsd-progsys/liquid-fixpoint#688), the LF submodule currently points to a branch.
Fixes #2272
@ranjitjhala I had to remove two things to make LH work with the
developversion of LF:fTyConPas a parser with the same name was made public at Use SMTLIB style serialization/deserialization for Horn queries liquid-fixpoint#683SourcePoswhich were added at Allow reading/saving horn queries from/to JSON liquid-fixpoint#680The 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.