HACKING

Working with Git (from 2014-06-15)

* 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.

Testing and documentation

* When you implement a new feature it needs to be documented in
  doc/release-notes/<next-version>.txt.
  When you fix a bug, drop a note in CHANGELOG.

* In both cases, you need to add regression tests
  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.
  You will be asked whether to accept the new error message.
  Alternatively, you can touch the corresponding source file, since,
  when the test case changes, it is assumed that the error message
  changes as well.

* Make sure you do not introduce performance regression.  If you

    make library-test

  you get a small table with benchmarks at the end.
  (Due to garbage collection, these benchmarks are not 100% stable.)
  Compare this with benchmarks before the new feature/bug fix.

* To avoid problems with the whitespace test failing we suggest add the
  following lines to .git/hooks/pre-commit

    echo "Starting pre-commit"
    make check-whitespace
    if [ $? -ne 0 ]; then
      exit 1
    fi
    echo "Ending pre-commit"

  You can fix the whitespace issues running

    make install-fix-agda-whitespace
    make fix-whitespace

Some Agda Hacking Lore

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

* 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.

* The following elisp code by Nils Anders Danielsson fixes whitespace
  issues upon save.  Add to your .emacs.

  (defvar fix-whitespace-modes
    '(text-mode agda2-mode haskell-mode emacs-lisp-mode LaTeX-mode TeX-mode)
    "*Whitespace issues should be fixed when these modes are used.")

  (add-hook 'before-save-hook
    (lambda nil
      (when (and (member major-mode fix-whitespace-modes)
                 (not buffer-read-only))
        ;; Delete trailing whitespace.
        (delete-trailing-whitespace)
        ;; Insert a final newline character, if necessary.
        (save-excursion
          (save-restriction
            (widen)
            (unless (equal ?\n (char-before (point-max)))
              (goto-char (point-max))
              (insert "\n")))))))


TODO: The following information is outdated, referring to darcs.  If
you know how to port these tips to git, update this 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