CI workflow fails on ubuntu about examples

[ahelwer]

There's an option in the workflow to re-run it. Looks like an issue with the TLAPS install, so probably there is some rare instance where the installation step fails nondeterministically. Here is the error message:

2023-07-12 12:42:09 (159 MB/s) - ‘tlaps-1.5.0-x86_64-linux-gnu-inst.bin’ saved [151669984/151669984]

Installing the TLA+ Proof System

    Version: 1.5.0
Destination: /home/runner/work/Examples/Examples/deps/tlapm-install

Extracting ... done.
Compiling Isabelle theories.
Building Pure ...
Pure FAILED
(see also /home/runner/work/Examples/Examples/deps/tlapm-install/lib/tlaps/heaps/polyml-5.4.0_x86_64-linux/log/Pure)

   xml_of_proof (PBound i) = XML.Elem ((...), ...) |
      xml_of_proof (... ...) = XML.Elem (...) |
      xml_of_proof ... = ... ... |
      xml_of_proof ... = ... |
      ...
At (line 57 of "Tools/xml_syntax.ML")
structure XML_Syntax : XML_SYNTAX
val it = (): unit
poly: scanaddrs.cpp:107: PolyWord ScanAddress::ScanStackAddress(PolyWord, StackObject*, bool): Assertion `val.IsDataPtr()' failed.
make: *** [IsaMakefile:262: /home/runner/work/Examples/Examples/deps/tlapm-install/lib/tlaps/heaps/polyml-5.4.0_x86_64-linux/Pure] Error 134
/home/runner/work/Examples/Examples/deps/tlapm-install/lib/tlaps/Isabelle2011-1/lib/scripts/run-polyml: line 77:  1847 Aborted                 (core dumped) "$POLY" -q $ML_OPTIONS
FATAL ERROR: Could not compile Isabelle/Pure


    *** ABORT ***.
Error: Process completed with exit code 2.

[lemmy]

TLAPS apparently also has an install failure on Windows, which causes the last two CI runs to fail:

...

2023-07-22 06:53:02 (13.9 MB/s) - ‘202210041448.tar.gz’ saved [11231483]

tar: tlapm-202210041448/zenon/regression/examples/data/TLAPS.tla: Cannot change mode to rwxr-xr-x: Not a directory
tar: Exiting with failure status due to previous errors
Error: Process completed with exit code 2.

[ahelwer]

That might be an issue with tar as packaged by msys2, will take a look.

[ahelwer]

@lemmy looks like your latest changes broke the workflow?

[lemmy]

EWD998Small.cfg finished in 24s on my machine, which is within the 30s timeout. Do I just increment the timeout?

[ahelwer]

There are actually two issues:

1. In Windows CI, EWD998Small.cfg hit hard timeout; the timeout is 60 seconds as set here. On both macOS and Linux it finished in 27 seconds. Maybe this is transient/nondeterministic or it runs differently on windows?
2. On macOS and Linux there is an error when smoke-testing large models where model specifications/ewd998/EWD998ChanID.cfg expected error code 0 but got 11 (deadlock failure). So maybe you need to add "ignore deadlock" to its config in the manifest?

[ahelwer]

Recommend closing this in favor of tlaplus/tlapm#88