Fix after switch to cmdliner

- "--toolbox A B" becomes "--toolbox A,B"
- "--isaprove" is deprecated and no longer supported

Author: Stephane Glondu

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"; *)

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

src/tlapm.t

@@ -1,5 +1,5 @@
 Test the --stdin option
-  $ cat <<EOF | (tlapm --toolbox 0 0 --stdin A.tla 2>&1 | grep -e '^@!!' | grep -v 'time-used')
+  $ cat <<EOF | (tlapm --toolbox 0,0 --stdin A.tla 2>&1 | grep -e '^@!!' | grep -v 'time-used')
   > ---- MODULE A ----
   > THEOREM
   >   ASSUME

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: <n>
   Changes the STRETCH parameter to <n>. This should only be used for

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

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");

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

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.
 

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

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

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

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

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

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

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

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