<div dir="ltr"><div dir="ltr"><div>There is a `difficulty: easy` label on GitHub (no guarantees that it's always accurate though).</div><div><br></div><div>Otherwise, my advice would be to find something that you want to work on (rather than something that's</div><div>easy, but uninteresting), and start digging into the code base, asking questions here or on the agda-dev [1]</div><div>mailing list.</div><div><br></div><div>We don't have an "Introduction to the Agda code base" in the user manual, but it would certainly be a useful</div><div>resource.<br></div><div><br></div><div></div><div> / Ulf<br></div><div><br></div><div>[1] <a href="https://lists.chalmers.se/mailman/listinfo/agda-dev">https://lists.chalmers.se/mailman/listinfo/agda-dev</a></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Dec 13, 2019 at 9:04 AM Herminie Pagel <<a href="mailto:herminie.pagel@gmail.com">herminie.pagel@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">I had a similar issue and probably more people also.<br><br>I guess it would be great to have a kind of contributing guide for newcomers to agda depending on their interests, backgrounds, objectives...<br><br>A newcomer should be able to self-assess where does she stand now regarding agda, the things to which she can contribute right away, and maybe to be able to discover a learning path to where she wants to be in the future. Such a contributing guide should do the job. I don't know if something is on the way in that direction or even if it is possible/desirable to extend the user base of agda.<div><br></div><div>Best! herminie<br></div><div><br></div><div><br></div><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Am Do., 12. Dez. 2019 um 08:08 Uhr schrieb Marko Dimjašević <<a href="mailto:marko@dimjasevic.net" target="_blank">marko@dimjasevic.net</a>>:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Dear Agda community,<br>
<br>
I'm interested in contributing to Agda in code. So far I contributed<br>
tiny documentation fixes, but now I'd be interested in making bug fixes<br>
and implementing small improvements or features. Therefore, I'd<br>
appreciate a pointer to good first issues or equivalent. HACKING.md [1]<br>
doesn't seem to have pointers to such issues nor could I find related<br>
information anywhere else in the documentation.<br>
<br>
Do you use a particular label in the issue tracker for good first<br>
issues?<br>
<br>
I'm looking for something that could hopefully be done in a day or two.<br>
I've been using Haskell professionally for a year and a half so you can<br>
expect some proficiency.<br>
<br>
<br>
[1] <a href="https://github.com/agda/agda/blob/master/HACKING.md" rel="noreferrer" target="_blank">https://github.com/agda/agda/blob/master/HACKING.md</a><br>
<br>
<br>
-- <br>
Regards,<br>
Marko Dimjašević <<a href="mailto:marko@dimjasevic.net" target="_blank">marko@dimjasevic.net</a>><br>
<a href="https://dimjasevic.net/marko" rel="noreferrer" target="_blank">https://dimjasevic.net/marko</a><br>
PGP key ID:       056E61A6F3B6C9323049DBF9565EE9641503F0AA<br>
Learn email self-defense! <a href="https://emailselfdefense.fsf.org" rel="noreferrer" target="_blank">https://emailselfdefense.fsf.org</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div></div>