Verify proofs in examples/ directory as part of PR workflow

[lemmy]

The prover's build checks a set of tests, and the PR verifies proofs from tlaplus/examples. However, the proofs in examples/ are not verified.

Related: https://github.com/tlaplus/tlapm/pull/135

[kape1395]

I thought we would move these examples to the https://github.com/tlaplus/Examples/ repo. If not, I can add them to the test cases.

[lemmy]

I don't have an opinion, except that some examples are perhaps too basic for the example repo?!

[muenchnerkindl]

I suggest we do this on a case-by-case basis. In particular, I think that Allocator, Euclid, Peterson, and perhaps GraphTheorem could go to the GitHub Examples repo. Bakery, Byzantine and standard Paxos, EWD 840, and LamportMutex are in there already, but we should check if there is anything in tlapm/examples that is worth merging into the existing modules. The other examples look too basic to me, but should probably be added to the tests if they aren't there already.

If you agree, I can take care of that reshuffle.

[kape1395]

Sounds like a good way to go.

[lemmy]

GraphTheorem could be aligned with a moved next to https://github.com/tlaplus/CommunityModules/blob/master/modules/Graphs.tla, like FiniteSetExtTheorem is next to FiniteSetExt in the CommunityModules?

[ahelwer]

I've been taking a look at this to compare the examples here with those in the tlaplus/examples repo using kdiff3. Here's what I found:

Example	Most-similar tlaplus/examples spec	How is tlaplus/examples version different?
ByzPaxos/BPConProof.tla	specifications/byzpaxos/BPConProof.tla	Minor changes; newer
ByzPaxos/Consensus.tla	specifications/byzpaxos/Consensus.tla	Identical except for some additional trailing whitespace
ByzPaxos/PConProof.tla	specifications/byzpaxos/PConProof.tla	Identical except for some additional trailing whitespace
ByzPaxos/VoteProof.tla	specifications/byzpaxos/VoteProof.tla	Identical except for some additional trailing whitespace
Cantor/Cantor*.tla	N/A	N/A
Dekker/Dekker.tla	N/A	N/A
paxos/Paxos.tla	specifications/paxos/Paxos.tla	Many differences, also lacking a proof
paxos/Consensus.tla	specifications/paxos/Consensus.tla	Additional comments and proofs
two_phase/TwoPhase.tla	specifications/TwoPhase/TwoPhase.tla	Lacking comments
two_phase/Alternate.tla	specifications/TwoPhase/Alternate.tla	Identical
Allocator.tla	specifications/Allocator/SimpleAllocator.tla	Seems older, lacks proofs
AtomicBakery.tla	specifications/Bakery-Boulangerie/Bakery.tla	Barely comparable; many differences
AtomicBakeryWithoutSMT.tla	specifications/Bakery-Boulangerie/Bakery.tla	Barely comparable; many differences
Bakery.tla	specifications/Bakery-Boulangerie/Bakery.tla	Barely comparable; many differences
BubbleSort.tla	N/A	N/A
Euclid.tla	N/A	N/A
EWD840.tla	specifications/EWD840/EWD840.tla	Numerous differences; proof was split out into EWD840_proof.tla; seems newer?
GraphTheorem.tla	N/A	N/A
LamportMutex.tla	specifications/lamport_mutex/LamportMutex.tla	Proof was split into LamportMutex_Proofs.tla; seems newer?
Peterson.tla	N/A	N/A
SimpleEventually.tla	N/A	N/A
SimpleEventuallyInt.tla	N/A	N/A
SimpleMutex.tla	N/A	N/A
SumAndMax.tla	N/A	N/A

I propose the following to integrate the specs into tlaplus/examples then delete the examples directory here:

Specs not in tlaplus/examples that should be added

• Cantor/Cantor*.tla
• Dekker/Dekker.tla
• BubbleSort.tla
• Euclid.tla
• GraphTheorem.tla
• Peterson.tla
• SimpleEventually.tla & SimpleEventuallyInt.tla (could go in specifications/LearnProofs)
• SimpleMutex.tla
• SumAndMax.tla (could go in specifications/LearnProofs)

Specs that should overwrite those in tlaplus/examples

• ByzPaxos/ Consensus.tla, PConProof.tla, VoteProof.tla (get rid of trailing whitespace)
• two_phase/TwoPhase.tla
• Allocator.tla

Specs that should just be deleted in favor of their tlaplus/examples counterparts

• ByzPaxos/BPConProof.tla
• paxos/Consensus.tla
• EWD840.tla
• LamportMutex.tla

Unsure how to integrate

• Bakery.tla, AtomicBakery.tla, AtomicBakeryWithoutSMT.tla
• paxos/Paxos.tla

Thoughts? Also, what's the deal with the examples_draft directory?