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

Robert White ai.robert.wangshuai at gmail.com
Wed Jul 1 20:30:15 UTC 2015
Next message: [opentheory-users] error loading article files (again?).
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
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 <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/20150701/ed4fd9e7/attachment-0001.html>
Next message: [opentheory-users] error loading article files (again?).
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
More information about the opentheory-users mailing list