Hi,
I see you have already consulted in OpenTheory mailing list and Joe Hurd
has suggested to use the development version of OpenTheory. Now I see this
error:
Test.ot.art
FAILED!
('@temp
@ind_typeTest0list'
a1))))))
('@temp @ind_typeTest0list'
a1'))))
('@temp @ind_typeTest0list' a1')))) <=>
HOL4.Test.@temp @ind_typeTest7 (abs r) = r)) in
P (HOL4.min. P)
different constants at path 10110 subterms: HOL4.min.@ vs HOL4.min.
different constants: HOL4.min.@ vs HOL4.min.
different constant names
I'm sorry for not understanding things at this level, only wondering: is
this indicating a bug in HOL's OpenTheory module?
Regards,
Chun
On 26 April 2017 at 03:57, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> wrote:
> 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
>> >>
>> >>
>> >
>>
>>
>
--
Chun Tian (binghe)
University of Bologna (Italy)
------------------------------------------------------------------------------
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
