[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 have a library Foo of many .agda modules,
and have a certain  KTest.agda  that is in Foo, depends on a lot of 
modules of Foo.
I compile and run  KTest  by

   > agda -c $agdaLibOpt KTest.agda
   > ./KTest

I never used a *.cabal file to type-check and compile my Foo library.
The above  `> agda'  command does everything.

Can people explain: why does one need cabal for this?

Further, I need to `make' KTest and run it with profiling.
And probably you say that for this it is not sufficient to run the 
command
   > agda -c <flags> KTest.agda

Right?
You say that it is needed
a) to create a certain  foo.cabal,
b) to add to foo.cabal  `--enable-library-profiling'
    (somewhere to the compilation flags section),
c) to run
    > cabal install
    in the folder where  foo.cabal  resides.
Do you?

If so, then can you, please, advise, how does this  foo.cabal  need to 
look?

Thanks,

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