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

Robert White ai.robert.wangshuai at gmail.com
Wed Jul 1 22:09:39 UTC 2015
Previous message: [opentheory-users] error loading article files (again?).
Next message: [opentheory-users] error loading article files (again?).
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
Okay then. Looks like I have to use the old data for testing then.
Please let me know when it's updated :)

Thanks a lot
Robert

On 1 July 2015 at 22:57, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Robert,
>
> Sorry, I haven't been able to do the merge yet (it's a bit fiddly, so
> it requires an uninterrupted block of time which is a scarce resource
> for me right now).
>
> However, I can answer your question right now. I do want the
> OpenTheory fork of HOL Light to be as close as possible to the main
> trunk of HOL Light, but there are certain changes that are required to
> export a standard theory library (which is the primary purpose of this
> fork). For example, introducing an explicit set type (A set) rather
> than the predicate (A -> bool) and removing default cases (e.g., PRE 0
> = 0) are necessary to ensure the standard theory library can be used
> in as many environments as possible.
>
> Cheers,
>
> Joe
>
>
>
> On Wed, Jul 1, 2015 at 1:30 PM, Robert White
> <ai.robert.wangshuai at gmail.com> wrote:
> > Dear Joe,
> >
> > Is there any updates on this?
> >
> > Regards,
> > Robert
> >
> > On 29 June 2015 at 21:04, Robert White <ai.robert.wangshuai at gmail.com>
> > wrote:
> >>
> >> Dear Joe,
> >>
> >> Thanks for the reply. I am looking forward to the updates!
> >>
> >> Here are things I found which might be useful for you:
> >>
> >> 1)
> >> Looks like there is something wrong going on there in sum.ml:
> >> Exception: Failure "REFL_TAC".
> >> Error in included file ----/hol_light/opentheory/stdlib/sum.ml
> >>
> >> 2) There is no CASES_TAC in the most up-to-date version of HOL Light.
> >>
> >> Questions:
> >> 1) Why do you want things to be different?
> >>
> >> Cheers
> >> Robert
> >>
> >>
> >>
> >>
> >> On 29 June 2015 at 20:30, Joe Leslie-Hurd <joe at gilith.com> wrote:
> >>>
> >>> Hi Robert,
> >>>
> >>> In general there are quite a few differences in definitions and
> >>> theorems between the OpenTheory fork of HOL Light and the trunk, and
> >>> some of that is here to stay (e.g., the explicit type of sets in the
> >>> OpenTheory fork).
> >>>
> >>> That said, it's past time to do a merge with the HOL Light trunk and
> >>> create a new version of the standard theory library: I will work on
> >>> this.
> >>>
> >>> Cheers,
> >>>
> >>> Joe
> >>>
> >>>
> >>> On Mon, Jun 29, 2015 at 10:43 AM, Robert White
> >>> <ai.robert.wangshuai at gmail.com> wrote:
> >>> > Dear Joe,
> >>> >
> >>> > I tried to update the arith.ml file. It seems more complicated than
> I
> >>> > expected.
> >>> > For example, we have LE_ZERO but the new version deleted it.
> >>> >
> >>> > So shall I continue or maybe you have better advice?
> >>> > Regards,
> >>> > Robert
> >>> >
> >>> > On 29 June 2015 at 19:16, Robert White <
> ai.robert.wangshuai at gmail.com>
> >>> > wrote:
> >>> >>
> >>> >> 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 (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/20150702/bf343cfb/attachment-0001.html>
Previous message: [opentheory-users] error loading article files (again?).
Next message: [opentheory-users] error loading article files (again?).
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
More information about the opentheory-users mailing list