Hi Chun,
Try with the latest update to HOL (672f27ee9), which I think may fix the
problem in HOL's OpenTheory Logging module.
Cheers,
Ramana
On 28 April 2017 at 19:22, Chun Tian (binghe) <binghe.l...@gmail.com> wrote:
> 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
