Unify pr/main workflows and use tlaplus/examples as integration tests

[ahelwer]

Simplified this PR to only use tlaplus/examples integration tests:

• PRs will use tlaplus/examples repo for integration testing
• Removed redundant running of test-fast-basic, which is run during make release

[ahelwer]

@kape1395 I'm getting this error when using the tlapm at _build/install/default/bin/tlapm:

specifications/TeachingConcurrency/Simple.tla
Checked proofs in 0.0s
FAILURE
Executable "zenon" not found in this PATH:
/opt/hostedtoolcache/opam/2.1.5/x86_64:/opt/hostedtoolcache/Python/3.11.6/x64/bin:/opt/hostedtoolcache/Python/3.11.6/x64:/home/runner/.local/bin:/opt/pipx_bin:/home/runner/.cargo/bin:/home/runner/.config/composer/vendor/bin:/usr/local/.ghcup/bin:/home/runner/.dotnet/tools:/snap/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games:/snap/bin:/home/runner/work/tlapm/tlapm/_build/default/src:/home/runner/work/tlapm/tlapm/_build/default/lib/tlaps/bin
 tlapm ending abnormally with (Failure
   "Executable \"zenon\" not found in this PATH:\
  \n/opt/hostedtoolcache/opam/2.1.5/x86_64:/opt/hostedtoolcache/Python/3.11.6/x64/bin:/opt/hostedtoolcache/Python/3.11.6/x64:/home/runner/.local/bin:/opt/pipx_bin:/home/runner/.cargo/bin:/home/runner/.config/composer/vendor/bin:/usr/local/.ghcup/bin:/home/runner/.dotnet/tools:/snap/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games:/snap/bin:/home/runner/work/tlapm/tlapm/_build/default/src:/home/runner/work/tlapm/tlapm/_build/default/lib/tlaps/bin\

Do you know what could be causing this? Why can't it find zenon?

[kape1395]

That's because you try to use the intermediate build files. These files have no proper locations for the provers.
After building TLAPM with make build install you can invoke it as opam exec -- tlapm instead of tlapm. This way you will use the version with the correct prover paths set already. Dune does that for the installed files (those in opam) and for running the project test cases).

[ahelwer]

Okay, so is the method of installation & execution of tlapm changed from this prerelease? https://github.com/tlaplus/tlapm/releases/tag/202210041448

How is the installer packaged now? What needs to be uploaded? Is it just the .tar.gz in the _build directory? How do you download & install that?

[kape1395]

Yes, that's changed. In the previous version, the release installer was actually an executable that builds Isabelle theories on installation, etc. Now all that is done while building a release, and the produced tar.gz is all you need. On my machine, after running make build release the file to upload is ./_build/tlaps-c72e177-dirty-x86_64-linux-gnu.tar.gz. If you need to use it in another git project / CI, just download it and extract it (tar -xzf ...) to a folder of your choice.

Maybe my previous comments were misleading; I thought you tried to run the TLAPM inside the TLAPM CI. There is no need to build the release, make build install is enough. But if you need to use the distributable file to download and use it, then the paragraph above should explain that.

[ahelwer]

This work is now ready for review, but the following issues need to be resolved before it can be merged:

1. Secrets need to be in place so upload to Inria nightly build server succeeds & tlaplus/examples CI trigger works
2. Existing bug currently in the main branch causing failing test needs to be fixed so CI will pass
3. The actual big issue, for some reason none of the proofs in tlaplus/examples are succeeding!!!

Separately, it may be worth asking whether it is really necessary to build & test tlaps with three different versions of ocaml (4.08.1, 4.13.0, 4.14.0) multiplied by the two supported platforms (linux & macos) on every CI run. Seems inefficient.

It's possible that the tlaplus/examples repo has some examples that are already run during tests of this repo. I will also look into this, they should be removed here to avoid redundancy.

[kape1395]

@ahelwer, regarding

The actual big issue, for some reason none of the proofs in tlaplus/examples are succeeding!!!

can you check if more checks are succeeding with branch lsp--updated_enabled_cdot at https://github.com/kape1395/tlapm/ ? That branch is not rebased on #55 yet.

[kape1395]

It's possible that the tlaplus/examples repo has some examples that are already run during tests of this repo. I will also look into this, they should be removed here to avoid redundancy.

Maybe some redundancy is OK? I think it would be good that the examples repo would have all the known examples. The tlapm repo might have them as test cases. But for a user it is natural to look for examples in a single place.

[ahelwer]

@kape1395 I reverted #55 but the tlaplus/examples checks are still failing unfortunately.

Separately, I see you merged support for ocaml 5.1.0. Should that be added to the list of ocaml versions used in the CI? Actually, should it replace all of them?

[kape1395]

