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
--
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.