[Agda] profiling

[Ulf Norell]

You pass `--enable-library-profiling` to `cabal`. To make libraries install
with profiling
by default you can add `library-profiling: True` to `~/.cabal/config`.

There are some issues with the new way cabal works and compiling Agda
programs
(see https://github.com/agda/agda/issues/4627), so I would try

   cabal v1-install ieee754 --enable-library-profiling

/ Ulf

On Sun, Jan 31, 2021 at 10:23 PM <mechvel at scico.botik.ru> wrote:

> On 2021-01-29 09:05, Ulf Norell wrote:
> > Hi Sergei,
> >
> > Agda compiles via Haskell so you can use all the Haskell profiling
> > tools on the code generated by Agda.
>
>
> I tried
>    > agda -c $agdaLibOpt --ghc-flag=-prof Foo.agda
>
> , where "-prof" is a flag for compiling with profiling by  ghc (8.8.3).
> It reports
>
>   Compiling MAlonzo.RTE      ( MAlonzo/RTE.hs, MAlonzo/RTE.o )
>   ...
>   MAlonzo/RTE.hs:9:1: error:
>     Could not find module ‘Numeric.IEEE’
>     Perhaps you haven't installed the profiling libraries for package
> ‘ieee754-0.8.0’?
>
> Need I to download the package  ieee754-0.8.0.tar.gz  for Haskell and
> somehow
> `make' it with profiling?
> There are the files  ieee754.cabal and Setup.lhs.
> Need I to do
>     > cabal install
> ?
> How to specify "with profiling"?
> May be to set somewhere to  Setup.lhs  "-enable-library-profiling" ?
>
> (it may occur hundreds of packages that may need to rebuild with
> profiling - ?).
>
> Thanks,
>
> ------
> Sergei
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210201/257e0d96/attachment.html>