[Agda] profiling

[mechvel at scico.botik.ru]

On 2021-02-01 10:42, Ulf Norell wrote:
> 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



I add `library-profiling: True` to  ~/.cabal/config
and command
   > cabal install --enable-library-profiling

to install Agda 2.6.1.1 (MAlonzo, ghc-8.8.3, Ubuntu Linux 18.04).
This ends up with

------------------------------------------------------
src/full/Agda/Utils/Memo.hs:8:1: error:
     Could not find module ‘Data.HashMap.Strict’
     Perhaps you haven't installed the profiling libraries for package 
‘unordered-containers-0.2.10.0’?
     ...
8 | import qualified Data.HashMap.Strict as HMap
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
src/full/Agda/Utils/Memo.hs:9:1: error:
     Could not find module ‘Data.Hashable’
     Perhaps you haven't installed the profiling libraries for package 
‘hashable-1.3.0.0’?
---------------------------------------------------------

Then I command
   > cabal v1-install unordered-containers-0.2.10.0 
--enable-library-profiling

and it reports "Already installed. Use --reinstall if you want to 
reinstall anyway."
The same is with  hashable-1.3.0.0.
Then,
   > cabal install --enable-library-profiling

has the same effect.
Need I to apply --reinstall to the above two packages?

--
SM



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