search

uwplse / verdi-raft

An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
BSD 2-Clause "Simplified" License
183 stars 19 forks source link

port to Coq 8.6 #43

Closed palmskog closed 7 years ago

palmskog commented 7 years ago

Fix proofs written for 8.5 that fail in 8.6 (not always completely cleanly). Restrict to 8.6 only. Verdi's Travis script needs to be adjusted after this is merged. To avoid making permanent a long and silly history, this should be squash-merged.

ztatlock commented 7 years ago

The changes all looked reasonable to me. Thanks for pushing the migration through!

jssandh2 commented 7 years ago

If we're indeed supporting Coq 8.6 for Verdi now, can we at least have the README.md reflect that by stating that Mac users can install that independently as : brew install coq ? cc : @wilcoxjay

palmskog commented 7 years ago

@jssandh2 Verdi (the framework) currently supports both Coq 8.5 and 8.6, regardless of how you install it. Verdi Raft is now 8.6 specific, since there is no reasonable way of supporting both 8.5 and 8.6 simultaneously in the proofs. However, we expect that most users of the framework never need to build or edit Verdi Raft - that's why we split it out from Verdi.

If you feel the Verdi documentation is lacking, please submit a Verdi PR and we can discuss those changes separately.

jssandh2 commented 7 years ago

@palmskog : Got it. Thanks for the clarification. The reason I mentioned it is because I got into an issue with Coq 8.6 when I installed Verdi (~ 3 weeks ago?). I had already installed Coq 8.6, and I needed to manually configure my .bash_profile so that opam was pointing to right Coq when I was doing a make. However, since verdi-raft will explicitly support Coq 8.6, this seems fine. I mentioned this merely because I have a branch on Verdi that I plan on merging once I write a few proofs, and it's using Coq 8.5 and I was worried that it would cause my PR to break.