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

[Joe Leslie-Hurd]

Hi Robert,

As far as I understand it, the update_database command uses some OCaml
magic to look for top-level OCaml bindings of type thm, and inserts
everything it finds into the theorems reference.

So to export more theorems for your project you could export all the
theorems in the theorems reference (this should be a superset of the
exported theorems).

Cheers,

Joe

On Thu, Jun 25, 2015 at 3:06 AM, 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 (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]
>