[Agda] profiling
mechvel at scico.botik.ru
mechvel at scico.botik.ru
Sun Jan 31 22:23:15 CET 2021
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
More information about the Agda
mailing list