[opentheory-users] Error loading articles

[Joe Leslie-Hurd]

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