From b0d16066a678ab7dce292d54104d9fd655214638 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 10 Oct 2024 08:09:16 +0200 Subject: [PATCH] Fix after switch to cmdliner - "--toolbox A B" becomes "--toolbox A,B" - "--isaprove" is deprecated and no longer supported --- lsp/lib/prover/prover.ml | 5 +++-- lsp/test/tlapm_mock.sh | 4 ++-- src/tlapm.t | 2 +- test/README | 2 +- test/TOOLS/do_junit_tests | 2 +- test/TOOLS/do_one_test | 2 +- test/TOOLS/do_soundness_tests | 2 +- test/fast/basic/nonexistent_test.tla | 2 +- test/fast/enabled_cdot/Level_of_parametric_INSTANCE_test.tla | 2 +- .../fast/fingerprint/FingerprintVariablesParameters_test.tla | 4 ++-- test/fast/fingerprint/load_v8_test.tla.disabled | 2 +- test/fast/fingerprint/load_v8old_test.tla.disabled | 2 +- test/fast/fingerprint/load_v9_test.tla.disabled | 2 +- .../language/INSTANCE_shift_due_to_omitted_modunits_test.tla | 2 +- test/fast/regression/z3_fingerprint_test.tla | 4 ++-- test/regression_tests/fingerprint_13_12_07_test-disabled.tla | 2 +- 16 files changed, 21 insertions(+), 20 deletions(-) diff --git a/lsp/lib/prover/prover.ml b/lsp/lib/prover/prover.ml index dfc7f4bb..7e7ec7e4 100644 --- a/lsp/lib/prover/prover.ml +++ b/lsp/lib/prover/prover.ml @@ -122,8 +122,9 @@ let start_async_with_exec st doc_uri doc_text range paths events_adder (* First arg s ignored, if executable is specified. *) executable; "--toolbox"; - string_of_int (Range.line_from range); - string_of_int (Range.line_till range); + Printf.sprintf "%d,%d" + (Range.line_from range) + (Range.line_till range); "--toolbox-vsn"; "2"; (* "--verbose"; *) diff --git a/lsp/test/tlapm_mock.sh b/lsp/test/tlapm_mock.sh index 6d8e60d6..9bdba357 100755 --- a/lsp/test/tlapm_mock.sh +++ b/lsp/test/tlapm_mock.sh @@ -45,7 +45,7 @@ function Empty() { cat << EOF \* TLAPM version 1.5.0 \* launched at 2023-09-30 23:39:35 with command line: -\* tlapm --toolbox 0 0 Empty.tla +\* tlapm --toolbox 0,0 Empty.tla @!!BEGIN @!!type:obligationsnumber @@ -64,7 +64,7 @@ function Some() { cat << EOF \* TLAPM version 1.5.0 \* launched at 2023-09-30 23:43:15 with command line: -\* tlapm --toolbox 0 0 Some.tla +\* tlapm --toolbox 0,0 Some.tla (* loading fingerprints in ".tlacache/Some.tlaps/fingerprints" *) @!!BEGIN diff --git a/src/tlapm.t b/src/tlapm.t index c44345eb..c9ae2e92 100644 --- a/src/tlapm.t +++ b/src/tlapm.t @@ -1,5 +1,5 @@ Test the --stdin option - $ cat <&1 | grep -e '^@!!' | grep -v 'time-used') + $ cat <&1 | grep -e '^@!!' | grep -v 'time-used') > ---- MODULE A ---- > THEOREM > ASSUME diff --git a/test/README b/test/README index 4136b30b..8e61451a 100644 --- a/test/README +++ b/test/README @@ -23,7 +23,7 @@ line of ==== are the commands for the test harness: with the "results" clause. The standard outputs and standard error outputs of the commands are all concatenated in execution order. If this clause is omitted, the default command is executed: - ${TLAPM} --toolbox 0 0 --nofp ${FILE} --stretch ${STRETCH} + ${TLAPM} --toolbox 0,0 --nofp ${FILE} --stretch ${STRETCH} - stretch: Changes the STRETCH parameter to . This should only be used for diff --git a/test/TOOLS/do_junit_tests b/test/TOOLS/do_junit_tests index deb3941e..8892a931 100755 --- a/test/TOOLS/do_junit_tests +++ b/test/TOOLS/do_junit_tests @@ -38,7 +38,7 @@ outf=/var/tmp/ju$$.txt FILE="`basename $f`" DIR="`dirname $f`" - cmd="cd $DIR; ${TLAPM} --toolbox 0 0 --nofp $FILE" + cmd="cd $DIR; ${TLAPM} --toolbox 0,0 --nofp $FILE" echo "" | tee -a $outf echo "+++ Running case: $FILE " | tee -a $outf echo "+++ working dir: "`pwd` | tee -a $outf diff --git a/test/TOOLS/do_one_test b/test/TOOLS/do_one_test index f0c45445..2c39139f 100755 --- a/test/TOOLS/do_one_test +++ b/test/TOOLS/do_one_test @@ -119,7 +119,7 @@ phase == 1 && FILENAME ~ /.*\/separator$/ { result = system (check_command); if (result != 0){ fail("explicit check failed"); } }else if (!command_done){ - run_command("${TLAPM} --toolbox 0 0 --nofp ${FILE} --stretch ${STRETCH} --debug=tempfiles "); + run_command("${TLAPM} --toolbox 0,0 --nofp ${FILE} --stretch ${STRETCH} --debug=tempfiles "); } if (result_code != expected_result){ fail("wrong result code"); diff --git a/test/TOOLS/do_soundness_tests b/test/TOOLS/do_soundness_tests index ce44850b..853e7a89 100755 --- a/test/TOOLS/do_soundness_tests +++ b/test/TOOLS/do_soundness_tests @@ -38,7 +38,7 @@ outf=/var/tmp/ju$$.txt FILE="`basename $f`" DIR="`dirname $f`" - cmd="cd $DIR; ${TLAPM} --toolbox 0 0 --nofp $FILE" + cmd="cd $DIR; ${TLAPM} --toolbox 0,0 --nofp $FILE" echo "" | tee -a $outf echo "+++ Running case: $FILE " | tee -a $outf echo "+++ working dir: "`pwd` | tee -a $outf diff --git a/test/fast/basic/nonexistent_test.tla b/test/fast/basic/nonexistent_test.tla index 6e5a848f..da214f5e 100644 --- a/test/fast/basic/nonexistent_test.tla +++ b/test/fast/basic/nonexistent_test.tla @@ -12,6 +12,6 @@ to the filename (filepath). THEOREM FALSE OBVIOUS ================================= -command: ${TLAPM} --toolbox 0 0 nonexistent_test +command: ${TLAPM} --toolbox 0,0 nonexistent_test stderr: obligation failed. diff --git a/test/fast/enabled_cdot/Level_of_parametric_INSTANCE_test.tla b/test/fast/enabled_cdot/Level_of_parametric_INSTANCE_test.tla index dd959793..e0fabbe1 100644 --- a/test/fast/enabled_cdot/Level_of_parametric_INSTANCE_test.tla +++ b/test/fast/enabled_cdot/Level_of_parametric_INSTANCE_test.tla @@ -27,5 +27,5 @@ THEOREM TRUE <1> QED ================================================== -command: ${TLAPM} --nofp --toolbox 0 0 ${FILE} +command: ${TLAPM} --nofp --toolbox 0,0 ${FILE} nostderr: ending abnormally diff --git a/test/fast/fingerprint/FingerprintVariablesParameters_test.tla b/test/fast/fingerprint/FingerprintVariablesParameters_test.tla index 32b8348d..671fe9bd 100644 --- a/test/fast/fingerprint/FingerprintVariablesParameters_test.tla +++ b/test/fast/fingerprint/FingerprintVariablesParameters_test.tla @@ -19,7 +19,7 @@ THEOREM \E y: y # y OBVIOUS ==================================== -command: ${TLAPM} --toolbox 0 0 ${FILE} +command: ${TLAPM} --toolbox 0,0 ${FILE} stderr: 1/2 obligations failed -command: ${TLAPM} --toolbox 0 0 ${FILE} +command: ${TLAPM} --toolbox 0,0 ${FILE} stderr: 1/2 obligations failed diff --git a/test/fast/fingerprint/load_v8_test.tla.disabled b/test/fast/fingerprint/load_v8_test.tla.disabled index 3ceb79dd..d6340c6c 100644 --- a/test/fast/fingerprint/load_v8_test.tla.disabled +++ b/test/fast/fingerprint/load_v8_test.tla.disabled @@ -27,7 +27,7 @@ THEOREM cantor == =============================================== command: rm -rf load_v8_test.tlaps command: cp -r load_v8_test.tlaps.testbase load_v8_test.tlaps -command: ${TLAPM} --toolbox 0 0 --isaprove ${FILE} +command: ${TLAPM} --toolbox 0,0 ${FILE} stdout: fingerprints written stderr: Translating fingerprints from version 8 stderr: already:true diff --git a/test/fast/fingerprint/load_v8old_test.tla.disabled b/test/fast/fingerprint/load_v8old_test.tla.disabled index 8a18e425..fa76d24d 100644 --- a/test/fast/fingerprint/load_v8old_test.tla.disabled +++ b/test/fast/fingerprint/load_v8old_test.tla.disabled @@ -127,7 +127,7 @@ OBVIOUS command: rm -rf .tlacache command: mkdir .tlacache command: cp -r load_v8old_test.tlaps.testbase .tlacache/load_v8old_test.tlaps -command: ${TLAPM} --toolbox 0 0 --isaprove ${FILE} +command: ${TLAPM} --toolbox 0,0 ${FILE} stdout: fingerprints written stderr: Translating fingerprints from version 8 stderr: already:true diff --git a/test/fast/fingerprint/load_v9_test.tla.disabled b/test/fast/fingerprint/load_v9_test.tla.disabled index 3a75958d..ffc14d38 100644 --- a/test/fast/fingerprint/load_v9_test.tla.disabled +++ b/test/fast/fingerprint/load_v9_test.tla.disabled @@ -27,7 +27,7 @@ THEOREM cantor == =============================================== command: rm -rf load_v9_test.tlaps command: cp -r load_v9_test.tlaps.testbase load_v9_test.tlaps -command: ${TLAPM} --toolbox 0 0 --isaprove ${FILE} +command: ${TLAPM} --toolbox 0,0 ${FILE} stdout: fingerprints written stderr: Translating fingerprints from version 9 stderr: already:true diff --git a/test/fast/language/INSTANCE_shift_due_to_omitted_modunits_test.tla b/test/fast/language/INSTANCE_shift_due_to_omitted_modunits_test.tla index a83b24d4..aa8ef138 100644 --- a/test/fast/language/INSTANCE_shift_due_to_omitted_modunits_test.tla +++ b/test/fast/language/INSTANCE_shift_due_to_omitted_modunits_test.tla @@ -25,5 +25,5 @@ OBVIOUS ============================================================ -command: ${TLAPM} --toolbox 0 0 ${FILE} +command: ${TLAPM} --toolbox 0,0 ${FILE} nostderr: Assertion failed diff --git a/test/fast/regression/z3_fingerprint_test.tla b/test/fast/regression/z3_fingerprint_test.tla index 45bfc991..75eaefe6 100644 --- a/test/fast/regression/z3_fingerprint_test.tla +++ b/test/fast/regression/z3_fingerprint_test.tla @@ -5,6 +5,6 @@ EXTENDS TLAPS, Naturals THEOREM foo == 2 + 2 = 4 BY Z3 ==== -command: ${TLAPM} --toolbox 0 0 --isaprove ${FILE} 2>/dev/null -command: ${TLAPM} --toolbox 0 0 --noproving ${FILE} +command: ${TLAPM} --toolbox 0,0 ${FILE} +command: ${TLAPM} --toolbox 0,0 --noproving ${FILE} stderr: already:true diff --git a/test/regression_tests/fingerprint_13_12_07_test-disabled.tla b/test/regression_tests/fingerprint_13_12_07_test-disabled.tla index ab4f22cc..4c85ac10 100644 --- a/test/regression_tests/fingerprint_13_12_07_test-disabled.tla +++ b/test/regression_tests/fingerprint_13_12_07_test-disabled.tla @@ -11,5 +11,5 @@ OBVIOUS THEOREM S # {} OBVIOUS ==== -command: ${TLAPM} --toolbox 0 0 --threads 1 --cleanfp ${FILE} +command: ${TLAPM} --toolbox 0,0 --threads 1 --cleanfp ${FILE} stderr: status:failed