Agda-2.3.2.2: HACKING

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.