diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 6b405e6..e809104 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -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 @@ -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 }} @@ -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 }} @@ -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 }} @@ -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 }} @@ -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 }} @@ -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 }} diff --git a/.github/workflows/pr.yml b/.github/workflows/pr.yml index bc3d170..bb3f716 100644 --- a/.github/workflows/pr.yml +++ b/.github/workflows/pr.yml @@ -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}} diff --git a/build.xml b/build.xml index f7d3123..ec19905 100644 --- a/build.xml +++ b/build.xml @@ -103,6 +103,12 @@ + + + + + + @@ -121,7 +127,9 @@ - + + + diff --git a/tests/AllTestsUnix.tla b/tests/AllTestsUnix.tla new file mode 100644 index 0000000..7827199 --- /dev/null +++ b/tests/AllTestsUnix.tla @@ -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 + +=========================================== diff --git a/tests/IOUtilsTests.tla b/tests/IOUtilsTests.tla index 6dbe2b0..1f3e86c 100644 --- a/tests/IOUtilsTests.tla +++ b/tests/IOUtilsTests.tla @@ -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") @@ -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"}, @@ -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? diff --git a/tests/IOUtilsUnixTests.tla b/tests/IOUtilsUnixTests.tla new file mode 100644 index 0000000..d55fb4a --- /dev/null +++ b/tests/IOUtilsUnixTests.tla @@ -0,0 +1,125 @@ +-------------------------- MODULE IOUtilsUnixTests -------------------------- +EXTENDS IOUtils, TLC, TLCExt, Integers + +ASSUME PrintT("IOUtilsUnixTests!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("IOUtilsUnixTests!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([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 = "") + +--------------------------------------------------------------------------------------------------------------------------- + +ASSUME PrintT("IOUtilsUnixTests!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("IOUtilsUnixTests!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("IOUtilsUnixTests!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("IOUtilsUnixTests!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("IOUtilsUnixTests!D") + +txtFile == "/tmp/txt-serialize-test.txt" +payloadTXT == "Some text with \" escapes \" \\" + +TXTSerializeResult == Serialize(payloadTXT, txtFile, [format |-> "TXT", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "TRUNCATE_EXISTING">>]) +ASSUME(LET ret == TXTSerializeResult IN /\ ret.exitValue = 0 + /\ ret.stderr = "") + +TXTDeserializeResult == Deserialize(txtFile, [format |-> "TXT", charset |-> "UTF-8"]) +ASSUME(LET ret == TXTDeserializeResult IN /\ ret.exitValue = 0 + /\ ret.stdout = payloadTXT + /\ ret.stderr = "") + +=============================================================================