Hi again, The issue happens because of the following mini theory with just one datatype definition:
open HolKernel Parse boolLib bossLib; val _ = new_theory "Test”; val _ = Datatype `Dertree = Der 'a (Dertree list)`; val _ = export_theory (); Error outputs: FATAL ERROR: opentheory failed: error in file "Test.art" around line 37270: trans 5016 def while executing trans command: terms not alpha-equivalent Regards, Chun Tian > Il giorno 25 apr 2017, alle ore 18:50, Chun Tian (binghe) > <binghe.l...@gmail.com> ha scritto: > > 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
