[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
TLAPS 1.1.1 -- Unexpected error while checking proofs
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",