BugFixing

2011-04-08 Andreas AIM XIII

2014-05-22 Andreas AIM XIX

2016-04-20 Andreas AIM XXIII

Fixing bugs in Agda

0 Getting Agda

  git clone git@github.com:agda/agda

  The source code is under
    src/full/Agda/

  If you are making changes to be submitted as pull request

    * fork agda on github
    * clone your fork

1 The fix-agda-whitespace program

The fix-whitespace program fixes whitespace issues. It is found at

  src/fix-agda-whitespace

It is run when you

  make test

To install it, run

  make install fix-agda-whitespace

from the root of the agda repository.

2 General structure of Agda

  source file .agda

    == Interaction/Imports.hs ==>   
    == Syntax/Parser/Parser.y ==>

  Syntax/Concrete.hs  

    == Scope checking: Syntax/Translation/ConcreteToAbstract.hs ==>

  Syntax/Abstract.hs

    == Type checking: TypeChecking/Rules/ ==>

  Syntax/Internal.hs

    <== Termination checking: Termination/

    == Coverage checking, translation to case trees: TypeChecking/Coverage.hs ==>

  TypeChecking/CompiledClause.hs

    == TypeChecking/Serialize.hs ==>

  interface .agdai

2 Issue tracker

  https://github.com/agda/agda/issues

3 Bug fixing tools

a) Test suite, see

  test/Succeed/
  test/Fail/
  test/interaction/

etc. Run it (frequently) with

  make test

but latest before you commit.

b) TAGS

  make TAGS

  creates  src/full/TAGS

  M-.      go to definition
  C-u M-.  alternate location
  M-*      go back

c) poor man's tags: grepping the source files

  A script "findhs" with content

  
    #!/bin/bash
    gfind -name "*hs" -exec grep -H "$1" {} \; 2> /dev/null
 

  Then, in src/full/Agda do e.g.

  
    findhs getInteraction


   to get all matches in .hs files for "getInteraction".

   Alternative: use  M-x rgrep  in emacs.

d) debug messages

  in ScopeM or TCM report debug messages with

    reportSLn "class.of.message" <verbosity level> "text"
    reportSDoc "class.of.message" <verbosity level> $ prettyTCM expr

4 Test cases

  Each fixed issue is turned into (a) test case(s), to be put in one of

    test/Succeed
    test/Fail
    test/interaction

  The test case should contain comments with

    date
    author
    previous, faulty behavior
    current, expected behavior

5 Submitting a patch

  Make sure to include all test cases and all changed .err files from test/Fail
  and changed .out files from test/interaction.

  Mention the issue number (e.g. #2134) in the commit message header.

  Create a pull request on github.

  If no one responds to your pull request, pester the main developers.

Good luck!