[opentheory-users] Debugging a failing trans

[Joe Leslie-Hurd]

Hi Ramana,

If you compile the development version of the opentheory tool

https://github.com/gilith/opentheory

and use it to process the article file, you get a lot more error
information including these last few lines:

different constants at path 10110 subterms: HOL4.min.@ vs HOL4.min.
different constants: HOL4.min.@ vs HOL4.min.
different constant names

So it looks like there are different constants at subterm path 10110.

Cheers,

Joe

On Wed, Apr 26, 2017 at 2:22 PM, Ramana Kumar <ramana at member.fsf.org> wrote:
> Hi OpenTheory list,
>
> I am trying to find out more about why an article file I generated causes
> opentheory to fail. It prints this error:
>
>  FATAL ERROR: opentheory failed:
>  error in file "Test.art" around line 37270:
>  trans
>  5016
>  def
>  while executing trans command:
>  terms not alpha-equivalent
>
> So obviously the trans command failed. But my attempts to figure out which
> theorems are being "trans"ed at that point (I made the article generator add
> comments) turned up theorems that looked OK. So, is it possible to ask the
> opentheory tool to give more information about the failing theorems? Can it
> print them out?
>
> The failing article can be found (for now) at
> https://hol-theorem-prover.org/Test.art.
>
> Cheers,
> Ramana
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>