-
Notifications
You must be signed in to change notification settings - Fork 0
/
HACKING
413 lines (296 loc) · 13.7 KB
/
HACKING
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
Working with Git (from 2013-06-15)
Stable branches
--------------------
For old releases (starting with 2.5.1) there are stable branches
stable-$VERSION, where e.g. VERSION=2.5.
Bug fixes should be based on the appropriate stable branch whenever
possible. See below.
Branches
---------
Branches should be used generously when fixing bugs and adding
features. Whenever possible bug fix branches should be based on the
latest stable branch rather than the master branch. For instance,
fixing issue 1234 would work as follows:
git checkout stable-$VERSION
git checkout -b issue1234 # create a new branch based on stable-$VERSION
... work on issue 1234 ...
git commit -p # record some patches
... working for a long time on issue 1234 ...
git rebase stable-$VERSION # get fresh upstream patches, keep own work on top
git commit -p # record some more patches
make install-bin test # ensure compilation and tests
# Done! If you have commit rights:
## Merge into stable
git checkout stable-$VERSION
git merge issue1234 # merge into stable-$VERSION
make install-bin test # ensure compilation and tests
git push
## Merge into master
git checkout master
git merge issue1234 # merge into master
make install-bin test # ensure compilation and tests
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 stable-$VERSION with master above.
The above procedure has the drawback that with each checkout, many
source files are touched and recompilation is slow. Here is an
alternative workflow, if you have commit rights and two local
repositories, one on master and one on stable-$VERSION (both
up-to-date).
stable$ git checkout -b issue1234
stable$ git commit ...
stable$ git checkout stable-$VERSION
stable$ git merge issue1234
stable$ make install-bin test
stable$ git push
stable$ git branch -d issue1234
# Now fast-forward stable-$VERSION branch without checking it out.
# Merge it into master (assuming stable-$VERSION is a `subset' of master).
master$ git fetch origin stable-$VERSION:stable-$VERSION
master$ git pull
master$ git merge stable-$VERSION
master$ make install-bin test
master$ git push
# Fast-forward master
stable$ git fetch origin master:master
stable$ git pull
Finding the commit that introduced a regression
-----------------------------------------------
If you want to find the commit that introduced a regression that
caused Module-that-should-be-accepted to be rejected, then you can
try the following recipe:
git clone <agda repository> agda-bug
cd agda-bug
git checkout <suitable branch>
cabal sandbox init
git bisect start <bad commit> <good commit>
cp <some path>/Module-that-should-be-accepted.agda .
git bisect run sh -c \
"cabal install --force-reinstalls \
--disable-library-profiling \
--disable-documentation || exit 125; \
.cabal-sandbox/bin/agda --ignore-interfaces \
Module-that-should-be-accepted.agda"
An alternative is to use the program agda-bisect from
src/agda-bisect:
git clone <agda repository> agda-bug
cd agda-bug
cp <some path>/Module-that-should-be-accepted.agda .
agda-bisect --bad <bad commit> --good <good commit> \
Module-that-should-be-accepted.agda
See agda-bisect --help for usage information.
The following command temporarily enables Bash completion for
agda-bisect:
source < (agda-bisect --bash-completion-script `which agda-bisect`)
Bash completion can perhaps be enabled more permanently by storing
the output of the command above in a file in a suitable directory
(like /etc/bash_completion.d/).
Cherry-picking a commit from master into stable
------------------------------------------------
For cherry-picking the commit 123 from master into stable, you can use
the follow instructions:
* To create two local repositories, one on master and one on
stable (both up-to-date).
* Fetch the local master from the local stable
agda-stable$ git fetch ~/agda-master
* Cherry-pick the commit 123 into the local stable
agda-stable$ git cherry-pick -x 123
* Merge the local stable into the local master
agda-master$ git fetch ~/agda-stable
agda-master$ git merge FETCH_HEAD
* Push both local repositories
agda-stable$ git push
agda-master$ git push
Standard library submodule
--------------------------
* A large part of the test suite involves the standard library.
Each version of Agda is deemed compatible with a corresponding version of the
standard library.
* Each commit in the main Agda repository has a reference to a branch and a
commit in the standard library repository. The tests are run using this
referenced version of the standard library.
+ The file `/.gitmodules` contains the URL of the standard library
repository and the name of the branch.
+ The path `/std-lib` is treated by git as a file containing the hash of the
referenced commit.
* To obtain the referenced version of the standard library, run:
make std-lib
* To obtain and install the referenced version of the standard library, run:
make up-to-date-std-lib
* To obtain and install the newest version of the standard library for the
referenced branch, run:
make fast-forward-std-lib
If the new version of the standard library also passes all tests, you can
have the repository point to it:
git add std-lib
git commit
* The standard library is tracked as a git submodule, which means that the
`/std-lib` subdirectory will appear as a git repository in a detached-HEAD
state.
To avoid this, you may run, inside the submodule directory:
git checkout <branch name>
and then, from the root directory:
git submodule update --remote [--merge|--rebase]
See: https://www.git-scm.com/book/en/v2/Git-Tools-Submodules
Testing and documentation
-------------------------
* When you implement a new feature it needs to be documented in
doc/user-manual/ and 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. Maybe you want to build
using `make' first as well.
* Additional options for the tests using the Haskell/tasty test runner
can be given using AGDA_TESTS_OPTIONS. By default,
the interactive mode (-i) is used and the number of parallel tests
to run (-j) is set to the number of CPU cores.
You can select certain tests to run by using the "-p" pattern option.
For example, to only run the simple MAlonzo compiler tests, you
can use the following command:
make AGDA_TESTS_OPTIONS="-i -j8 -p MAlonzo/simple" compiler-test
You can use the AGDA_ARGS environment variable to pass additional
arguments to Agda when executing the Succeed/Fail/Compiler tests.
* 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.
* Tests under test/Succeed will also be tested for expected warning
messages if there is a corresponding .warn file. If you want to
record a new warning, touch the .warn file, run make succeed and
accept the new golden value.
* 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.
* You can obtain a simple profile by using -vprofile:7. This works
also in the Emacs mode, output goes to the *Agda debug* buffer. Note
that the -vprofile:7 option is /not/ supposed to be given in an
OPTIONS pragma, use agda2-program-args.
* 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
* To build the user manual locally, you need to install
the following dependencies:
- Python >=3.3
- Sphinx and sphinx-rtd-theme
pip install --user -r doc/user-manual/requirements.txt
Note that the `--user` option puts the Sphinx binaries in
`$HOME/.local/bin`.
- LaTeX
To see the list of available targets, execute `make help`
in doc/user-manual. E.g., call `make html` to build the
documentation in html format.
* Running the test-suite using Cabal sandboxes
If the sandbox uses for example the directory
`dist/dist-sandbox-12345` you can run the test-suite using the
following commands:
export AGDA_BIN=dist/dist-sandbox-12345/build/agda/agda
export AGDA_TESTS_BIN=dist/dist-sandbox-12345/build/agda-tests/agda-tests
make test
Internal test-suite
-------------------
The internal test-suite is used for testing the Agda library (which
after closing Issue #2083 doesn't use the QuickCheck library).
The test-suite uses the same directory structure than the Agda
library.
A new internal test or a new QuickCheck instance, i.e. instances of
`Arbitrary` or `CoArbitrary`, for a module
Agda.Foo.Bar
should be added into the module
InternalTests.Foo.Bar
in the internal test-suite.
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.
* GHC warnings are turned on globally in Agda.cabal. If you want to
turn on or off an individual warning in a specific file, use an
OPTIONS_GHC pragma. Don't use -Wall, because the meaning of this
flag can vary between different versions of GHC.
* The GHC documentation (7.10.1) contains the following information
about orphan instances:
"GHC identifies orphan modules, and visits the interface file of
every orphan module below the module being compiled. This is
usually wasted work, but there is no avoiding it. You should
therefore do your best to have as few orphan modules as possible."
https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/separate-compilation.html#orphan-modules
In order to avoid /unnecessary/ orphan instances the flag
-fwarn-orphans is turned on. If you feel that you really want to use
an orphan instance, place
{-# OPTIONS_GHC -fno-warn-orphans #-}
at the top of the module containing the instance.
Haskell-mode and the Agda codebase
-----------------------------------
* If you're using a recent haskell-mode (use `M-x package-install
haskell-mode' to be sure, what's packaged by debian is not enough),
and you're editing an Haskell file, you can load it up in by tapping
`C-c C-l', and agreeing to emacs proposals about paths and whatsnot.
You can toggle from :load to :reload with `C-u C-c C-l', which you
probably want since otherwise you'll load up the world each time.
You have semantic jumps with `M-.'. No more pesky T.A.G.S.!
You can jump to errors and warnings with `C-x `'. You can probably do
many other things, emacs is your oyster.
One little caveat: GHCi needs some generated files to work. To make
sure you have them, you can issue `cabal build' and kill it when it
starts compiling modules. There doesn't seem to be a programmatic way
to instruct cabal to do so. They're pretty stable so you don't have
to do that often.
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")))))))
Cabal stuff
-----------
* For running cabal repl use the following command (see
https://code.google.com/p/agda/issues/detail?id=1196):
cabal repl --ghc-options=-Wwarn
Documentation
-------------
See http://agda.readthedocs.io/en/latest/contribute/documentation.html .