In the LSP PR (#93), I rolled the versions to include 5.1.0 (https://github.com/tlaplus/tlapm/pull/93/files#diff-614df7545ae0c590d09c7d02f81aca54fe47524715e5e12fdbd3b9496eac51bcR8)
But I don't know what was the reason to build that on 3 versions; maybe others know.

From my side - I agree, maybe sticking with a single/latest ocaml version is enough. That would also simplify the LSP branch as the LSP server could be made non-optional. Now it builds only if ocaml-5.1.0 is there and optional libs are installed.

I tried to check a random file from the examples with the #93 version.

opam exec -- tlapm ./bcastByz/bcastByz.tla
> ...
> [INFO]: All 797 obligations proved.

Maybe we should look more precisely at what actually fails.

[kape1395]

Checked another case. It fails like that

opam exec -- tlapm specifications/ewd998/AsyncTerminationDetection_proof.tla

but works as

opam exec -- tlapm -I specifications/ewd998 AsyncTerminationDetection_proof.tla

[kape1395]

I found the script. It passes on my machine with the #95 (I made a mistake in the previous comments; I used #95, not #93 version).

$ python3 ./.github/scripts/check_proofs.py  --tlapm_path ~/.opam/5.1.0/ --manifest_path manifest.json 
specifications/LearnProofs/AddTwo.tla
Checked proofs in 0.2s
specifications/LearnProofs/FindHighest.tla
Checked proofs in 0.3s
specifications/LoopInvariance/BinarySearch.tla
Checked proofs in 6.3s
specifications/MisraReachability/ParReachProofs.tla
Checked proofs in 1.4s
specifications/MisraReachability/ReachableProofs.tla
Checked proofs in 5.4s
specifications/Paxos/Voting.tla
Checked proofs in 0.7s
specifications/PaxosHowToWinATuringAward/Voting.tla
Checked proofs in 0.7s
specifications/TeachingConcurrency/Simple.tla
Checked proofs in 0.3s
specifications/TeachingConcurrency/SimpleRegular.tla
Checked proofs in 5.3s
specifications/TwoPhase/TLAPS.tla
Checked proofs in 0.3s
specifications/TwoPhase/TwoPhase.tla
Checked proofs in 0.2s
specifications/ewd840/EWD840_proof.tla
Checked proofs in 0.6s
specifications/ewd840/TLAPS.tla
Checked proofs in 0.3s
specifications/ewd998/AsyncTerminationDetection_proof.tla
Checked proofs in 0.3s
specifications/lamport_mutex/TLAPS.tla
Checked proofs in 0.3s
specifications/sums_even/TLAPS.tla
Checked proofs in 0.1s
specifications/sums_even/sums_even.tla
Checked proofs in 0.2s
specifications/Majority/MajorityProof.tla
Checked proofs in 7.2s

[kape1395]

It also works like this:

$ tar -xzf tlaps-b0f6012-x86_64-linux-gnu.tar.gz 
$ python3 ./.github/scripts/check_proofs.py  --tlapm_path tlaps-b0f6012-x86_64-linux-gnu --manifest_path manifest.json 

Thus, the release is built correctly.

[ahelwer]

@kape1395 excellent! So I guess this PR is on hold until your #93 and #95 PRs both go in. Who do we harass to get those into main?

[damiendoligez]

From my side - I agree, maybe sticking with a single/latest ocaml version is enough.

I tend to agree with the idea of testing PRs on 5.1.0 only, but Debian Stable is still on OCaml 4.13.1, so it would be good to test with that, at least from time to time, to make sure we remain compatible with it.

[damiendoligez]

The actual big issue, for some reason none of the proofs in tlaplus/examples are succeeding!!!

Many of the failures are due to ptl_to_trp being installed in the wrong location. I have a fix at #99. @kape1395 could you have a look at that?

[ahelwer]

@damiendoligez @kape1395 the tlaplus/examples proofs almost all pass except for AsyncTerminationDetection_proof.tla, for an interesting reason. It looks like prior versions of TLAPS had an operator called ENABLEDrules defined, which the proof uses, but this latest version of TLAPS no longer defines that operator: https://github.com/tlaplus/Examples/blob/62d104f2e1cfd63b3f928342b8f634298706d145/specifications/ewd998/AsyncTerminationDetection_proof.tla#L96

[muenchnerkindl]

@ahelwer ENABLEDrules requires a build based on the updated_enabled_cdot branch. Is this the case here?

[ahelwer]

@muenchnerkindl This is just using the tlaplus/tlapm main branch head + these PR changes. Currently the tlaplus/examples CI uses this prerelease: https://github.com/tlaplus/tlapm/releases/tag/202210041448

[kape1395]

The updated_enabled_cdot merged with the current main can be found in this PR: #95.

[ahelwer]

Okay, what should be the sequence of events? Will that branch be merged to main in the near future? This PR can't be merged anyway until someone either puts in the needed secrets or gives me access so I can do it.

[ahelwer]

@kape1395 any idea why this build isn't succeeding?

[kape1395]

@ahelwer, I have updated the Isabelle build in #109. Hope that will make that part more stable and portable.

• I think this branch should be merged after the Isabelle branch, but there is a failing test. @muenchnerkindl should take a look at it.
• I guess that will be after Smt changes #70, which now looks like actively progressing.

[damiendoligez]

@ahelwer

Generate a new no-PIN SSH keypair, upload the public key to the authorized_keys file on the Inria server, and store the private key in the secrets.INRIA_SSH_PRIVKEY variable in this repo

I've generated the keypair and set the secret here, but I don't know under which user to install the public key on the Inria server.

[ahelwer]

@damiendoligez Could just create a new user called tlapmrelease or something that only has write access to that one directory where we want to upload the files

[lemmy]

@ahelwer

Generate a new no-PIN SSH keypair, upload the public key to the authorized_keys file on the Inria server, and store the private key in the secrets.INRIA_SSH_PRIVKEY variable in this repo

I've generated the keypair and set the secret here, but I don't know under which user to install the public key on the Inria server.

The CI of tlaplus/tlaplus already uploads as github to the INRIA machine: https://github.com/tlaplus/tlaplus/blob/d1504b6dc0ed35e3d4d343a3d380d0f4fe4980e9/.github/workflows/main.yml#L180

[ahelwer]

@kape1395 I simplified this PR so it just runs a subset of the proof specs in the tlaplus/examples repo. Quite a few failed so had to be skipped but at least this gives a baseline to work with and improve upon.