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

[Robert White]

Dear Joe,
I think HOL Light is more updated. We maybe need to export some files
again.
For example. the arith.ml
The first missing thm is ADD_SUBR, while in the up-to-date HOL Light they
have ADD_SUBR defined but not in OpenTheory HOL.
So I have the feeling that we need to generate the base.art again I think?

Regards,
Robert


On 26 June 2015 at 06:44, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Robert,
>
> This is a mystery to me: perhaps there are many theorems deleted in
> the OpenTheory fork of HOL Light compared to the standard distribution
> (which is what the database.ml file records)?
>
> Cheers,
>
> Joe
>
>
> On Thu, Jun 25, 2015 at 3:26 AM, Robert White
> <ai.robert.wangshuai at gmail.com> wrote:
> > 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 (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]
> >>
> >
> >
> >
> > --
> >
> > 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]
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150629/27179a4e/attachment-0001.html>