[opentheory-users] interpretation in separate file

[Joe Leslie-Hurd]

By the way, I am working on adding this feature, but for various
technical reasons of how the code is structured it's turning out to be
non-trivial. I'll let you know when the feature is added.

Cheers,

Joe

On Sun, Apr 3, 2016 at 10:16 PM, Joe Leslie-Hurd <joe at gilith.com> wrote:
> Sure thing, I'll work on adding this feature.
>
> Cheers,
>
> Joe
>
> On Fri, Apr 1, 2016 at 3:41 PM, Ramana Kumar <ramana at member.fsf.org> wrote:
>> Hi Joe,
>>
>> I would like to reopen this request. It seems like I'm going to be copying
>> interpretations around a lot again.
>>
>> Cheers,
>> Ramana
>>
>> On 4 March 2016 at 12:14, Ramana Kumar <ramana at member.fsf.org> wrote:
>>>
>>> Hi Joe,
>>>
>>> It turns out this is not so urgent for me since Michael and I came up with
>>> another method:
>>> Put all the article-combination stuff into one file uninterpreted.thy
>>> (main block is a union), then turn that into uninterpreted.art, and finally
>>> do the interpretation all at once (so it only appears in one file) in
>>> interpreted.thy, whose main block is an article block for
>>> "uninterpreted.art".
>>>
>>> However, interpretations from files would probably still be good for other
>>> scenarios. I would tweak your suggested syntax to use "interpretation"
>>> rather than "interpret-file", to match "article" (which also takes a
>>> filename).
>>>
>>> Cheers,
>>> Ramana
>>>
>>> On 5 March 2016 at 05:51, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>>>
>>>> Hi Ramana,
>>>>
>>>> I agree with you that it would be good for theory files to support
>>>> pulling in interpretations from files. How about the following syntax:
>>>>
>>>> interpret-file: "file.int"
>>>>
>>>> inside a theory block? It probably makes sense to allow multiple of
>>>> these, just like multiple
>>>>
>>>> interpret: type/const "X" as "Y"
>>>>
>>>> lines are allowed, but raise an error if the same symbol is
>>>> interpreted in multiple ways.
>>>>
>>>> Cheers,
>>>>
>>>> Joe
>>>>
>>>> On Thu, Mar 3, 2016 at 4:21 PM, Ramana Kumar <ramana at member.fsf.org>
>>>> wrote:
>>>> > Is it possible to include an interpretation in a theory file, rather
>>>> > than
>>>> > having to write it out inline? Since I sometimes want to include a
>>>> > rather
>>>> > large interpretation within multiple blocks within the same theory
>>>> > file, I
>>>> > end up having to write a template file and then generate the real .thy
>>>> > file
>>>> > from that, to avoid lots of copy-pasting. Is mine the recommended
>>>> > approach,
>>>> > or is there a better way?
>>>> >
>>>> > _______________________________________________
>>>> > opentheory-users mailing list
>>>> > opentheory-users at gilith.com
>>>> > http://www.gilith.com/opentheory/mailing-list
>>>> >
>>>>
>>>> _______________________________________________
>>>> opentheory-users mailing list
>>>> opentheory-users at gilith.com
>>>> http://www.gilith.com/opentheory/mailing-list
>>>
>>>
>>
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>>