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

Hi Marco,

I am a bit confused now. Checking all proof obligations (-C) is the recommended way to verify the installation according to http://tla.msr-inria.inria.fr/tlaps/content/Download/Source.html.

This recommendation is out of date. We will remove it soon.

In addition I also noticed that the binary distribution runs `tlapm -C -I +examples/cantor Cantor1.tla` for the self-test ("Performing a self-test..."), however, the exit code is 0 even if tlapm fails, which will cause the self-test to never report failure.

This is a bug in the test. We will fix it in the next version (not the upcoming one which will be released in the next few days).

Thank you for your report and information,
best regards,
Tomer

On Friday, 23 August 2013 14:16:12 UTC+1, shaolintl wrote:
> Hi Macro,
>
> The -C option is not well tested but the problem seems not to occur in the current build of the prover. We will release the next version soon but if you want access to the development files, this can be arranged.
>
>
>
> Best regards,
> Tomer
>
>
>
>

> On 23 August 2013 14:35, <marc...@xxxxxxxxx> wrote:
>
>
> 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.
>
>
>
> --
>
> 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.

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