[opentheory-users] format of opentheory parameters

[Joe Leslie-Hurd]

[cc'ing the opentheory mailing list]

Hi Gunter,

I've just finished investigating this issue, and discovered that the
opentheory tool had some hidden constraints:

1. For a FILE.thy to be recognized as a theory, FILE had to be a valid
package name.

2. For a FILE.tgz to be recognized as a tarball, FILE had to be a
valid package name-version.

These hidden constraints are simply confusing and serve no useful
purpose that I can discover, so I have removed them and released a new
version of the opentheory tool.

Your original invocation

opentheory info two_c.thy

should now work just fine (even though two_c is not a valid package name).

Thank you for the bug report,

Joe




On Sat, Aug 15, 2015 at 10:44 AM, Günter Rote <rote at inf.fu-berlin.de> wrote:
> Am 15.08.2015 um 19:35 schrieb Joe Leslie-Hurd:
>> [cc'ing the opentheory mailing list]
>>
>> Hi Gunter,
>>
>>> INPUT is one of the following:
>>>   - A package: NAME-VERSION or NAME (for the latest version)
>>>   - A theory source file: FILE.thy or theory:FILE
>>>   - ...
>>
>> What this meant to say (and I agree it's not crystal clear) is that if
>> the file has an extension .thy it will be treated by default as a
>> theory file, but you can treat any other file as a theory file by
>> prepending theory: to the name of the file. So if you have a theory
>> file two_c.thy you can process it just using
>>
>> opentheory info two_c.thy
>>
>> but if you have a theory file called two_c.txt then you will need to
>> prepend theory: for the opentheory tool to properly interpret it:
>
> Yes, that is how I understood it.
>
>> opentheory info theory:two_c.txt
>>
>>>> opentheory info two_c.thy
>>> triggers
>>> opentheory: unknown type of input: two_c.thy
>>
>> In the light of the above, this error is very strange. What platform are you on?
>
> Gnu/Linux, more specifically Ubuntu 12.04
> I have compiled opentheory with the mlton compiler.
>
>