<div dir="ltr">Dear Joe,<div><br></div><div>I still have problems:</div><div><br></div><div> <p class=""><span class="">$ opentheory upgrade</span></p> <p class=""><span class=""></span><br></p> <p class=""><span class="">FATAL ERROR: opentheory failed:</span></p> <p class=""><span class="">no matching installed packages</span></p> <p class=""><span class="">package upgrade failed</span></p><p class=""><span class=""><br></span></p><p class=""><span class="">Shall I maybe install everything again or wait for a more stable release? I don't know why it is not working right now.</span></p><p class="">Regards,</p><p class="">Robert</p></div></div><div class="gmail_extra"><br><div class="gmail_quote">On 29 October 2015 at 13:00, <span dir="ltr"><<a href="mailto:opentheory-users-request@gilith.com" target="_blank">opentheory-users-request@gilith.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Send opentheory-users mailing list submissions to<br> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br> <br> To subscribe or unsubscribe via the World Wide Web, visit<br> <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br> or, via email, send a message with subject or body 'help' to<br> <a href="mailto:opentheory-users-request@gilith.com">opentheory-users-request@gilith.com</a><br> <br> You can reach the person managing the list at<br> <a href="mailto:opentheory-users-owner@gilith.com">opentheory-users-owner@gilith.com</a><br> <br> When replying, please edit your Subject line so it is more specific<br> than "Re: Contents of opentheory-users digest..."<br> <br> <br> Today's Topics:<br> <br> 1. Re: Error loading articles (Joe Leslie-Hurd)<br> 2. Re: Error loading articles (Joe Leslie-Hurd)<br> <br> <br> ----------------------------------------------------------------------<br> <br> Message: 1<br> Date: Wed, 28 Oct 2015 08:10:07 -0700<br> From: Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>><br> To: OpenTheory users <<a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a>><br> Subject: Re: [opentheory-users] Error loading articles<br> Message-ID:<br> <CACQy07mOF=rDmrm2rqOymQSq504K8Gn7FdPBsr=<a href="mailto:ubYrmADynig@mail.gmail.com">ubYrmADynig@mail.gmail.com</a>><br> Content-Type: text/plain; charset=UTF-8<br> <br> Hi Robert,<br> <br> > 1) Here is the first problem: I can't import modular theory<br> ><br> > opentheory: unknown switch "--directory"<br> <br> I needed to add an extra switch to the opentheory tool that returned<br> the directory in which the theory file lives:<br> <br> $ opentheory info --directory base<br> /Users/joe/.opentheory/packages/base-1.200<br> <br> If you upgrade your opentheory tool to the latest release this switch<br> should be recognized.<br> <br> > 2) I also noticed that you removed start_logging();; Then how should I<br> > export the proofs. Could you please give me an example or maybe update the<br> > hacking doc?<br> <br> Yes, I did some simple renamings to consistently export the various<br> parts of a theory. I've already updated the FAQ:<br> <br> <a href="http://www.gilith.com/research/opentheory/faq.html#export-from-hol-light" rel="noreferrer" target="_blank">http://www.gilith.com/research/opentheory/faq.html#export-from-hol-light</a><br> <br> I'll also update the hacking doc shortly.<br> <br> Cheers,<br> <br> Joe<br> <br> <br> <br> ------------------------------<br> <br> Message: 2<br> Date: Wed, 28 Oct 2015 08:21:55 -0700<br> From: Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>><br> To: OpenTheory users <<a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a>><br> Subject: Re: [opentheory-users] Error loading articles<br> Message-ID:<br> <CACQy07nwYDX-ukd1Am98r0owrAMUR8A6T5MPkbx-n6qPc=<a href="mailto:Jtkw@mail.gmail.com">Jtkw@mail.gmail.com</a>><br> Content-Type: text/plain; charset=UTF-8<br> <br> Hi Robert,<br> <br> I've now updated the hacking document: the changes are awaiting your approval.<br> <br> I also remembered that to use the new import functionality you'll also<br> need to upgrade your theories using<br> <br> opentheory update<br> opentheory upgrade<br> <br> The new version of the theories contain the HOL Light theorem names,<br> and I also changed the format of the HOL Light symbol name mapping so<br> you'll likely get errors if you try to import earlier versions of the<br> theories.<br> <br> Cheers,<br> <br> Joe<br> <br> On Wed, Oct 28, 2015 at 8:10 AM, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote:<br> > Hi Robert,<br> ><br> >> 1) Here is the first problem: I can't import modular theory<br> >><br> >> opentheory: unknown switch "--directory"<br> ><br> > I needed to add an extra switch to the opentheory tool that returned<br> > the directory in which the theory file lives:<br> ><br> > $ opentheory info --directory base<br> > /Users/joe/.opentheory/packages/base-1.200<br> ><br> > If you upgrade your opentheory tool to the latest release this switch<br> > should be recognized.<br> ><br> >> 2) I also noticed that you removed start_logging();; Then how should I<br> >> export the proofs. Could you please give me an example or maybe update the<br> >> hacking doc?<br> ><br> > Yes, I did some simple renamings to consistently export the various<br> > parts of a theory. I've already updated the FAQ:<br> ><br> > <a href="http://www.gilith.com/research/opentheory/faq.html#export-from-hol-light" rel="noreferrer" target="_blank">http://www.gilith.com/research/opentheory/faq.html#export-from-hol-light</a><br> ><br> > I'll also update the hacking doc shortly.<br> ><br> > Cheers,<br> ><br> > Joe<br> <br> <br> <br> ------------------------------<br> <br> Subject: Digest Footer<br> <br> _______________________________________________<br> opentheory-users mailing list<br> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br> <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br> <br> <br> ------------------------------<br> <br> End of opentheory-users Digest, Vol 39, Issue 17<br> ************************************************<br> </blockquote></div><br><br clear="all"><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 dir="ltr"><div dir="ltr"><div dir="ltr"><div><br></div><div>Regards,</div><div>Robert </div><div><br></div><div>New homepage at Github: <a href="https://airobert.github.io/" target="_blank">https://airobert.github.io/</a><br></div><div><span style="font-size:12.8px">New email address at ILLC: </span><a href="mailto:shuai.wang@student.uva.nl" style="font-size:12.8px" target="_blank">shuai.wang@student.uva.nl</a><br></div><div><span style="font-size:12px;line-height:20px">Carolina MacGillavrylaan </span><span style="font-size:12px;line-height:20px">2246</span><span style="font-size:12px;line-height:20px"> , 1098 XK AMSTERDAM HP: </span><span style="color:rgb(20,24,35);font-family:helvetica,arial,sans-serif;font-size:13px;line-height:17.94px;white-space:pre-wrap">0652691901</span><br></div><div><br></div></div></div></div></div></div></div></div></div></div></div></div> </div>