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

[Robert White]

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]
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150625/80e4f217/attachment.html>