Hi Chun Tian,
It's hard to know exactly what's wrong, but I expect there's a bug in the
OpenTheory proof recording facility of HOL4, which is implemented in
src/opentheory/postbool/Logging.sml.
When you ask Holmake to generate an .ot.art file it first generates a raw
.art file by recording all the proofs (and definitions etc.) in the theory
directly, then it post-processes this .art file into the .ot.art file using
the external opentheory tool. The external tool might have a bug, or, more
likely, the original generated .art file is invalid. You can see the
semantics of .art files on the OpenTheory website here:
http://www.gilith.com/research/opentheory/article.html.
One way to debug this would be to edit Logging.sml so that whenever it
generates a "trans" line in the article, it first checks that the theorems
it just logged really have the correct shape, and print them out if not.
Another approach would be to try reading the generated .art file until it
fails with your own custom reader that can print more debugging information
(or maybe ask on the OpenTheory mailing list if the opentheory tool has
some options for printing more info). There is code for reading articles in
HOL4, under src/opentheory/postbool/Opentheory.sml.
I hope that helps. What are you planning to do with the recorded OpenTheory
packages when you get this to work?
If you send me as small an example as you can make of the failure, I may be
able to debug it. It might take me a while to find time for it though.
Cheers,
Ramana
On 25 April 2017 at 05:38, Chun Tian (binghe) <binghe.l...@gmail.com> wrote:
> Hi,
>
> I have created some formal theories which builds successfully in all HOL
> modes (stdknl, expk and logknl). But when I added the following lines into
> my Holmakefile:
>
> ifeq ($(KERNELID),otknl)
> all: $(patsubst %Script.sml,%.ot.art,$(wildcard *Script.sml))
> endif
>
> the building process failed strangely saying “terms not alpha-equivalent”
> ?! like this:
>
> CutFree.ot.art
> FAILED!
>
> FATAL ERROR: opentheory failed:
> error in file "CutFree.art" around line 77960:
> trans
> 10633
> def
> while executing trans command:
> terms not alpha-equivalent
> Lambek.ot.art
> M-KILLED
> make: *** [all] Error 1
>
> The issue happens when generating *.ot.art files from *.art files. Maybe
> it’s an issue in “opentheory” but HOL?
>
> But any way, does anyone have any idea on what’s going on? the *.art files
> are so long and each line is so short, it’s unreadable to me, thus I have
> no idea which of my theorems (at line 77960) caused the issue:
>
> def
> 10614
> ref
> appTerm
> 10631
> def
> betaConv
> 10632
> def
> trans
> 10633 <— line 77960
> def
> 10593
> ref
> 10599
> ref
> appTerm
> 10634
> def
> betaConv
>
> Regards,
>
> Chun Tian
>
>
>
> ------------------------------------------------------------
> ------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
