Skip to content

Update GitHub Actions workflows to support multiple operating systems… #121

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
lemmy merged 3 commits into from
Mar 11, 2026
Merged

Update GitHub Actions workflows to support multiple operating systems… #121

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
130d1ea
Update GitHub Actions workflows to support multiple operating systems…
lemmy Mar 11, 2026
d040a42
Add Unix-specific tests and update build configuration for test execu…
lemmy Mar 11, 2026
6bbd75a
Update GitHub Actions workflows to use the new output syntax for sett…
lemmy Mar 11, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 16 additions & 9 deletions .github/workflows/main.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,11 +11,18 @@ on:
jobs:
build:

runs-on: ubuntu-latest
runs-on: ${{ matrix.os }}
strategy:
matrix:
os: [ubuntu-latest, macos-latest, windows-latest]
permissions:
contents: write # Required by actions/create-release@v1
packages: read


defaults:
run:
shell: bash

steps:
- uses: actions/checkout@v2
- name: Setup tmate session
Expand All @@ -25,12 +32,12 @@ jobs:
limit-access-to-actor: true
- name: Get current date
id: date
run: echo "::set-output name=date::$(date +'%Y%m%d%H%M')"
run: echo "date=$(date +'%Y%m%d%H%M')" >> "$GITHUB_OUTPUT"
- name: Build with Ant
run: ant -noinput -buildfile build.xml -Dtimestamp=${{steps.date.outputs.date}}
- name: Create Release
id: create_release
if: github.event_name == 'push'
if: github.event_name == 'push' && matrix.os == 'ubuntu-latest'
uses: actions/create-release@v1
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
Expand All @@ -41,7 +48,7 @@ jobs:
prerelease: false
- name: Upload Release Asset
id: upload-release-asset
if: github.event_name == 'push'
if: github.event_name == 'push' && matrix.os == 'ubuntu-latest'
uses: actions/upload-release-asset@v1.0.1
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
Expand All @@ -52,7 +59,7 @@ jobs:
asset_content_type: application/zip
- name: Upload dateless Release Asset
id: upload-dateless-release-asset
if: github.event_name == 'push'
if: github.event_name == 'push' && matrix.os == 'ubuntu-latest'
uses: actions/upload-release-asset@v1.0.1
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
Expand All @@ -63,7 +70,7 @@ jobs:
asset_content_type: application/zip
- name: Upload Release Asset
id: upload-release-asset-deps
if: github.event_name == 'push'
if: github.event_name == 'push' && matrix.os == 'ubuntu-latest'
uses: actions/upload-release-asset@v1.0.1
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
Expand All @@ -74,7 +81,7 @@ jobs:
asset_content_type: application/zip
- name: Upload dateless Release Asset
id: upload-dateless-release-asset-deps
if: github.event_name == 'push'
if: github.event_name == 'push' && matrix.os == 'ubuntu-latest'
uses: actions/upload-release-asset@v1.0.1
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
Expand All @@ -84,7 +91,7 @@ jobs:
asset_name: CommunityModules-deps.jar
asset_content_type: application/zip
- name: Repository Dispatch
if: github.event.client_payload.source != 'tlaplus'
if: github.event.client_payload.source != 'tlaplus' && matrix.os == 'ubuntu-latest'
uses: peter-evans/repository-dispatch@v3
with:
token: ${{ secrets.REPO_DISPATCH_TOKEN }}
Expand Down
13 changes: 10 additions & 3 deletions .github/workflows/pr.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,12 +6,19 @@ on:
jobs:
build:

runs-on: ubuntu-latest

runs-on: ${{ matrix.os }}
strategy:
matrix:
os: [ubuntu-latest, macos-latest, windows-latest]

defaults:
run:
shell: bash

steps:
- uses: actions/checkout@v2
- name: Get current date
id: date
run: echo "::set-output name=date::$(date +'%Y%m%d%H%M')"
run: echo "date=$(date +'%Y%m%d%H%M')" >> "$GITHUB_OUTPUT"
- name: Build with Ant
run: ant -noinput -buildfile build.xml -Dtimestamp=${{steps.date.outputs.date}}
10 changes: 9 additions & 1 deletion build.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -103,6 +103,12 @@
</target>

<target name="test" depends="dist" description="Run the modules in tests/ on the TLA+ modules in dist/">
<!-- On Unix, run AllTestsUnix which includes IOExec/shell tests; on Windows, run AllTests only. -->
<condition property="allTests" value="${basedir}/tests/AllTestsUnix">
<not><os family="windows"/></not>
</condition>
<property name="allTests" value="${basedir}/tests/AllTests"/>

