[opentheory-users] Error loading articles

[Joe Leslie-Hurd]

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