-
Notifications
You must be signed in to change notification settings - Fork 200
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Move some specs from remote spec table into local repo #116
Conversation
Signed-off-by: Andrew Helwer <[email protected]>
Signed-off-by: Andrew Helwer <[email protected]>
Signed-off-by: Andrew Helwer <[email protected]>
Signed-off-by: Andrew Helwer <[email protected]>
Signed-off-by: Andrew Helwer <[email protected]>
Signed-off-by: Andrew Helwer <[email protected]>
Signed-off-by: Andrew Helwer <[email protected]>
Signed-off-by: Andrew Helwer <[email protected]>
Signed-off-by: Andrew Helwer <[email protected]>
Signed-off-by: Andrew Helwer <[email protected]>
Signed-off-by: Andrew Helwer <[email protected]>
Signed-off-by: Andrew Helwer <[email protected]>
Signed-off-by: Andrew Helwer <[email protected]>
@@ -5,3 +5,8 @@ | |||
# Example: | |||
specifications/doesnotexist | |||
|
|||
# Ignore submodules to ensure deterministic local execution |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can you please explain why they would introduce non-determinism? Don't the submodule points to a particular commit?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Basically if some people have the repo checked out with submodules they'll generate a different manifest.json than if other people have the repo checked out without submodules.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is that a problem given that the authoritative manifest is generated by our GitHub action?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It isn't actually generated by the action, the action just validates that it's correct.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sounds good enough to catch it when somebody accidentally generates the manifest without the submodules. :-)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I suppose it is, but putting these dirs in the .ciignore file saves whoever is trying to submit specs to the examples repo a CI round trip. It's easy to remove these if we want to add these dirs to the CI eventually, although at this point we literally do want the CI to ignore them.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah you're talking about adding the submodule specs to the CI. Well, maybe. I will look into doing that after this work.
Signed-off-by: Andrew Helwer <[email protected]>
Signed-off-by: Andrew Helwer <[email protected]>
Signed-off-by: Andrew Helwer <[email protected]>
Signed-off-by: Andrew Helwer <[email protected]>
Signed-off-by: Andrew Helwer <[email protected]>
Signed-off-by: Andrew Helwer <[email protected]>
Signed-off-by: Andrew Helwer <[email protected]>
Signed-off-by: Andrew Helwer <[email protected]>
Added: - Murat's PlusCal version of Lamport & Gray's analysis of Paxos vs. Two-Phase Commit - Voucher Transaction System - Atomic Commitment Protocol - Byzantine Paxos Signed-off-by: Andrew Helwer <[email protected]>
Also update remote spec table format.
Specs added: