<div dir="ltr">Ok, I will try now.<div> </div><div>Thanks a lot.</div><div> </div><div>Regards,</div><div>Robert</div></div><div class="gmail_extra"> <div class="gmail_quote">On 7 June 2015 at 08:56, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Robert, It turned out the import code didn't work very well, but I have fixed it up and it seems to be doing the right thing. For each theory you import, you have to first extend_the_interpretation so the importer can give a HOL Light name to the OpenTheory symbols in the article. Also, a nice feature is that imports build on each other, so you can import a sequence of theories where assumptions in later theories are satisfied by theorems in earlier theories. Below is an example showing how to import theories - each article file was generated by a command of the form: opentheory info --article -o natural-prime.art natural-prime This new import code is all checked in to my HOL Light fork available at <a href="http://src.gilith.com/hol-light.html" target="_blank">http://src.gilith.com/hol-light.html</a> Cheers, Joe (* ------------------------------------------------------------------------- *) (* Importing a theory. *) (* ------------------------------------------------------------------------- *) extend_the_interpretation "opentheory/theories/natural-divides/<a href="http://natural-divides.int" target="_blank">natural-divides.int</a>";; import_article "natural-divides.art";; extend_the_interpretation "opentheory/theories/stream/<a href="http://stream.int" target="_blank">stream.int</a>";; import_article "stream.art";; extend_the_interpretation "opentheory/theories/natural-prime/<a href="http://natural-prime.int" target="_blank">natural-prime.int</a>";; import_article "natural-prime.art";; <div class="HOEnZb"><div class="h5"> On Fri, Jun 5, 2015 at 1:33 PM, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote: > OK, that's not good. Let me take a look. > > Cheers, > > Joe > > On Fri, Jun 5, 2015 at 12:59 PM, Robert White > <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> wrote: >> :( >> >> looks it is not working that way. >> >> # import_article "../laholide/opentheory/natural-divides.art";; >> Exception: >> Failure >> "in article ../laholide/opentheory/natural-divides.art at line 159: >> defineConst\nstack = [Term; \"Number.Natural.divides\"; Var; Var; >> []]\nunknown constant \"Number.Natural.divides\"". >> # >> >> >> and when I load other files, say list.art. I get all the thm as None. OHHH >> :( >> >> # import_article "../laholide/opentheory/list.art";; >> val it : >> (term list * term) list * (thm option * (term list * term)) option list = >> ([([], `(!) = (\p. p = (\x. T))`); >> ([], `(/\) = (\p q. (\f. f p q) = (\f. f T T))`); >> ([], `!n. EVEN (SUC n) <=> ~EVEN n`); >> ([], `!n. EVEN (BIT0 (BIT1 _0) * n)`); >> ([], `!m n. SUC m = SUC n <=> m = n`); >> ([], `!m n p. m * n = m * p <=> m = _0 \/ n = p`); >> ([], `!m n. m <= n /\ n <= m <=> m = n`); ([], `BIT0 _0 = _0`); >> ([], `!n. _0 + n = n`); ([], `!n. BIT0 (SUC n) = SUC (SUC (BIT0 n))`); >> ([], `!m n. SUC m + n = SUC (m + n)`); >> ([], `!m n. m + SUC n = SUC (m + n)`); >> ([], `!p. p _0 /\ (!n. p n ==> p (SUC n)) ==> (!n. p n)`); >> ([], `!n. BIT1 n = SUC (BIT0 n)`); ([], `!n. _0 <= n`); >> ([], `!m. m <= _0 <=> m = _0`); ([], `!n. BIT0 (BIT1 _0) * n = n + n`); >> ([], `!m n. m <= SUC n <=> m = SUC n \/ m <= n`); >> ([], `!m n. m * n = _0 <=> m = _0 \/ n = _0`); ([], `!n. ~(SUC n = >> _0)`); >> ([], `!m n p. m * n <= m * p <=> m = _0 \/ n <= p`); >> ([], `!m n. SUC m <= n <=> m < n`); >> ([], `!m n p. m * n < m * p <=> ~(m = _0) /\ n < p`); >> ([], `!m n. m <= n <=> m < n \/ m = n`); >> ([], `!m n. EVEN (m * n) <=> EVEN m \/ EVEN n`); >> ([], `!m n. EVEN (m + n) <=> EVEN m <=> EVEN n`); >> ([], `!m n. ~(m <= n /\ n < m)`); ([], `!m n. ~(m < n /\ n <= m)`); >> ([], `!m. m EXP _0 = BIT1 _0`); ([], `!m n. m EXP SUC n = m * m EXP n`); >> ([], `!m n p. m * n * p = (m * n) * p`); >> ([], `!m n. m EXP n = _0 <=> m = _0 /\ ~(n = _0)`); >> ([], `!p m n. m + p = n + p <=> m = n`); >> ([], `!e f. ?!fn. fn _0 = e /\ (!n. fn (SUC n) = f (fn n) n)`); >> ([], `!m n. ~(m <= n) <=> n < m`); >> ([], `!m n. m < n <=> (?d. n = m + SUC d)`); ([], `!m n. m + n = n + >> m`); >> ([], `!m. m + _0 = m`); ([], `!m n. SUC m <= SUC n <=> m <= n`); >> ([], `CARD {} = _0`); >> ([], >> `!x s. >> FINITE s >> ==> CARD (x INSERT s) = (if x IN s then CARD s else SUC (CARD >> s))`); >> ([], `!n. n <= SUC n`); ([], `!n. n <= n`); >> ([], `!m n p. m <= n /\ n <= p ==> m <= p`); >> ([], `!m n. (m + n) - m = n`); ([], `!n. n - n = _0`); >> ([], `!m n. m + n = _0 <=> m = _0 /\ n = _0`); ([], `!m n. m <= m + n`); >> ([], `!m n. m + n = n <=> m = _0`); ([], `!n. SUC n - BIT1 _0 = n`); >> ([], `!m. ~(m < _0)`); ([], `!m. m = _0 \/ (?n. m = SUC n)`); >> ([], `!m n. SUC m < SUC n <=> m < n`); ([], `!n. n < SUC n`); >> ([], `!p x. p x ==> p ((@) p)`); >> ([], `!n. {m | m < SUC n} = _0 INSERT {SUC m | m < n}`); >> ([], `!m n. n <= m + n`); ([], `!n. ~(n < n)`); ([], `!m. m - _0 = m`); >> ([], `!n. _0 < SUC n`); ([], `!m n. ~(m < n) <=> n <= m`); >> ([], `!m n. n <= m ==> SUC m - SUC n = m - n`); >> ([], `!m. SUC m = m + BIT1 _0`); ([], `!m n p. m + n + p = (m + n) + >> p`); >> ([], `!m n p. m < n /\ n <= p ==> m < p`); >> ([], `!m n p. m + n <= m + p <=> n <= p`)], >> [None; None; None; None; None; None; None; None; None; None; None; None; >> None; None; None; None; None; None; None; None; None; None; None; None; >> None; None; None; None; None; None; None; None; None; None; None; None; >> None; None; None; None; None; None; None; None; None; None; None; None; >> None; None; None; None; None; None; None; None; None; None; None; None; >> None; None; None; None; None; None; None; None; None; None; None; None; >> None; None; None; None; None; None; None; None; None; None; None; None; >> None; None; None; None; None; None; None; None; None; None; None; None; >> None; None; None; ...]) >> >> >> >> >> On 5 June 2015 at 19:14, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote: >>> >>> Hi Robert, >>> >>> Perhaps a more realistic case study would be to import a new theory >>> from the OpenTheory repo: >>> >>> <a href="http://opentheory.gilith.com/" target="_blank">http://opentheory.gilith.com/</a> >>> >>> For example, >>> >>> opentheory install natural-divides >>> opentheory info --article -o natural-divides.art natural-divides >>> >>> and then import this article file? >>> >>> Cheers, >>> >>> Joe >>> >>> On Fri, Jun 5, 2015 at 10:04 AM, Robert White >>> <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> wrote: >>> > Hi Joe, >>> > >>> > At the moment I am only trying to load the old proofs. but if I don't >>> > change >>> > the <a href="http://hol.ml" target="_blank">hol.ml</a> file there will be conflict then. So seems the only solution >>> > is >>> > that I completely comment out the rest of the files loaded in <a href="http://hol.ml" target="_blank">hol.ml</a> if >>> > so? >>> > >>> > No, I don't have new theories so far. >>> > Regards, >>> > Robert >>> > >>> > On 5 June 2015 at 19:00, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote: >>> >> >>> >> Hi Robert, >>> >> >>> >> You are using it correctly. The intent of the import facility is to >>> >> extend the current logical context by bringing in a new theory, not to >>> >> change the current logical context. The error that you are redefining >>> >> the T constant is an indication that you are trying to change the >>> >> current logical context. >>> >> >>> >> What is your eventual goal using the OpenTheory importer in HOL Light? >>> >> I assume you have some new theories you want to import that are not >>> >> already in HOL Light. >>> >> >>> >> Cheers, >>> >> >>> >> Joe >>> >> >>> >> >>> >> On Fri, Jun 5, 2015 at 5:44 AM, Robert White >>> >> <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> wrote: >>> >> > Dear Joe, >>> >> > >>> >> > I am wondering if I am using it correctly. I would like to load some >>> >> > thm >>> >> > in >>> >> > and do some proof checking and proof optimisation. However, after >>> >> > loading >>> >> > the <a href="http://hol.ml" target="_blank">hol.ml</a> and then do >>> >> > let all = import_article "../../laholide/opentheory/bool.art";; >>> >> > I get errors saying I am redefining constants. For instance, the >>> >> > bool.art >>> >> > file: >>> >> > >>> >> > # let all = import_article "../../laholide/opentheory/bool.art";; >>> >> > Exception: >>> >> > Failure >>> >> > "in article ../../laholide/opentheory/bool.art at line 89: >>> >> > defineConst\nstack = [Term; \"Data.Bool.T\"; Thm]\nnew_constant: >>> >> > constant T >>> >> > has already been declared". >>> >> > >>> >> > I could solve the problem by either not loading some of the files in >>> >> > HOL, so >>> >> > constants won't be redefined, or try to detect the problems that are >>> >> > defined >>> >> > but going to be redefined the same way. I would you solve the problem >>> >> > for >>> >> > the OpenTheory version of HOL. >>> >> > >>> >> > Thanks >>> >> > Regards, >>> >> > Robert >>> >> > >>> >> > >>> >> > On 5 June 2015 at 08:38, Robert White <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> >>> >> > wrote: >>> >> >> >>> >> >> Thanks Joe! >>> >> >> >>> >> >> I will have to do some more test. I will let you know if I find any >>> >> >> bug. >>> >> >> >>> >> >> Regards, >>> >> >> Robert >>> >> >> >>> >> >> On 5 June 2015 at 04:55, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote: >>> >> >>> >>> >> >>> Robert and I have updated the HOL Light importer to work with >>> >> >>> version >>> >> >>> 6 articles, which is now available from >>> >> >>> >>> >> >>> <a href="http://src.gilith.com/hol-light.html" target="_blank">http://src.gilith.com/hol-light.html</a> >>> >> >>> >>> >> >>> It is very lightly tested at this point, so it may well be buggy. I >>> >> >>> was able to read in the standard theory library as a version 6 >>> >> >>> article, which I generated using the command >>> >> >>> >>> >> >>> opentheory info --article -o base.art base >>> >> >>> >>> >> >>> but I didn't even look closely at the results. >>> >> >>> >>> >> >>> Cheers, >>> >> >>> >>> >> >>> Joe >>> >> >>> >>> >> >>> >>> >> >>> On Wed, Jun 3, 2015 at 2:12 PM, Robert White >>> >> >>> <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> wrote: >>> >> >>> > Thanks for the reply. >>> >> >>> > >>> >> >>> > I would like to give it a try so I choose option 3 for now. I >>> >> >>> > will >>> >> >>> > use >>> >> >>> > option 1 to continue my project alongside. >>> >> >>> > >>> >> >>> > Regards, >>> >> >>> > Robert >>> >> >>> > >>> >> >>> > On 3 June 2015 at 22:46, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote: >>> >> >>> >> >>> >> >>> >> Hi Robert, >>> >> >>> >> >>> >> >>> >> Unfortunately I have not yet updated the import capability in my >>> >> >>> >> HOL >>> >> >>> >> Light fork to work with version 6 theories. You can either: >>> >> >>> >> >>> >> >>> >> 1. Use the command I showed you before to convert version 6 >>> >> >>> >> articles >>> >> >>> >> to version 5 before importing them. >>> >> >>> >> 2. Wait for me to implement this functionality. >>> >> >>> >> 3. Implement it yourself and send me a pull request. >>> >> >>> >> >>> >> >>> >> Please let me know what you decide: it may affect the wait time >>> >> >>> >> in >>> >> >>> >> solution 2 :-) >>> >> >>> >> >>> >> >>> >> Cheers, >>> >> >>> >> >>> >> >>> >> Joe >>> >> >>> >> >>> >> >>> >> On Wed, Jun 3, 2015 at 7:58 AM, Robert White >>> >> >>> >> <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> wrote: >>> >> >>> >> > Dear Joe, >>> >> >>> >> > >>> >> >>> >> > I noticed that I can't using import for the current version >>> >> >>> >> > (version >>> >> >>> >> > 6). >>> >> >>> >> > I >>> >> >>> >> > am using the one from: >>> >> >>> >> > >>> >> >>> >> > git clone <a href="http://src.gilith.com/hol-light" target="_blank">http://src.gilith.com/hol-light</a> >>> >> >>> >> > >>> >> >>> >> > >>> >> >>> >> > I wonder if you have implemented it/updated the <a href="http://import.ml" target="_blank">import.ml</a> >>> >> >>> >> > file, >>> >> >>> >> > so I >>> >> >>> >> > won't >>> >> >>> >> > have to redo your work. >>> >> >>> >> > >>> >> >>> >> > >>> >> >>> >> > Thanks >>> >> >>> >> > >>> >> >>> >> > Robert >>> >> >>> >> > >>> >> >>> >> > >>> >> >>> > >>> >> >>> > >>> >> >>> > >>> >> >>> > >>> >> >>> > -- >>> >> >>> > >>> >> >>> > Regards, >>> >> >>> > Robert White (Shuai Wang) >>> >> >>> > INRIA Deducteam >>> >> >> >>> >> >> >>> >> >> >>> >> >> >>> >> >> -- >>> >> >> >>> >> >> Regards, >>> >> >> Robert White (Shuai Wang) >>> >> >> INRIA Deducteam >>> >> >> [Moving to ILLC of UvA from this Sep. ] >>> >> >> [New email address will be <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a>] >>> >> >> >>> >> > >>> >> > >>> >> > >>> >> > -- >>> >> > >>> >> > Regards, >>> >> > Robert White (Shuai Wang) >>> >> > INRIA Deducteam >>> >> > [Moving to ILLC of UvA from this Sep. ] >>> >> > [New email address will be <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a>] >>> >> > >>> > >>> > >>> > >>> > >>> > -- >>> > >>> > Regards, >>> > Robert White (Shuai Wang) >>> > INRIA Deducteam >>> > [Moving to ILLC of UvA from this Sep. ] >>> > [New email address will be <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a>] >>> > >> >> >> >> >> -- >> >> Regards, >> Robert White (Shuai Wang) >> INRIA Deducteam >> [Moving to ILLC of UvA from this Sep. ] >> [New email address will be <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a>] >> </div></div></blockquote></div> <div> </div>-- <div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div> </div><div>Regards,</div><div><a href="http://www.dptinfo.ens-cachan.fr/~swang/" target="_blank">Robert White </a>(Shuai Wang)</div><div><a href="https://www.rocq.inria.fr/deducteam/" target="_blank">INRIA Deducteam</a></div><div>[Moving to ILLC of UvA from this Sep. ]</div><div>[New email address will be <a href="mailto:shuai.wang@student.uva.nl" target="_blank">shuai.wang@student.uva.nl</a>]</div><div> </div></div></div></div></div></div></div></div></div></div></div> </div>