HACKING

Working with Git

* Maintenance branches.

  For old releases (starting with 2.4.0) there are maintenance branches
  maint-X.Y.Z. Bug fixes should be based on the appropriate maintenance branch
  whenever possible. See below.

* Branches should be used generously when fixing bugs and adding features.
  Whenever possible bug fix branches should be based on the latest maintenance
  branch rather than the master branch.  For instance, fixing issue 1234 would
  work as follows:

    git checkout maint-2.4.0
    git checkout -b issue1234 # create a new branch based on maint-2.4.0
    ... work on issue 1234 ...
    git commit -p             # record some patches

    # If you have commit rights
    git checkout maint-2.4.0
    git merge issue1234       # merge into maint-2.4.0
    git push
    git checkout master
    git merge issue1234       # merge into master
    git push
    git branch -d issue1234   # delete the branch

    # Otherwise, push branch to your GitHub fork of Agda and create a pull
    # request.
    git push -u myfork issue1234
    Go to https://github.com/agda/agda and click the green button next to the
    branch dropdown.

  For new features replace maint-2.4.0 with master above.

Some Agda Hacking Lore

* Whenever you change the interface file format you should update
  Agda.TypeChecking.Serialise.currentInterfaceVersion.

* When a new feature is implemented it should be documented in
  doc/release-notes/<next-version>.txt. It is also a good idea to add
  test cases under test/succeed and test/fail, and maybe also
  test/interaction. When adding test cases under test/fail, remember
  to record the error messages (.err files) after running make test.

* Run the test-suite, using make test (which does not work properly
  unless you run autoreconf and ./configure first).

  Tests under test/fail can fail if an error message has changed. To
  accept the new error message, touch the corresponding source file.

* Under darcs 2.5 the --test flag is not enabled by default. This can
  be changed by adding the following line to _darcs/prefs/defaults:

    ALL test

* To avoid problems with the whitespace test failing you can add the
  following line to _darcs/prefs/defaults:

    record prehook make fix-whitespace

* Use __IMPOSSIBLE__ instead of calls to error. __IMPOSSIBLE__
  generates errors of the following form:

   An internal error has occurred. Please report this as a bug.
   Location of the error: ...

  Calls to error can make Agda fail with an error message in the *ghci*
  buffer.

Emacs mode

* Load times (wall-clock time) can be measured using
  agda2-measure-load-time.

* If you fix a bug related to syntax highlighting, please add a test
  case under test/interaction. Example .in file command:

    IOTCM "Foo.agda" NonInteractive Direct (Cmd_load "Foo.agda" [])

  If you want to include interactive highlighting directives, replace
  NonInteractive with Interactive.