[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