<!-- If an assert fails, TLC will return a non-zero exit value which is makes the ant target fail. -->
<java classname="tlc2.TLC" fork="true" failonerror="true">
<!-- Tell Java to use a garbage collector which makes TLC happy. -->
Expand All @@ -121,7 +127,9 @@
<arg value="-metadir"/>
<arg value="${basedir}/build/states"/>
<arg value="-cleanup"/>
<arg value="${basedir}/tests/AllTests"/>
<arg value="-config"/>
<arg value="${basedir}/tests/AllTests.cfg"/>
<arg value="${allTests}"/>

<classpath>
<pathelement location="${tlc}/tla2tools.jar" />
Expand Down
9 changes: 9 additions & 0 deletions tests/AllTestsUnix.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
---------- MODULE AllTestsUnix -----------

(***************************************************)
(* Unix-only tests that depend on /bin/sh, bash, *)
(* cat, ls, echo, and Unix path conventions. *)
(***************************************************)
EXTENDS AllTests, IOUtilsUnixTests

===========================================
137 changes: 7 additions & 130 deletions tests/IOUtilsTests.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,76 +3,10 @@ EXTENDS IOUtils, TLC, TLCExt, Integers

ASSUME PrintT("IOUtilsTests!A")

\* Spaces and quotes should be passed directly to the program.
ASSUME(LET ret == IOExec(<<"echo", "'foo' ", " \"bar\"">>) IN /\ ret.exitValue = 0
/\ ret.stdout = "'foo' \"bar\"\n"
/\ ret.stderr = "")
\* Exit values and standard error should be returned properly.
ASSUME(LET ret == IOExec(<<"cat", "/does/not/exist">>) IN /\ ret.exitValue = 1
/\ ret.stdout = ""
/\ ret.stderr = "cat: /does/not/exist: No such file or directory\n")

\* Spaces and quotes should be passed directly to the program.
ASSUME(LET ret == IOExecTemplate(<<"bash", "-c", "echo %1$s %2$s">>, <<"foo", "bar">>)
IN /\ ret.exitValue = 0
/\ ret.stdout = "foo bar\n"
/\ ret.stderr = "")

\* Spaces and quotes should be passed directly to the program.
ASSUME(LET ret == IOExecTemplate(<<"echo", "'%1$s'", "\"%2$s\"">>, <<" foo", "bar ">>)
IN /\ ret.exitValue = 0
/\ ret.stdout = "' foo' \"bar \"\n"
/\ ret.stderr = "")

\* Exit values and standard error should be returned properly.
ASSUME(LET ret == IOExecTemplate(<<"cat", "/does/not/exist">>, <<>>)
IN /\ ret.exitValue = 1
/\ ret.stdout = ""
/\ ret.stderr = "cat: /does/not/exist: No such file or directory\n")

---------------------------------------------------------------------------------------------------------------------------

ASSUME PrintT("IOUtilsTests!B")

(***********************************************************************)
(* Check that environment variables work with IOUtils!IOExec operator: *)
(***********************************************************************)

\* SOME_TEST_ENV_VAR is set in Ant's build.xml file.

ASSUME(LET ret == IOExec(<<"/bin/sh", "-c", "echo $SOME_TEST_ENV_VAR">>)
IN /\ ret.exitValue = 0
/\ ret.stdout = "TLCFTW\n"
/\ ret.stderr = "")

ASSUME(LET ret == IOEnvExec([SOME_VAR_42 |-> "42"], <<"/bin/sh", "-c", "echo $SOME_VAR_42">>)
IN /\ ret.exitValue = 0
/\ ret.stdout = "42\n"
/\ ret.stderr = "")

ASSUME(LET ret == IOEnvExecTemplate([SOME_VAR_42 |-> "42"], <<"/bin/sh", "-c", "echo $SOME_VAR_42">>, <<>>)
IN /\ ret.exitValue = 0
/\ ret.stdout = "42\n"
/\ ret.stderr = "")

ASSUME(LET ret == IOEnvExecTemplate([SOME_VAR_42 |-> "42"], <<"/bin/sh", "-c", "echo $SOME_VAR_42">>, <<>>)
IN /\ ret.exitValue = 0
/\ ret.stdout = "42\n"
/\ ret.stderr = "")

ASSUME(LET ret == IOEnvExecTemplate([A |-> 1, B |-> 2], <<"/bin/sh", "-c", "echo $A $B">>, <<>>)
IN /\ ret.exitValue = 0
/\ ret.stdout = "1 2\n"
/\ ret.stderr = "")

