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