TLAPS 1.1.1 -- Unexpected error while checking proofs

[melver <marco...@xxxxxxxxx>]

Hi,

With the most recent version of TLAPS 1.1.1, while trying to verify
that everything works as expected, testing the binary distribution as well as when compiling from source, I run the command `tlapm -C -I +examples/cantor Cantor1.tla` and get the following output:

        (* loading fingerprints in "Cantor1.tlaps/fingerprints" *)
        (* created new "Cantor1.tlaps/Cantor1.thy" *)
        (* fingerprints written in "Cantor1.tlaps/fingerprints" *)
        Checking the proofs with Isabelle. This may take a long time.
        (* Isabelle parsing "Cantor1.tlaps/Cantor1.thy" ... done *)
        (* Obligation checking trace follows. *)
        (* *)
        Unexpected error while checking proofs.

`isabelle.log` shows the following output:

        *** Inner syntax error (line 17 of "/tmp/tlaps-1.1.1/tlapm/examples/Cantor1.tlaps/Cantor1.thy") at "<

        ***   1 > 1 )"

        *** Failed to parse proposition

I was able to fix one issue with the following patch, but the above syntax  error is still present:

diff -Naur tlaps-1.1.1/tlapm/src/backend/prep.ml tlaps-1.1.1-fix/tlapm/src/backend/prep.ml
--- tlaps-1.1.1/tlapm/src/backend/prep.ml	2012-11-22 11:47:58.000000000 +0000
+++ tlaps-1.1.1-fix/tlapm/src/backend/prep.ml	2013-05-03 23:33:36.003597833 +0100
@@ -425,7 +425,7 @@
     ["trivial"],
     prob,
     cleanup prob,
-    "using assms by safe",
+    "using assms by safe\n",
     [Types.Triv]
   end
 ;;

Regards,
Marco