[Agda] --jobs?

[Wolfram Kahl]

On Mon, Aug 25, 2014 at 08:14:39AM +0200, Ulf Norell wrote:
> In principle there's no problem (at least if you limit the parallelism to
> one thread per module, like ghc). In practice we need some non-trivial
> refactoring of the import chasing code. It's on the todo list.

Most of the time during interactive development, it is of course
a single module that is typechecked over and over again ---
how much opportunity for parallelisation is there in view of the
sequentialisation imposed by the the typecheking monad?
Are there perhaps actually places where you could just throw in
a `par` and see whether it helps?

I am routinely linking Agda with -threaded, and call it e.g. with -N4
on a six-core machine --- this currently has effect only on
garbage collection, but still results in small speed-ups with respect
to real time (at cost of increased user time).
(Even for the standard library, type checking with

   +RTS -N4 -H2G -M2G -RTS

 is faster than just omitting the -N4.
)


Wolfram