search

tlaplus / tlapm

The TLA Proof Manager
https://proofs.tlapl.us/
BSD 2-Clause "Simplified" License
62 stars 20 forks source link

Verify proofs in examples/ directory as part of PR workflow #136

Open lemmy opened 3 months ago

lemmy commented 3 months ago

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 commented 3 months ago

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 commented 3 months ago

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

muenchnerkindl commented 3 months ago

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 commented 3 months ago

Sounds like a good way to go.

lemmy commented 3 months ago

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 commented 2 months ago

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

Specs that should overwrite those in tlaplus/examples

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

Unsure how to integrate

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