Hi Ramana, Thanks for your detailed explanation. For your question about what am I planning to do with the ot files, to be honest I have no plan. If I understand OpenTheory correctly, the theory I developed may be able to run in HOL light and Isabelle without full porting work, but currently I have no such need or interest at all.
So I’m going to find out which exact theorem caused the issue first, and move this theorem (I hope it’s just one) into a whole new script file, then try to find out which proof step caused the issue. In case I can isolate the issue, I’ll ask help here again. (otherwise it’s not worth wasting your valuable time looking into long proof scripts) Regards, Chun > Il giorno 25 apr 2017, alle ore 10:04, Ramana Kumar > <ramana.ku...@cl.cam.ac.uk> ha scritto: > > 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 > >
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ 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
