Oh sorry. Originally I couldn't reproduce the error, but now I can. You can
avoid it by using a Test.otd file to skip logging certain theorems, e.g.,
Test.otd:
skipthm Dertree_TY_DEF
delproof Dertree_case_def
delproof Dertree_size_def
delproof Dertree_11
delproof Dertree_Axiom
delproof Dertree_case_cong
delproof Dertree_induction
delproof Dertree_nchotomy
skipthm datatype_Dertree
(This avoids logging almost everything, but you could experiment with
different variations, depending on which theorems you actually need logged.)
At a brief look, it seems like there are still some problems with the
treatment of retired constants. However, I haven't been able to find or
solve the problem yet. I just want to let you know I might not be able to
look at it for a couple of weeks. Regarding retired constants, the
following change to HOL is probably an improvement (but not enough to get
your example to work):
diff --git a/src/opentheory/postbool/Logging.sml
b/src/opentheory/postbool/Logging.sml
index a46f17319..3a3c7149a 100644
--- a/src/opentheory/postbool/Logging.sml
+++ b/src/opentheory/postbool/Logging.sml
@@ -205,7 +205,7 @@ val (log_term, log_thm, log_clear,
in () end
end
- fun strip_old s = let
+ fun strip_old s = if not (String.isSubstring "old" s) then s else let
open Substring
val s = triml 3 (trimr 5 (full s))
val (_,s) = splitl Char.isDigit s
On 1 May 2017 at 21:22, Chun Tian (binghe) <[email protected]> wrote:
> But that’s the *same* mini theory we used before, with only a single
> Datatype definition:
>
> open HolKernel Parse boolLib bossLib;
> val _ = new_theory "Test”;
>
> val _ = Datatype `Dertree = Der 'a (Dertree list)`;
>
> val _ = export_theory ();
>
> I have no way to break that Datatype definition into smaller pieces ...
>
> Regards,
>
> Chun Tian
>
> > Il giorno 01 mag 2017, alle ore 07:42, Ramana Kumar <
> [email protected]> ha scritto:
> >
> > I think it would help if you could find another "mini" theory that
> exhibits the same issue... it's hard to tell what's wrong just from the
> error messages you sent.
> >
> > On 29 April 2017 at 23:25, Chun Tian (binghe) <[email protected]>
> wrote:
> > Hi Ramana,
> >
> > Thanks for fixing the issue. I have rebuilt HOL with 672f27ee9 included,
> now previous error in file "Test.art" around line 37270 has disappeared,
> but we got the next issue round line 99993:
> >
> > FATAL ERROR: opentheory failed:
> > in Article.fromTextFile:
> > error in file "Test.art" around line 99993:
> > thm
> > 13076
> > ref
> > …
> > Rule.alpha: not alpha-equivalent
> >
> > Full logs in zip is in attach. (the mail is re-sent with compressed
> attachments)
> >
> > Regards,
> >
> > Chun Tian
> >
> >
> >
> >
> > > Il giorno 29 apr 2017, alle ore 15:21, Chun Tian (binghe) <
> [email protected]> ha scritto:
> > >
> > >> Il giorno 29 apr 2017, alle ore 01:02, Ramana Kumar <
> [email protected]> ha scritto:
> > >>
> > >> 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) <[email protected]>
> 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 <[email protected]>
> 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?
> > >
> >
> >
> >
>
>
------------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
