[opentheory-users] opentheory-users Digest, Vol 39, Issue 17

[Ramana Kumar]

On 30 October 2015 at 14:44, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Robert,
>
> Unfortunately you can't update the opentheory tool itself using
> opentheory update,


I don't think this is unfortunate at all. Tools which attempt to update
themselves don't play nicely with package managers.



> you have to reinstall it. If you're tracking the
> development version then you can update by following these
> instructions:
>
> http://src.gilith.com/opentheory.html
>
> Otherwise you will have to download and build from the release site:
>
> http://www.gilith.com/software/opentheory/download.html
>
>
Or use a package, if there is one, for your package manager.
For example, for Arch Linux: https://aur.archlinux.org/packages/opentheory.



> Cheers,
>
> Joe
>
> On Thu, Oct 29, 2015 at 3:11 PM, Robert White
> <ai.robert.wangshuai at gmail.com> 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 <joe at gilith.com> 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
> >> <ai.robert.wangshuai at gmail.com> 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, <opentheory-users-request at gilith.com>
> >> > wrote:
> >> >>
> >> >> Send opentheory-users mailing list submissions to
> >> >>         opentheory-users at gilith.com
> >> >>
> >> >> To subscribe or unsubscribe via the World Wide Web, visit
> >> >>         http://www.gilith.com/opentheory/mailing-list
> >> >> or, via email, send a message with subject or body 'help' to
> >> >>         opentheory-users-request at gilith.com
> >> >>
> >> >> You can reach the person managing the list at
> >> >>         opentheory-users-owner at gilith.com
> >> >>
> >> >> 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 <joe at gilith.com>
> >> >> To: OpenTheory users <opentheory-users at gilith.com>
> >> >> Subject: Re: [opentheory-users] Error loading articles
> >> >> Message-ID:
> >> >>
> >> >> <CACQy07mOF=rDmrm2rqOymQSq504K8Gn7FdPBsr=ubYrmADynig at mail.gmail.com>
> >> >> 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:
> >> >>
> >> >>
> >> >>
> http://www.gilith.com/research/opentheory/faq.html#export-from-hol-light
> >> >>
> >> >> 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 <joe at gilith.com>
> >> >> To: OpenTheory users <opentheory-users at gilith.com>
> >> >> Subject: Re: [opentheory-users] Error loading articles
> >> >> Message-ID:
> >> >>
> >> >> <CACQy07nwYDX-ukd1Am98r0owrAMUR8A6T5MPkbx-n6qPc=Jtkw at mail.gmail.com>
> >> >> 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 <joe at gilith.com>
> >> >> 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:
> >> >> >
> >> >> >
> >> >> >
> http://www.gilith.com/research/opentheory/faq.html#export-from-hol-light
> >> >> >
> >> >> > I'll also update the hacking doc shortly.
> >> >> >
> >> >> > Cheers,
> >> >> >
> >> >> > Joe
> >> >>
> >> >>
> >> >>
> >> >> ------------------------------
> >> >>
> >> >> Subject: Digest Footer
> >> >>
> >> >> _______________________________________________
> >> >> opentheory-users mailing list
> >> >> opentheory-users at gilith.com
> >> >> http://www.gilith.com/opentheory/mailing-list
> >> >>
> >> >>
> >> >> ------------------------------
> >> >>
> >> >> End of opentheory-users Digest, Vol 39, Issue 17
> >> >> ************************************************
> >> >
> >> >
> >> >
> >> >
> >> > --
> >> >
> >> > Regards,
> >> > Robert
> >> >
> >> > New homepage at Github: https://airobert.github.io/
> >> > New email address at ILLC: shuai.wang at student.uva.nl
> >> > Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM  HP: 0652691901
> >> >
> >> >
> >> > _______________________________________________
> >> > opentheory-users mailing list
> >> > opentheory-users at gilith.com
> >> > http://www.gilith.com/opentheory/mailing-list
> >> >
> >>
> >> _______________________________________________
> >> opentheory-users mailing list
> >> opentheory-users at gilith.com
> >> http://www.gilith.com/opentheory/mailing-list
> >
> >
> >
> >
> > --
> >
> > Regards,
> > Robert
> >
> > New homepage at Github: https://airobert.github.io/
> > New email address at ILLC: shuai.wang at student.uva.nl
> > Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM  HP: 0652691901
> >
> >
> > _______________________________________________
> > opentheory-users mailing list
> > opentheory-users at gilith.com
> > http://www.gilith.com/opentheory/mailing-list
> >
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20151030/1a85c1f4/attachment-0001.html>