search

iu-parfunc / verified-instances

Verified instances for parallel programming.
BSD 3-Clause "New" or "Revised" License
8 stars 5 forks source link

Updates for LH 084 #10

Closed ranjitjhala closed 5 years ago

ranjitjhala commented 5 years ago

Hi @RyanGlScott -

I made a bunch of updates to make the Sum/Prod files compatible with LH 084, so so the UCSC folks @lkuper and @KamalaRamas can play around with those proofs. Not sure if we want to merge this back into the master or create a separate branch on your original? Any thoughts?

The relevant branch is here:

https://github.com/ranjitjhala/verified-instances/tree/lh-84

RyanGlScott commented 5 years ago

I have no objections to merging this into master—if it doesn't work with the latest version of Liquid Haskell, then let's fix it!

ranjitjhala commented 5 years ago

Well its not so easy because the rest of the stuff is linked to earlier versions of lvars etc. so not sure if that will break or no 😟

RyanGlScott commented 5 years ago

Ah. Is the issue that the LVar-related code doesn't build with a newer GHC? If so, perhaps we should take the existing stack.yaml file, rename it to something else (e.g., stack-lts-8.21.yaml), and add a new stack.yaml file without support for the LVar stuff. That way, we can incrementally port over the LVar code later, while still retaining the ability to build it if you explicitly point stack to the right YAML file.

ranjitjhala commented 5 years ago

Yes, I'd say either:

  1. Just leave the current thing in a branch OR
  2. First update the whole thing so it builds with stack-lts-12.2 or similar and then update the LH bits?

I can totally understand if you don't want to undertake the hassle of (2) ATM (other priorities etc.) in which case make an LH-84 branch or such and I'll submit a PR against that?

RyanGlScott commented 5 years ago

Question: is the new code backwards-compatible with old versions of Liquid Haskell? If so, I would suggest just keeping all of the code in master, since it wouldn't hurt anything to do so. If breaking changes are required, then I would be in favor of archiving the current code in a branch, then putting the new code in master.

ranjitjhala commented 5 years ago

Nope, the new code is not backwards compatible so it will break stuff.

ranjitjhala commented 5 years ago

so yes, better to archive I think and make the new stuff master? shall I submit a PR against master then?

RyanGlScott commented 5 years ago

Indeed, a PR against master sounds good. In fact, #11 has appeared. Hooray!

Also, I've archived the current master in the https://github.com/iu-parfunc/verified-instances/tree/lts-8.21 branch.

RyanGlScott commented 5 years ago

Resolved in #11.