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

[Robert White]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20151029/93191dff/attachment-0001.html>