[Agda-dev] Agda Compiler Alterations Guide :: Notes
Andreas Abel
abela at chalmers.se
Wed Oct 3 09:41:15 CEST 2018
I did small tutorials how to fix a bug in Agda on the Agda meetings,
here are some brief notes:
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=DevelopersManual.BugFixing
This includes at least a rought picture over the main pipeline (from
Parsing to Compilation) in Agda.
Otherwise, some developer's notes are in
https://github.com/agda/agda/blob/master/HACKING
On 02/10/18 20:30, Guillaume Brunerie wrote:
> One suggestion would be that you browse the commit history on github,
> look at the commits that are touching the same parts of Agda that you're
> interested in, and try to understand the changes made by the author of
> the commit.
> You will most likely learn a lot in this way.
>
> Den tis 2 okt. 2018 18:15Musa Al-hassy <alhassy at gmail.com
> <mailto:alhassy at gmail.com>> skrev:
>
> Going to the language's Implementors meeting --on a whole other
> continent-- seems rather unreasonable to obtain
> minimal direction on altering the compiler. I want to work on the
> compiler, but I don't have superfluous funds.
>
> Once again, I appeal to the community: Surely someone has jotted
> down some messy
> notes on how to make alterations; anything helps, such as how the
> system is interconnected
> or where a reasonable place to begin and work from!
>
> Honestly, anything helps!
>
> This is an opportunity to get some manual made for others to contribute.
> People have things on the Agda ``wish list'', and people like me
> might realise
> them if guiding manuals were in-place.
>
> On Tue, Oct 2, 2018 at 10:19 AM Andreas Abel <abela at chalmers.se
> <mailto:abela at chalmers.se>> wrote:
> >
> > > Does anyone have notes, or knows how to, or can provide a guide
> > > to making alterations to the Agda compiler.
> >
> > Well, we know how to, but have not anything written down. The Agda
> > meeting is a place for getting insider information.
> >
> > http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AIMXXVIII
> >
> > > My steps and code can be found at https://github.com/alhassy/agda
> >
> > I commented here:
> >
> https://github.com/alhassy/agda/commit/6043e77e4a72518711f5f808fb4eb593cbf0bb7c#commitcomment-30735013
> >
> > On 02/10/18 15:15, Musa Al-hassy wrote:
> > > Dear Agda Community,
> > >
> > > Does anyone have notes, or knows how to, or can provide a guide
> > > to making alterations to the Agda compiler.
> > >
> > > I would like to experiment with adding record declaration
> combinators.
> > > In general, I am trying to add some meta-programming features that
> > > would generate new declarations based on existing declarations,
> > > somewhat like Haskell's deriving (or deriving-via).
> > >
> > > To elaborate further on what I'm really trying to accomplish,
> consider:
> > >
> > > record SingleSortedAlgebra : Set₁ where
> > > field
> > > Carrier : Set
> > > _⊕_ : Carrier → Carrier → Carrier
> > >
> > > One of my aims is to introduce construct “fields-of”:
> > >
> > > record SingleSortedAlgebraWithConstant : Set₁ where
> > > fields-of SingleSortedAlgebra renaming (_⊕_ to _⟨$⟩_)
> > > field
> > > ε : Carrier
> > >
> > > Which should have the same net result as:
> > >
> > > record SingleSortedAlgebraWithConstant : Set₁ where
> > > field
> > > Carrier : Set
> > > _⟨$⟩_ : Carrier → Carrier → Carrier
> > > ε : Carrier
> > >
> > > I have been unsuccessful in locating any documentation to help
> me achieve
> > > such changes to the Agda compiler. If you know of any, please
> send them my way.
> > >
> > > I have been trying to make super simple changes, like aliases
> for keywords,
> > > and have been unsuccessful for some time.
> > > In particular, to make an observable change I wanted the compiler
> > > to accept the keyword `mmodule` in place of the existing
> `module` keyword.
> > > I grep'd for "module" in the agda source, including in the alex
> and happy files,
> > > prepended the strings with an extra `m`, then re-compiled and
> re-built
> > > everything.
> > > The result was a broken agda sytem: A file containing only `mmodule
> > > silly1 where`
> > > could no longer type check with module name and file name
> errors; even though
> > > the file name was silly1.agda.
> > >
> > > My steps and code can be found at https://github.com/alhassy/agda
> > >
> > > My current aim is to provide renaming of record fields, that
> would provide
> > > an isomorphic record declaration but with some fields renamed,
> as a starting
> > > point. [I am well aware of Agda's renaming features when
> opening a module;
> > > this is different, as it is about generating new declarations].
> > >
> > > Any advice would be appreciated --any existing notes would be
> immensely helpful!
> > >
> > > Best regards,
> > >
> > > Musa Al-hassy
> > > _______________________________________________
> > > Agda-dev mailing list
> > > Agda-dev at lists.chalmers.se <mailto:Agda-dev at lists.chalmers.se>
> > > https://lists.chalmers.se/mailman/listinfo/agda-dev
> > >
> >
> > --
> > Andreas Abel <>< Du bist der geliebte Mensch.
> >
> > Department of Computer Science and Engineering
> > Chalmers and Gothenburg University, Sweden
> >
> > andreas.abel at gu.se <mailto:andreas.abel at gu.se>
> > http://www.cse.chalmers.se/~abela/
> <http://www.cse.chalmers.se/%7Eabela/>
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se <mailto:Agda-dev at lists.chalmers.se>
> https://lists.chalmers.se/mailman/listinfo/agda-dev
>
>
>
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
>
--
Andreas Abel <>< Du bist der geliebte Mensch.
Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden
andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/
More information about the Agda-dev
mailing list