[opentheory-users] interpretation in separate file

[Ramana Kumar]

Cool :) That looks good.

On 3 May 2016 at 13:51, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Ramana,
>
> Following your suggestion I've written documentation for the
> interpretation files:
>
> http://www.gilith.com/research/opentheory/interpretation.html
>
> I've also converted all of my theories on the Gilith repo to use
> interpretation files rather than interpret: lines, because it's easier
> to read and keep in sync with my HOL Light source theories.
>
> Cheers,
>
> Joe
>
> On Mon, Apr 25, 2016 at 11:54 PM, Joe Leslie-Hurd <joe at gilith.com> wrote:
> > Yes, the documentation could definitely be improved by describing
> > interpretation files. Your reverse engineering is quite correct, plus
> > comments are also allowed. For an example take a look at the
> > interpretation file used by the latest version of the byte-def theory:
> >
> > http://opentheory.gilith.com/opentheory/packages/byte-def-1.98/word.int
> >
> > Cheers,
> >
> > Joe
> >
> >
> >
> > On Mon, Apr 25, 2016 at 11:30 PM, Ramana Kumar <ramana at member.fsf.org>
> wrote:
> >> 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
> >>
> >>
> >>
> >> _______________________________________________
> >> 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/20160503/2c843a23/attachment-0001.html>