[opentheory-users] interpretation in separate file

[Ramana Kumar]

Hi Joe,

Thanks for implementing this!

I think the documentation isn't very clear about what interpretation files
should contain. However, I think I figured it out to some extent: They
should have lines like the "interpret:" lines except without the leading
"interpret:", and blank lines are allowed.

I'm trying it out more now, and will let you know if I run into anything.

Cheers,
Ramana

On 24 April 2016 at 16:58, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Ramana,
>
> The latest version of the opentheory tool (release 20160423) now
> includes support for
>
> interpretation: "file.int"
>
> lines in theory files, as documented here:
>
> http://www.gilith.com/research/opentheory/theory.html
>
> It's lightly tested, so please let me know if you discover anything
> odd with the new feature.
>
> Cheers,
>
> Joe
>
> On Wed, Apr 20, 2016 at 9:37 PM, Ramana Kumar <ramana at member.fsf.org>
> wrote:
> > Cool. Thanks!
> >
> > On 21 April 2016 at 02:40, Joe Leslie-Hurd <joe at gilith.com> wrote:
> >>
> >> 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
> >> >>
> >>
> >> _______________________________________________
> >> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20160426/0202f874/attachment.html>