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 @@
- "using assms by safe",
+ "using assms by safe\n",
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/groups/opt_out.