[opentheory-users] error loading article files (again?).

[Robert White]

Hi again.

There are over 2200 thms in the hol database.ml but there are "to the
most"[1] 1885 thms. So where are the rest?

[1]I tried to load the files commented out in hol.ml.


On 25 June 2015 at 12:16, Robert White <ai.robert.wangshuai at gmail.com>
wrote:

> Hi Joe,
>
> So I tested the HOL "theorems" also, Here are the results:
> # List.length(!theorems);;
> val it : int = 1670
>
> So that means there are 1670 - 1214 = 456 theorems not exported to
> Opentheory?
>
>
>
>
> On 25 June 2015 at 12:06, Robert White <ai.robert.wangshuai at gmail.com>
> wrote:
>
>> Hi Joe,
>>
>> Thanks for the reply.
>>
>> 2) So maybe I can try to export them? Cos the more thms I get is better
>> for my tests.
>> but I got more thms when I do this search. Why is that (So far we should
>> have 1214 right? 1214 are those only exported but 1670 are all of them (so
>> far))?
>>
>>  # List.length (search [])
>>   ;;
>> val it : int = 1670
>>
>>
>> On 24 June 2015 at 23:11, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>
>>> Hi Robert,
>>>
>>> Welcome back!
>>>
>>> 1) There hasn't been much development on OpenTheory in recent weeks,
>>> just some extensions to the natural-divides theory to support my
>>> recent blog post on the extended GCD algorithm:
>>>
>>>
>>> https://gilith.wordpress.com/2015/06/24/natural-number-greatest-common-divisor/
>>>
>>> 2) There is no real reason why those HOL Light theories have not been
>>> ported to OpenTheory, except that some of them might not be needed to
>>> compile a standard theory library (which is a common base of theories
>>> that is expected to be implemented in every theorem prover).
>>>
>>> We do not use the database.ml file which lists all the theorems in the
>>> main branch of the HOL Light theorem prover (not the OpenTheory fork).
>>> But I've just checked in a version of the fork that creates a theorem
>>> database of the standard theory library at the bottom of the hol.ml
>>> file, so after loading with #use "hol.ml";; you can search the
>>> database like so:
>>>
>>> # search [`MAX (SUC m) (SUC n)`];;
>>> val it : (string * thm) list =
>>>   [("MAX_SUC", |- !m n. MAX (SUC m) (SUC n) = SUC (MAX m n))]
>>>
>>> 3) It looks like you need to extend_the_interpretation before loading
>>> the proofs as described in
>>>
>>> http://www.gilith.com/opentheory/mailing-list/2015-June/000515.html
>>>
>>> Cheers,
>>>
>>> Joe
>>>
>>> On Wed, Jun 24, 2015 at 1:31 PM, Robert White
>>> <ai.robert.wangshuai at gmail.com> wrote:
>>> > Dear Joe and all,
>>> >
>>> > I am back to the community!
>>> >
>>> > I have the following questions and updates for you:
>>> >
>>> > 1) I will be finishing my internship in a few weeks and it would be
>>> nice of
>>> > you if you can give me some description of the most recent updates of
>>> > OpenTheory.
>>> >
>>> > 2)
>>> > I noticed there is a part not imported to Opentheory (in hol.ml) :
>>> >
>>> > (* Not yet ported to OpenTheory
>>> > loads "calc_int.ml";;   (* Calculation with integer-valued reals
>>> > *)
>>> > loads "realarith.ml";;  (* Universal linear real decision procedure
>>> > *)
>>> > loads "real.ml";;       (* Derived properties of reals
>>> > *)
>>> > loads "calc_rat.ml";;   (* Calculation with rational-valued reals
>>> > *)
>>> > loads "int.ml";;        (* Definition of integers
>>> > *)
>>> > loads "iterate.ml";;    (* Iterated operations
>>> > *)
>>> > loads "cart.ml";;       (* Finite Cartesian products
>>> > *)
>>> > *)
>>> >
>>> > Is there any reason why not?
>>> >
>>> > Also, there is a database.ml file. Shall I ignore that in OpenTheory
>>> HOL?
>>> > (since it is not complete anyway)
>>> >
>>> > 3)
>>> > I have problem loading article files:
>>> >
>>> > # let p = load_proofs
>>> > "/home/robert/Project/laholide/opentheory/stream.art";;
>>> > Exception:
>>> > Failure
>>> >  "in article /home/robert/Project/laholide/opentheory/stream.art at
>>> line
>>> > 1273: defineTypeOp\nstack = [Thm; [\"A\"]; \"Data.Stream.nth\";
>>> > \"Data.Stream.fromFunction\"; \"Data.Stream.stream\"; Var; Var;
>>> > \"Data.Stream.unfold\"; Var; \"Data.Stream.iterate\";
>>> > \"Data.Stream.replicate\"]\nunknown type operator
>>> \"Data.Stream.stream\"".
>>> > # let p = load_proofs
>>> > "/home/robert/Project/laholide/opentheory/natural-prime.art";;
>>> > Exception:
>>> > Failure
>>> >  "in article
>>> /home/robert/Project/laholide/opentheory/natural-prime.art at
>>> > line 191: const\nstack = [\"Number.Natural.divides\"; Term; Var; Term;
>>> Term;
>>> > Var; \"Number.Natural.prime\"; Term; Var; [[]; [[Var; Term]]];
>>> Thm]\nunknown
>>> > constant \"Number.Natural.divides\"".
>>> > # let p = load_proofs
>>> > "/home/robert/Project/laholide/opentheory/natural-divide.art";;
>>> > Exception:
>>> > Sys_error
>>> >  "/home/robert/Project/laholide/opentheory/natural-divide.art: No such
>>> file
>>> > or directory".
>>> > # let p = load_proofs
>>> > "/home/robert/Project/laholide/opentheory/natural-divides.art";;
>>> > Exception:
>>> > Failure
>>> >  "in article
>>> /home/robert/Project/laholide/opentheory/natural-divides.art at
>>> > line 159: defineConst\nstack = [Term; \"Number.Natural.divides\"; Var;
>>> Var;
>>> > []]\nunknown constant \"Number.Natural.divides\"".
>>> > # let p = load_proofs
>>> > "/home/robert/Project/laholide/opentheory/modular.art";;
>>> > Exception:
>>> > Failure
>>> >  "in article /home/robert/Project/laholide/opentheory/modular.art at
>>> line
>>> > 155: const\nstack = [\"Number.Modular.modulus\"; Term; Term; Var; Var;
>>> > \"Number.Modular.equivalent\"; Term; Var; Term; Var; [];
>>> > \"HOLLight.modular_to_class\"; \"HOLLight.modular_from_class\";
>>> > \"Number.Modular.modular\"; TypeOp<fun>; TypeOp<fun>;
>>> Const<!>]\nunknown
>>> > constant \"Number.Modular.modulus\"".
>>> > # let p = load_proofs
>>> "/home/robert/Project/laholide/opentheory/gfp.art";;
>>> > Exception:
>>> > Failure
>>> >  "in article /home/robert/Project/laholide/opentheory/gfp.art at line
>>> 54:
>>> > const\nstack = [\"Number.GF(p).oddprime\"; Term; Var; []]\nunknown
>>> constant
>>> > \"Number.GF(p).oddprime\"".
>>> > # let p = load_proofs
>>> > "/home/robert/Project/laholide/opentheory/natural-fibonacci.art";;
>>> > Exception:
>>> > Failure
>>> >  "in article
>>> /home/robert/Project/laholide/opentheory/natural-fibonacci.art
>>> > at line 1933: defineConstList\nstack = [Thm;
>>> > [[\"Number.Natural.Fibonacci.zeckendorf\"; Var]]; Var; [];
>>> Thm]\nunknown
>>> > constant \"Number.Natural.Fibonacci.zeckendorf\"".
>>> > # let p = load_proofs
>>> "/home/robert/Project/laholide/opentheory/word.art";;
>>> > Exception:
>>> > Failure
>>> >  "in article /home/robert/Project/laholide/opentheory/word.art at line
>>> 130:
>>> > const\nstack = [\"Data.Word.width\"; Term; \"Data.Word.modulus\"; Thm;
>>> > Thm]\nunknown constant \"Data.Word.width\"".
>>> > #
>>> >
>>> > Could you please help on that? It seems I can't even play with the
>>> other
>>> > article files I used to be able to load either :(
>>> >
>>> > Thanks very much!
>>> >
>>> > --
>>> >
>>> > Regards,
>>> > Robert White (Shuai Wang)
>>> > INRIA Deducteam
>>> > [Moving to ILLC of UvA from this Sep to continue my masters. ]
>>> > [New email address will be shuai.wang at student.uva.nl]
>>> >
>>>
>>
>>
>>
>> --
>>
>> Regards,
>> Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
>> INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
>> [Moving to ILLC of UvA from this Sep to continue my masters. ]
>> [New email address will be shuai.wang at student.uva.nl]
>>
>>
>
>
> --
>
> Regards,
> Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
> INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
> [Moving to ILLC of UvA from this Sep to continue my masters. ]
> [New email address will be shuai.wang at student.uva.nl]
>
>


-- 

Regards,
Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
[Moving to ILLC of UvA from this Sep to continue my masters. ]
[New email address will be shuai.wang at student.uva.nl]
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150625/2310c6bb/attachment-0001.html>