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

[Joe Leslie-Hurd]

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
>