<div dir="ltr"><span style="font-size:12.8000001907349px">Dear Joe and all,</span><div style="font-size:12.8000001907349px"><br></div><div style="font-size:12.8000001907349px">I am back to the community!</div><div style="font-size:12.8000001907349px"><br></div><div style="font-size:12.8000001907349px">I have the following questions and updates for you:</div><div style="font-size:12.8000001907349px"><br></div><div style="font-size:12.8000001907349px">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.</div><div style="font-size:12.8000001907349px"><br></div><div style="font-size:12.8000001907349px">2) </div><div style="font-size:12.8000001907349px">I noticed there is a part not imported to Opentheory (in <a href="http://hol.ml/" target="_blank">hol.ml</a>) :</div><div style="font-size:12.8000001907349px"><br></div><div style="font-size:12.8000001907349px"><div>(* Not yet ported to OpenTheory</div><div>loads "<a href="http://calc_int.ml/" target="_blank">calc_int.ml</a>";; (* Calculation with integer-valued reals *)</div><div>loads "<a href="http://realarith.ml/" target="_blank">realarith.ml</a>";; (* Universal linear real decision procedure *)</div><div>loads "<a href="http://real.ml/" target="_blank">real.ml</a>";; (* Derived properties of reals *)</div><div>loads "<a href="http://calc_rat.ml/" target="_blank">calc_rat.ml</a>";; (* Calculation with rational-valued reals *)</div><div>loads "<a href="http://int.ml/" target="_blank">int.ml</a>";; (* Definition of integers *)</div><div>loads "<a href="http://iterate.ml/" target="_blank">iterate.ml</a>";; (* Iterated operations *)</div><div>loads "<a href="http://cart.ml/" target="_blank">cart.ml</a>";; (* Finite Cartesian products *)</div><div>*)</div></div><div style="font-size:12.8000001907349px"><br></div><div style="font-size:12.8000001907349px">Is there any reason why not?</div><div style="font-size:12.8000001907349px"><br></div><div style="font-size:12.8000001907349px">Also, there is a <a href="http://database.ml/" target="_blank">database.ml</a> file. Shall I ignore that in OpenTheory HOL? (since it is not complete anyway)</div><div style="font-size:12.8000001907349px"><br></div><div style="font-size:12.8000001907349px">3) </div><div style="font-size:12.8000001907349px">I have problem loading article files:</div><div style="font-size:12.8000001907349px"><br></div><div style="font-size:12.8000001907349px"><div># let p = load_proofs "/home/robert/Project/laholide/opentheory/stream.art";;</div><div>Exception:</div><div>Failure</div><div> "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\"".</div><div># let p = load_proofs "/home/robert/Project/laholide/opentheory/natural-prime.art";;</div><div>Exception:</div><div>Failure</div><div> "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\"".</div><div># let p = load_proofs "/home/robert/Project/laholide/opentheory/natural-divide.art";;</div><div>Exception:</div><div>Sys_error</div><div> "/home/robert/Project/laholide/opentheory/natural-divide.art: No such file or directory".</div><div># let p = load_proofs "/home/robert/Project/laholide/opentheory/natural-divides.art";;</div><div>Exception:</div><div>Failure</div><div> "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\"".</div><div># let p = load_proofs "/home/robert/Project/laholide/opentheory/modular.art";;</div><div>Exception:</div><div>Failure</div><div> "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\"".</div><div># let p = load_proofs "/home/robert/Project/laholide/opentheory/gfp.art";;</div><div>Exception:</div><div>Failure</div><div> "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\"".</div><div># let p = load_proofs "/home/robert/Project/laholide/opentheory/natural-fibonacci.art";;</div><div>Exception:</div><div>Failure</div><div> "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\"".</div><div># let p = load_proofs "/home/robert/Project/laholide/opentheory/word.art";;</div><div>Exception:</div><div>Failure</div><div> "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\"".</div><div># </div></div><div style="font-size:12.8000001907349px"><br></div><div style="font-size:12.8000001907349px">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 :(</div><div style="font-size:12.8000001907349px"><br></div><div style="font-size:12.8000001907349px">Thanks very much!</div><div><br></div>-- <br><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div><br></div><div>Regards,</div><div><a href="http://www.dptinfo.ens-cachan.fr/~swang/" target="_blank">Robert White </a>(Shuai Wang)</div><div><a href="https://www.rocq.inria.fr/deducteam/" target="_blank">INRIA Deducteam</a></div><div>[Moving to ILLC of UvA from this Sep <span style="font-size:small">to continue my masters</span><span style="font-size:12.8000001907349px">. ]</span></div><div>[New email address will be <a href="mailto:shuai.wang@student.uva.nl" target="_blank">shuai.wang@student.uva.nl</a>]</div><div><br></div></div></div></div></div></div></div></div></div> </div>