<div dir="ltr"><div>I suggested installing ieee754 with profiling enabled. I didn't say anything about setting up a</div><div> .cabal file for your project (although, that is certainly a thing that one can do).</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 10:51 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>
I have a library Foo of many .agda modules,<br>
and have a certain  KTest.agda  that is in Foo, depends on a lot of <br>
modules of Foo.<br>
I compile and run  KTest  by<br>
<br>
   > agda -c $agdaLibOpt KTest.agda<br>
   > ./KTest<br>
<br>
I never used a *.cabal file to type-check and compile my Foo library.<br>
The above  `> agda'  command does everything.<br>
<br>
Can people explain: why does one need cabal for this?<br>
<br>
Further, I need to `make' KTest and run it with profiling.<br>
And probably you say that for this it is not sufficient to run the <br>
command<br>
   > agda -c <flags> KTest.agda<br>
<br>
Right?<br>
You say that it is needed<br>
a) to create a certain  foo.cabal,<br>
b) to add to foo.cabal  `--enable-library-profiling'<br>
    (somewhere to the compilation flags section),<br>
c) to run<br>
    > cabal install<br>
    in the folder where  foo.cabal  resides.<br>
Do you?<br>
<br>
If so, then can you, please, advise, how does this  foo.cabal  need to <br>
look?<br>
<br>
Thanks,<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>