<div dir="ltr"><div>You don't need to build Agda with profiling, only the program that you wanted to profile.</div><div><br></div><div>/ Ulf<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Feb 3, 2021 at 12:02 AM <<a href="mailto:mechvel@scico.botik.ru">mechvel@scico.botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On 2021-02-01 10:42, Ulf Norell wrote:<br>
> You pass `--enable-library-profiling` to `cabal`. To make libraries<br>
> install with profiling<br>
> by default you can add `library-profiling: True` to `~/.cabal/config`.<br>
> <br>
> There are some issues with the new way cabal works and compiling Agda<br>
> programs<br>
> (see <a href="https://github.com/agda/agda/issues/4627" rel="noreferrer" target="_blank">https://github.com/agda/agda/issues/4627</a>), so I would try<br>
> <br>
>    cabal v1-install ieee754 --enable-library-profiling<br>
<br>
<br>
<br>
I add `library-profiling: True` to  ~/.cabal/config<br>
and command<br>
   > cabal install --enable-library-profiling<br>
<br>
to install Agda 2.6.1.1 (MAlonzo, ghc-8.8.3, Ubuntu Linux 18.04).<br>
This ends up with<br>
<br>
------------------------------------------------------<br>
src/full/Agda/Utils/Memo.hs:8:1: error:<br>
     Could not find module ‘Data.HashMap.Strict’<br>
     Perhaps you haven't installed the profiling libraries for package <br>
‘unordered-containers-0.2.10.0’?<br>
     ...<br>
8 | import qualified Data.HashMap.Strict as HMap<br>
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^<br>
src/full/Agda/Utils/Memo.hs:9:1: error:<br>
     Could not find module ‘Data.Hashable’<br>
     Perhaps you haven't installed the profiling libraries for package <br>
‘hashable-1.3.0.0’?<br>
---------------------------------------------------------<br>
<br>
Then I command<br>
   > cabal v1-install unordered-containers-0.2.10.0 <br>
--enable-library-profiling<br>
<br>
and it reports "Already installed. Use --reinstall if you want to <br>
reinstall anyway."<br>
The same is with  hashable-1.3.0.0.<br>
Then,<br>
   > cabal install --enable-library-profiling<br>
<br>
has the same effect.<br>
Need I to apply --reinstall to the above two packages?<br>
<br>
--<br>
SM<br>
<br>
<br>
<br>
> <br>
> On Sun, Jan 31, 2021 at 10:23 PM <<a href="mailto:mechvel@scico.botik.ru" target="_blank">mechvel@scico.botik.ru</a>> wrote:<br>
> <br>
>> On 2021-01-29 09:05, Ulf Norell wrote:<br>
>>> Hi Sergei,<br>
>>> <br>
>>> Agda compiles via Haskell so you can use all the Haskell profiling<br>
>>> tools on the code generated by Agda.<br>
>> <br>
>> I tried<br>
>>> agda -c $agdaLibOpt --ghc-flag=-prof Foo.agda<br>
>> <br>
>> , where "-prof" is a flag for compiling with profiling by  ghc<br>
>> (8.8.3).<br>
>> It reports<br>
>> <br>
>> Compiling MAlonzo.RTE      ( MAlonzo/RTE.hs, MAlonzo/RTE.o )<br>
>> ...<br>
>> MAlonzo/RTE.hs:9:1: error:<br>
>> Could not find module ‘Numeric.IEEE’<br>
>> Perhaps you haven't installed the profiling libraries for<br>
>> package<br>
>> ‘ieee754-0.8.0’?<br>
>> <br>
>> Need I to download the package  ieee754-0.8.0.tar.gz  for Haskell<br>
>> and<br>
>> somehow<br>
>> `make' it with profiling?<br>
>> There are the files  ieee754.cabal and Setup.lhs.<br>
>> Need I to do<br>
>>> cabal install<br>
>> ?<br>
>> How to specify "with profiling"?<br>
>> May be to set somewhere to  Setup.lhs  "-enable-library-profiling" ?<br>
>> <br>
>> (it may occur hundreds of packages that may need to rebuild with<br>
>> profiling - ?).<br>
>> <br>
>> Thanks,<br>
>> <br>
>> ------<br>
>> Sergei<br>
</blockquote></div>