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