Add SANY as a parser backend option

.github/workflows/ci.yml

@@ -106,5 +106,23 @@ jobs:
                   | map(.path + "\u0000")
                   | join("")' \
                 | xargs --verbose --null --no-run-if-empty -I {TLA_FILE} \
-                time "$DEPS_DIR/tlapm-install/bin/tlapm" "$EXAMPLES_DIR/{TLA_FILE}" -I "$DEPS_DIR/community" --stretch 5
+                time "$DEPS_DIR/tlapm-install/bin/tlapm" --cleanfp "$EXAMPLES_DIR/{TLA_FILE}" -I "$DEPS_DIR/community" --stretch 5
+            - name: SANY backend examples test
+              run: |
+                find "$EXAMPLES_DIR/specifications" -iname "manifest.json" -print0 \
+                | xargs --null --no-run-if-empty \
+                jq --join-output '
+                  .modules
+                  | map(select(has("proof")))
+                  # Failing on Linux
+                  | map(select(.path != "specifications/LoopInvariance/SumSequence.tla"))
+                  # Failing in SANY due to subexpression usage
+                  | map(select(.path != "specifications/ewd840/EWD840_proof.tla"))
+                  | map(select(.path != "specifications/byzpaxos/PConProof.tla"))
+                  # Skip checking long-running proofs
+                  | map(select(.proof.maxRuntimeMinutes <= 1))
+                  | map(.path + "\u0000")
+                  | join("")' \
+                | xargs --verbose --null --no-run-if-empty -I {TLA_FILE} \
+                time "$DEPS_DIR/tlapm-install/bin/tlapm" --cleanfp --parser SANY "$EXAMPLES_DIR/{TLA_FILE}" -I "$DEPS_DIR/community" --stretch 5
 

deps/tla2tools.jar/Makefile

@@ -0,0 +1,11 @@
+TLA_TOOLS_JAR_URL=https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar
+
+tla2tools.jar:
+	wget --progress=dot:giga $(TLA_TOOLS_JAR_URL)
+
+clean:
+	rm -f tla2tools.jar
+
+sany: tla2tools.jar
+
+.PHONY: sany clean

deps/tla2tools.jar/dune

@@ -0,0 +1,9 @@
+; Download SANY
+(rule
+ (deps "Makefile")
+ (targets tla2tools.jar)
+ (action (run "make" "-C" "." "sany")))
+
+(install
+ (section (site (tlapm backends)))
+ (files (tla2tools.jar as bin/tla2tools.jar)))

dune-project

@@ -51,6 +51,7 @@
   ppx_inline_test
   ppx_assert
   ppx_deriving
+  xmlm
   (ounit2 :with-test)
   (alcotest :with-test)
   (ocolor :with-test)

src/dune

@@ -22,6 +22,7 @@
   dune-site
   dune-build-info
   camlzip ; main deps.
+  xmlm
   sexplib)
  ; for inline tests only (ppx_assert).
  (foreign_stubs

src/params.ml

@@ -56,6 +56,11 @@ let prefer_stdlib = ref false
 (* If set to true, the TLAPM will prefer the modules from the STDLIB
    instead of modules with the same names in the search path. *)
 
+type parser = | Tlapm | Sany
+let parser_backend = ref Tlapm
+
+let module_jar_paths = ref []
+
 let noproving = ref false (* Don't send any obligation to the back-ends. *)
 
 let printallobs = ref false

src/params.mli

@@ -7,6 +7,9 @@ val toolbox: bool ref
 val toolbox_vsn: int ref
 val use_stdin: bool ref
 val prefer_stdlib: bool ref
+type parser = | Tlapm | Sany
+val parser_backend: parser ref
+val module_jar_paths : string list ref
 
 (* expr/fmt.ml *)
 val debugging: string -> bool

src/paths.ml

@@ -15,15 +15,25 @@ let backend_paths =
 let stdlib_paths =
   site_paths Setup_paths.Sites.stdlib [ "lib"; "tlapm"; "stdlib" ]
 
+let backend_path_elems =
+  let site_bin bs = Filename.concat bs "bin" in
+  let site_isa bs = List.fold_left Filename.concat bs [ "Isabelle"; "bin" ] in
+  let site_paths bs = [ site_bin bs; site_isa bs ] in
+  List.concat (List.map site_paths backend_paths)
+
 (** If the backends site is not available ([]), then look for executables in the PATH,
       otherwise we are in the dune-based build and should look for the backends in the
       specified site locations. *)
 let backend_path_string =
-  let site_bin bs = Filename.concat bs "bin" in
-  let site_isa bs = List.fold_left Filename.concat bs [ "Isabelle"; "bin" ] in
-  let site_paths bs = [ site_bin bs; site_isa bs ] in
-  let path_elems = List.concat (List.map site_paths backend_paths) in
-  Printf.sprintf "%s:%s" (String.concat ":" path_elems) (Sys.getenv "PATH")
+  let paths = String.concat ":" backend_path_elems in
+  try Printf.sprintf "%s:%s" paths (Sys.getenv "PATH")
+  with Not_found -> paths
+
+
+let backend_classpath_string jar_file =
+  let classpath = List.map (fun path -> Filename.concat path jar_file) backend_path_elems |> String.concat ":" in
+  try Printf.sprintf "%s:%s" classpath (Sys.getenv "CLASSPATH")
+  with Not_found -> classpath
 
 let find_path_containing paths file =
   let find_actual path = Sys.file_exists (Filename.concat path file) in

src/paths.mli

@@ -1,4 +1,5 @@
 val backend_path_string : string
+val backend_classpath_string : string -> string
 val backend_paths : string list
 val stdlib_paths : string list
 val find_path_containing : string list -> string -> string option