Isabelle2025

[muenchnerkindl]

This PR upgrades the Isabelle backend to Isabelle2025 and also fixes all proofs in the standard library of theorems. This also required a subtle change to the SMT backend contributed by @rozlynd.

[kape1395]

Several proofs fail, at least on my PC. Not sure if that's hardware or OS. I'm using Linux.

• tlapm/library/FunctionTheorems_proofs.tla

  Line 926 in 403f631

  <1>20. ASSUME NEW t \in S \cup {x} PROVE \E i \in 1..m+1 : G[i] = t

  - fails when checking from IDE, but passed when checked using tlapm directly (after cleaning cache).
• These fail from CLI as well:

  • tlapm/library/NaturalsInduction_proofs.tla

    Line 192 in 403f631

    <5>. QED BY <3>1, <4>2, <4>3, l-1 \in 0 .. k, m \in 0 .. l-2

  • tlapm/library/SequencesExtTheorems_proofs.tla

    Line 311 in 403f631

    <1>2. IsPrefix(s,t) <=> Len(s) <= Len(t) /\ s = SubSeq(t, 1, Len(s))

  • tlapm/library/SequencesExtTheorems_proofs.tla

    Line 323 in 403f631

    <1>1. IsStrictPrefix(s,t) => Len(s) < Len(t)

[muenchnerkindl]

Hmm, how can we debug this? I tried again, and all these proofs are checked on my end (admittedly on a quite fast Mac, but they don't even take long). Does the PM use a bundled version of Z3 or the one found locally, which could introduce another variation point? I'll try to get access to a Linux machine and see what happens.

[ahelwer]

Here's a result from my side, on Linux (old i7-4790k CPU from 2014):

1. git fetch origin
2. git checkout isabelle2025
3. git clean -dfx (deletes all files not checked into git)
4. make release
5. ./_build/tlapm/bin/tlapm --cleanfp library/FunctionTheorems_proofs.tla -> success
6. ./_build/tlapm/bin/tlapm --cleanfp --stretch 2 library/NaturalsInduction_proofs.tla -> failure (1/278 failed)
7. ./_build/tlapm/bin/tlapm --cleanfp --stretch 2 library/SequencesExtTheorems_proofs.tla -> failure (2/606 failed)

@muenchnerkindl if you would like me to set up a Linux VM in Azure for you I have some credits so can do that. Just send me your public SSH key to put in the ~/.ssh/authorized_keys file.

[lemmy]

Would it be possible to make the Github Action the source of truth?

[ahelwer]

I actually don't think the library proofs are checked in the CI, so yeah we could do that. They also fail on the main branch build for me.

[muenchnerkindl]

They also fail on the main branch build for me.

Yeah, that's why I (tried to) fix them. ;-)

[ahelwer]

That makes sense! Okay, I'll add the library proofs to the CI and comment out the ones that are failing. Then this PR can un-comment those proofs, and we will see whether they are fixed from the semi-objective perspective of the github CI.

[ahelwer]

Okay if you rebase this PR on the latest changes in main, you can get the CI to check specific library proofs by deleting these lines:

tlapm/.github/workflows/ci.yml

Lines 68 to 74 in 867b949

	-not -name "BagsTheorems_proofs.tla" \
	-and -not -name "FiniteSetTheorems_proofs.tla" \
	-and -not -name "FunctionTheorems_proofs.tla" \
	-and -not -name "NaturalsInduction_proofs.tla" \
	-and -not -name "SequenceTheorems_proofs.tla" \
	-and -not -name "SequencesExtTheorems_proofs.tla" \
	-and -not -name "WellFoundedInduction_proofs.tla" \

[muenchnerkindl]

Thanks @ahelwer! So I commented out the line for FunctionTheorems_proofs.tla but I don't see the CI running. Do I have to start it manually for the PR?

[ahelwer]

Ah, I wish github had better reporting for this but you have to check the repository Actions tab to see it:

invalid workflow file: .github/workflows/ci.yml#L63
You have an error in your yaml syntax on line 63

So I think you have to delete the line instead of commenting it out.

[muenchnerkindl]

OK, GitHub confirms that the proofs work on MacOS and fail on Linux. I even tried to decompose the failing proof, but still the same result. I'll install a local Linux box and continue testing there.

[kape1395]

Two steps were failing on my PC in SequencesExtTheorems_proofs.tla. I made a PR #220 fixing them.

[kape1395]

LGTM

[muenchnerkindl]

Thanks again @kape1395! I am quite disgusted by the fact that the behavior of Z3 differs significantly between OSes. Perhaps we should seriously compare with how cvc5 behaves.

@ahelwer, @lemmy: do you think we should leave the CI as it is, i.e. running all library proofs? They take quite a while on the GitHub servers, and I do not know how problematic this is.

[ahelwer]

The CI now takes 24 minutes instead of 18, which is not too bad. It's important for the library proofs to continue passing, I think? I will move the library checks later in the CI though so basic unit tests run first.

The Z3 version also has not been upgraded in a while, perhaps there are changes to its behavior (for better or worse here, who can say).