[Agda] type check performance

[Nils Anders Danielsson]

On 2015-03-31 16:14, Wolfram Kahl wrote:
> With that, Agda remains running while GHC is running, too...
> (The Agda process even remains quite active, but I don't know why.)

See Agda.Compiler.CallCompiler.callCompiler:

   -- | Calls a compiler:
   --
   -- * Checks the exit code to see if the compiler exits successfully.
   --   If not, then an exception is raised, containing the text the
   --   compiler printed to stderr (if any).
   --
   -- * Uses the debug printout machinery to relay any progress
   --   information the compiler prints to stdout.

> What I do to avoid having Agda and GHC fight for memory is passing
>
>    --ghc-flag="-abort"
>
> to Agda --- GHC implements the flag "-abort" by not recognising it ;-) .
> After Agda finishes and GHC bails out on the "-abort", I call GHC
> separately with a commend line derived from that displayed by Agda,
> with appropriate RTS arguments added.

Ouch.

I guess you would want Agda to just dump all its memory in some way
before calling GHC (perhaps using exec), but in other, less
memory-constrained cases this could be annoying (note that the compiler
can be called interactively from Emacs).

While the compiler is running Agda should only touch a small amount of
memory (unless the compiler prints lots of stuff to stdout/stderr), so I
would hope that the rest of the memory should be paged out, if
necessary.

I suggest that you perform an experiment. Replace callCompiler with a
procedure that does not capture the output, and see if this affects
performance. The following code should work:

   callCompiler cmd args = do
     exitcode <- liftIO $ rawSystem cmd args
     case exitcode of
       ExitSuccess   -> return ()
       ExitFailure _ -> typeError (CompilationError "<no message>")

-- 
/NAD