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

Adding proof using annotation. #5

Closed ahmet-celik closed 8 years ago

wilcoxjay commented 8 years ago

Hello @ahmet-celik,

Thank you very much for the PR! We had been talking about adding these annotations just this week, so you have great timing!

Before I merge this, would you mind undoing the changes that remove the last newline of each file? If this is too much trouble, just let me know, and I can do it when I merge.

Thanks again!

James

palmskog commented 8 years ago

Unless Ahmet can do it really quickly, I can take care of the newline thing in a separate branch, along with some small manual adjustments. (Yes, I asked Ahmet to do these changes, but wasn't prepared for full-blown PR this quickly.)

wilcoxjay commented 8 years ago

That makes sense.

Since there is no way to change the branch on a Github PR, either Ahmet will need to push these changes, or we will need to close this PR and open a separate one for Karl's branch.

ahmet-celik commented 8 years ago

Your welcome. I added the last newline of each file. Thanks, Ahmet

palmskog commented 8 years ago

I think this looks good enough to be merged on its own now, so @wilcoxjay feel free to do that if you agree.

However, to get the full benefit of the quick compilation toolchain, there are still some changes that need to be made in makefiles and in other places, but I think that should go in separate PRs.

Thanks again Ahmet!

wilcoxjay commented 8 years ago

Sounds good, merging!