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

[Robert White]

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 <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/20150624/ff546f0f/attachment.html>