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

[marco...@xxxxxxxxx]

Yes, the Isabelle version is 2011. The error can also be reproduced using the binary distribution on the TLAPS website, which includes all dependencies, including Isabelle 2011.

On Friday, 23 August 2013 10:01:32 UTC+1, shaolintl  wrote:
> 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,
> Tomer
> 
> 
> 
> 
> 
> 
> 
> On 21 August 2013 16:15, melver <marc...@xxxxxxxxx> wrote:
> 
> 
> 
> 
> 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 tlaplu...@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.