[Agda] profiling

[Ulf Norell]

You don't need to build Agda with profiling, only the program that you
wanted to profile.

/ Ulf

On Wed, Feb 3, 2021 at 12:02 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 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210203/78a30440/attachment.html>