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

[Joe Leslie-Hurd]

Hi Robert,

Unfortunately you can't update the opentheory tool itself using
opentheory update, 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

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
>