Karolis Petrauskas
Karolis Petrauskas
Do you know if there is any progress on this? I want to work on the TLAPS integration this summer and wonder if that overlaps with others.
From the build perspective. The current tests in TLAPS depend on the files in the standard library, including the `Functions.tla`. E.g. `./test/fast/regression/consensus/consensus_test.tla` -> `FiniteSetTheorems` -> `Functions`. But I haven't checked...
The same problem with the `ivy` command here.
I agree with this. Also, if the releasing process changes, can we avoid releases if no new commits are on the main branch? Currently, each day, I get notifications on...
@lemmy, my account Karolis Petrauskas ([email protected]) User Id : 336ed76d-ac43-6c31-9b7e-079e407795b1
I noticed that VSCode complains about the extension ID: 
#84 is merged now. Can we close this issue?
@muenchnerkindl, all the tests are passing with this Isabelle version. What do you think about merging it into #109 ?
The TLAPS now works with the Isabelle2024-RC2, so I checked if the failures to prove some statements are still here (as in #109). And the problems are still here. I...
Indeed, in Isabelle2023, your lemma is proved by `auto`, but fails if `assumes "f(S) = 0"` is uncommented. It also passes if this useless assumption is moved to be the...