ASSUME(LET ret == IOEnvExec(IOEnv, <<"/bin/sh", "-c", "echo $SOME_TEST_ENV_VAR">>)
IN /\ ret.exitValue = 0
/\ ret.stdout = "TLCFTW\n"
/\ ret.stderr = "")

\* Contrary to the /bin/sh -c echo $SOME_VAR technique above, the IOEnv operator does *not* append a dangling
\* newline to the value. Environment variable names made out of non-legal chars for TLA+ records can fall
\* back to ordinary function application.
\* The IOEnv operator does *not* append a dangling newline to the value (contrary to
\* reading env vars via /bin/sh -c echo). Environment variable names made out of
\* non-legal chars for TLA+ records can fall back to ordinary function application.

ASSUME(IOEnv.SOME_TEST_ENV_VAR = "TLCFTW")
ASSUME(IOEnv["SOME_TEST_ENV_VAR"] = "TLCFTW")
Expand Down Expand Up @@ -109,68 +43,11 @@ ASSUME(AssertEq(zeroPadN(0, 1), "0"))

---------------------------------------------------------------------------------------------------------------------------

ASSUME PrintT("IOUtilsTests!C")

(***********************************************************************)
(* Check that TLC can be launched through the IOUtils!IOExec operator: *)
(***********************************************************************)

\* Exit if tlc/tla2tools.jar doesn't exist. Since the tests are run with this tla2tools.jar, this assumption should hold.
ASSUME(LET ret == IOExec(<<"ls", "tlc/tla2tools.jar">>)
IN /\ ret.exitValue = 0
/\ ret.stdout = "tlc/tla2tools.jar\n"
/\ ret.stderr = "")

ASSUME PrintT("IOUtilsTests!C!b")

\* Run TLC without any parameters. TLC prints its version number, git commit, ... to stdout and sets RETVAL ($?) to 1.
ASSUME(LET ret == IOExec(<<"java", "-jar", "tlc/tla2tools.jar">>)
IN /\ PrintT(ret)
/\ ret.exitValue = 1
/\ ret.stderr = "")

ASSUME PrintT("IOUtilsTests!C!c")

\* Run TLC with some basic spec that passes.
ASSUME(LET ret == IOExec(<<"java", "-jar", "tlc/tla2tools.jar", "tests/nested/Counter">>)
IN /\ PrintT(ret)
/\ ret.exitValue = 0
/\ ret.stderr = "")

ASSUME PrintT("IOUtilsTests!C!d")

\* Run TLC with some spec depending on CommunityModules and CM on the classpath.
\* Pass an environment variable to the nested spec.
ASSUME(LET ret == IOEnvExec([SOME_NESTED_VAR |-> "SOME_VAL", B |-> "23"],
<<"java", "-cp", "modules:build/deps:build/modules:tlc/tla2tools.jar", "tlc2.TLC",
"-config", "Counter.cfg", "tests/nested/CounterCM">>)
IN /\ PrintT(ret)
/\ ret.exitValue = 0
/\ ret.stderr = "")

---------------------------------------------------------------------------------------------------------------------------

ASSUME PrintT("IOUtilsTests!D")

ASSUME PrintT("IOUtilsTests!D!A")

file == "/tmp/txt-serialize-test.txt"
payloadTXT == "Some text with \" escapes \" \\"

TXTSerializeResult == Serialize(payloadTXT, file, [format |-> "TXT", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "TRUNCATE_EXISTING">>])
ASSUME(LET ret == TXTSerializeResult IN /\ ret.exitValue = 0
/\ ret.stderr = "")

TXTDeserializeResult == Deserialize(file, [format |-> "TXT", charset |-> "UTF-8"])
ASSUME(LET ret == TXTDeserializeResult IN /\ ret.exitValue = 0
/\ ret.stdout = payloadTXT
/\ ret.stderr = "")

---------------------------------------------------------------------------------------------------------------------------
ASSUME PrintT("IOUtilsTests!B")

\* Simple round-trip test with a variety of different small structures

file2 == "/tmp/bin-serialize-test.vos"
file == "build/tests/bin-serialize-test.vos"
payloadBIN == <<
"foo",
{"bar"},
Expand All @@ -179,8 +56,8 @@ payloadBIN == <<
[x |-> 1, y |-> 2]
>>

ASSUME /\ IOSerialize(payloadBIN, file2, FALSE)
/\ LET value == IODeserialize(file2, FALSE)
ASSUME /\ IOSerialize(payloadBIN, file, FALSE)
/\ LET value == IODeserialize(file, FALSE)
IN value = payloadBIN

\* Test: can we read a string TLC has never encountered before?
Expand Down
Loading
Loading