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

[Robert White]

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