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

[Joe Leslie-Hurd]

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