[Agda] profiling

[Ulf Norell]

I suggested installing ieee754 with profiling enabled. I didn't say
anything about setting up a
.cabal file for your project (although, that is certainly a thing that one
can do).

/ Ulf

On Wed, Feb 3, 2021 at 10:51 AM <mechvel at scico.botik.ru> wrote:

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210203/a34c67b9/attachment.html>