Port to v8.6: - Githubissues

uwplse / PUMPKIN-PATCH

Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker

MIT License

51 stars 2 forks source link

Port to v8.6: #2

Closed ejgallego closed 6 years ago

ejgallego commented 6 years ago

99% of the patching is due to the dubious Context representation change in Coq upstream.
update gitignore for newer ocaml versions.
add .merlin file

tlringer commented 6 years ago

Thanks for making this change! I will test this once I update to 8.6 locally, likely sometime next week.

tlringer commented 6 years ago

One of the regression test cases fails (example 6 in Regress.v). I'll need to see investigate to determine what caused this and how to fix it before porting the tool.

ejgallego commented 6 years ago

Umm, interesting; likely a 8.6 change in itself I think. Unless I did some typo/silly error, the patch should not make a difference in PUMPKIN-PATCH semantics themselves.

tlringer commented 6 years ago

Correct. All of your changes look good. The problem is that changes in tactic behavior between 8.5 and 8.6 meant that my regression tests produced different terms, which exposed bugs or unimplemented features that didn't matter with the old terms. I've added the necessary code to get those test cases working again, and I will push soon. Thanks again for going through the work and making this change!

ejgallego commented 6 years ago

No problem, thanks to you! Indeed 8.5 to 8.6 was a bit "rough", I think that 8.6 to 8.7 had much better regression testing so IMHO things should work better. It is interesting to know that tactic changes were meaningful in your context.