[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] TLAPS 1.1.1 -- Unexpected error while checking proofs

Hi Marco,

I could not reproduce this error but wanted to confirm that you are using the Isabelle version that was shipped with the tlapm distribution (2011-1). Newer versions include changes that are not backward compatible.

Best regards,

On 21 August 2013 16:15, melver <marco...@xxxxxxxxx> wrote:

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 @@
     cleanup prob,
-    "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.