<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On 30 October 2015 at 14:44, 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, Unfortunately you can't update the opentheory tool itself using opentheory update,</blockquote><div> </div><div>I don't think this is unfortunate at all. Tools which attempt to update themselves don't play nicely with package managers. </div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> you have to reinstall it. If you're tracking the development version then you can update by following these instructions: <a href="http://src.gilith.com/opentheory.html" rel="noreferrer" target="_blank">http://src.gilith.com/opentheory.html</a> Otherwise you will have to download and build from the release site: <a href="http://www.gilith.com/software/opentheory/download.html" rel="noreferrer" target="_blank">http://www.gilith.com/software/opentheory/download.html</a> </blockquote><div> </div><div>Or use a package, if there is one, for your package manager. </div><div>For example, for Arch Linux: <a href="https://aur.archlinux.org/packages/opentheory">https://aur.archlinux.org/packages/opentheory</a>. </div><div> </div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> Cheers, Joe On Thu, Oct 29, 2015 at 3:11 PM, Robert White <div class="HOEnZb"><div class="h5"><<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> wrote: > Dear Joe, > > ----------------------------- > > $ 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 -v > > opentheory 1.3 (release 20150102) > > > Looks like I have to install it again then? > > > > On 29 October 2015 at 17:57, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote: >> >> 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 >> >> 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> > > > > > -- > > 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>