[Agda] type check performance

[Andrea Vezzosi]

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

Can we hope that in a garbage collected language like Haskell?

On Tue, Mar 31, 2015 at 4:58 PM, Nils Anders Danielsson <nad at cse.gu.se> wrote:
> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda