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

[Joe Leslie-Hurd]

Hi Robert,

I have now completed the merge of the OpenTheory fork of HOL Light
with the trunk, and the standard theory library now contains 1231
theorems (up from 1214). You can get the latest version of the
OpenTheory fork of HOL Light simply by executing a git pull, and you
can install the latest version (base-1.200) of the standard theory
library using

opentheory update
opentheory upgrade

Cheers,

Joe

On Wed, Jul 1, 2015 at 3:09 PM, Robert White
<ai.robert.wangshuai at gmail.com> wrote:
> 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 (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]
>