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