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

[Joe Leslie-Hurd]

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]
>