Thanks Chun Tian,
I can reproduce the issue.
I tried finding out which theorems were causing the failure. They're rather
ugly (I will paste at the end of this email), but they look like valid
inputs to the "trans" function to me. It could be something to do with the
fact that some of the constants have been deleted, but I don't know why
this would make a difference to OpenTheory, which never deletes anything.
So maybe we should ask on the OpenTheory mailing list and supply the
Test.art file?
first argument to trans:
#|- (∃abs.
# (∀a. abs (Test$old1->@temp @ind_typeTest7<-old a) = a) ∧
# ∀r.
# (λa1'.
# ∀'Dertree' '@temp @ind_typeTest0list' .
# (∀a0'.
# (∃a0 a1.
# (a0' =
# (λa0 a1.
# ind_type$CONSTR 0 a0
# (ind_type$FCONS a1 (λn. ind_type$BOTTOM))) a0
# a1) ∧ '@temp @ind_typeTest0list' a1) ⇒
# 'Dertree' a0') ∧
# (∀a1'.
# (a1' =
# ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM)) ∨
# (∃a0 a1.
# (a1' =
# (λa0 a1.
# ind_type$CONSTR (SUC (SUC 0)) ARB
# (ind_type$FCONS a0
# (ind_type$FCONS a1 (λn. ind_type$BOTTOM))))
# a0 a1) ∧ 'Dertree' a0 ∧
# '@temp @ind_typeTest0list' a1) ⇒
# '@temp @ind_typeTest0list' a1') ⇒
# '@temp @ind_typeTest0list' a1') r ⇔
# (Test$old1->@temp @ind_typeTest7<-old (abs r) = r)) ⇔
# (λP. P ($@ P))
# (λabs.
# (∀a. abs (Test$old1->@temp @ind_typeTest7<-old a) = a) ∧
# ∀r.
# (λa1'.
# ∀'Dertree' '@temp @ind_typeTest0list' .
# (∀a0'.
# (∃a0 a1.
# (a0' =
# (λa0 a1.
# ind_type$CONSTR 0 a0
# (ind_type$FCONS a1 (λn. ind_type$BOTTOM))) a0
# a1) ∧ '@temp @ind_typeTest0list' a1) ⇒
# 'Dertree' a0') ∧
# (∀a1'.
# (a1' =
# ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM)) ∨
# (∃a0 a1.
# (a1' =
# (λa0 a1.
# ind_type$CONSTR (SUC (SUC 0)) ARB
# (ind_type$FCONS a0
# (ind_type$FCONS a1
# (λn. ind_type$BOTTOM)))) a0 a1) ∧
# 'Dertree' a0 ∧ '@temp @ind_typeTest0list' a1) ⇒
# '@temp @ind_typeTest0list' a1') ⇒
# '@temp @ind_typeTest0list' a1') r ⇔
# (Test$old1->@temp @ind_typeTest7<-old (abs r) = r))
second argument to trans:
#|- (λP. P ($@ P))
# (λabs.
# (∀a. abs (Test$old1->@temp @ind_typeTest7<-old a) = a) ∧
# ∀r.
# (λa1'.
# ∀'Dertree' '@temp @ind_typeTest0list' .
# (∀a0'.
# (∃a0 a1.
# (a0' =
# (λa0 a1.
# ind_type$CONSTR 0 a0
# (ind_type$FCONS a1 (λn. ind_type$BOTTOM))) a0
# a1) ∧ '@temp @ind_typeTest0list' a1) ⇒
# 'Dertree' a0') ∧
# (∀a1'.
# (a1' =
# ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM)) ∨
# (∃a0 a1.
# (a1' =
# (λa0 a1.
# ind_type$CONSTR (SUC (SUC 0)) ARB
# (ind_type$FCONS a0
# (ind_type$FCONS a1
# (λn. ind_type$BOTTOM)))) a0 a1) ∧
# 'Dertree' a0 ∧ '@temp @ind_typeTest0list' a1) ⇒
# '@temp @ind_typeTest0list' a1') ⇒
# '@temp @ind_typeTest0list' a1') r ⇔
# (Test$old1->@temp @ind_typeTest7<-old (abs r) = r)) ⇔
# (λabs.
# (∀a. abs (Test$old1->@temp @ind_typeTest7<-old a) = a) ∧
# ∀r.
# (λa1'.
# ∀'Dertree' '@temp @ind_typeTest0list' .
# (∀a0'.
# (∃a0 a1.
# (a0' =
# (λa0 a1.
# ind_type$CONSTR 0 a0
# (ind_type$FCONS a1 (λn. ind_type$BOTTOM))) a0
# a1) ∧ '@temp @ind_typeTest0list' a1) ⇒
# 'Dertree' a0') ∧
# (∀a1'.
# (a1' =
# ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM)) ∨
# (∃a0 a1.
# (a1' =
# (λa0 a1.
# ind_type$CONSTR (SUC (SUC 0)) ARB
# (ind_type$FCONS a0
# (ind_type$FCONS a1 (λn. ind_type$BOTTOM))))
# a0 a1) ∧ 'Dertree' a0 ∧
# '@temp @ind_typeTest0list' a1) ⇒
# '@temp @ind_typeTest0list' a1') ⇒
# '@temp @ind_typeTest0list' a1') r ⇔
# (Test$old1->@temp @ind_typeTest7<-old (abs r) = r))
# (@abs.
# (∀a. abs (Test$old1->@temp @ind_typeTest7<-old a) = a) ∧
# ∀r.
# (λa1'.
# ∀'Dertree' '@temp @ind_typeTest0list' .
# (∀a0'.
# (∃a0 a1.
# (a0' =
# (λa0 a1.
# ind_type$CONSTR 0 a0
# (ind_type$FCONS a1 (λn. ind_type$BOTTOM))) a0
# a1) ∧ '@temp @ind_typeTest0list' a1) ⇒
# 'Dertree' a0') ∧
# (∀a1'.
# (a1' =
# ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM)) ∨
# (∃a0 a1.
# (a1' =
# (λa0 a1.
# ind_type$CONSTR (SUC (SUC 0)) ARB
# (ind_type$FCONS a0
# (ind_type$FCONS a1
# (λn. ind_type$BOTTOM)))) a0 a1) ∧
# 'Dertree' a0 ∧ '@temp @ind_typeTest0list' a1) ⇒
# '@temp @ind_typeTest0list' a1') ⇒
# '@temp @ind_typeTest0list' a1') r ⇔
# (Test$old1->@temp @ind_typeTest7<-old (abs r) = r))
On 26 April 2017 at 03:55, Chun Tian (binghe) <binghe.l...@gmail.com> wrote:
> 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
> >>
> >>
> >
>
>
------------------------------------------------------------------------------
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
