Ticket #295 (assigned defect)

Opened 9 months ago

Last modified 8 months ago

haddock consumes too much memory

Reported by: abel Owned by: Fūzetsu
Priority: major Milestone:
Version: 2.15.0 Keywords:
Cc:

Description

Producing the doc for Agda (260 modules, 70 kloc) takes 2.5g of resident memory on my Ubuntu 12.04 Linux 64bit machine. This leads to thrashing unless I close all other big apps (like firefox). I do not need to close firefox when running ghc on Agda or running Agda on it's standard library.

Here the time stats (not very illuminating):

	Command being timed: "cabal haddock"
	User time (seconds): 283.54
	System time (seconds): 9.91
	Percent of CPU this job got: 89%
	Elapsed (wall clock) time (h:mm:ss or m:ss): 5:26.72
	Average shared text size (kbytes): 0
	Average unshared data size (kbytes): 0
	Average stack size (kbytes): 0
	Average total size (kbytes): 0
	Maximum resident set size (kbytes): 11120448
	Average resident set size (kbytes): 0
	Major (requiring I/O) page faults: 578
	Minor (reclaiming a frame) page faults: 3759501
	Voluntary context switches: 14902
	Involuntary context switches: 31922
	Swaps: 0
	File system inputs: 176104
	File system outputs: 356088
	Socket messages sent: 0
	Socket messages received: 0
	Signals delivered: 0
	Page size (bytes): 4096
	Exit status: 0

Size of documentation produced: 8m of .html

$ haddock --version
Haddock version 2.13.2, (c) Simon Marlow 2006
Ported to use the GHC API by David Waern 2006-2008

Here the full output:

$ /usr/bin/time --verbose cabal haddock
Running Haddock for Agda-2.3.3...
Preprocessing library Agda-2.3.3...
Warning: The documentation for the following packages are not installed. No
links will be generated to these packages: QuickCheck-2.6, binary-0.7.1.0,
boxes-0.1.3, rts-1.0, cpphs-1.17.1, data-hash-0.2.0.0, geniplate-0.6.0.3,
hashable-1.2.1.0, hashtables-1.1.2.1, haskeline-0.7.0.3,
haskell-src-exts-1.14.0, mtl-2.1.2, parallel-3.2.0.3, primitive-0.5.1.0,
random-1.0.1.1, split-0.2.2, strict-0.3.2, terminfo-0.3.2.5, text-0.11.3.1,
transformers-0.3.0.0, unordered-containers-0.2.3.3, vector-0.10.9.1,
xhtml-3000.2.1, zlib-0.5.4.1
Haddock coverage:
Warning: Agda-2.3.3:Agda.Utils.Maybe.Strict: Could not find documentation for exported module: Data.Strict.Maybe
  90% ( 19 / 21) in 'Agda.Utils.Maybe.Strict'
   0% (  0 /  2) in 'Agda.Utils.SemiRing'
   0% (  0 /  2) in 'Agda.TypeChecking.Monad.Debug'
  86% ( 12 / 14) in 'Agda.Utils.BiMap'
  50% (  1 /  2) in 'Agda.Utils.Pointed'
  85% ( 11 / 13) in 'Agda.Utils.VarSet'
   0% (  0 /  4) in 'Agda.Utils.Char'
  33% (  1 /  3) in 'Agda.Utils.Unicode'
  14% (  1 /  7) in 'Agda.Utils.Pointer'
  91% ( 10 / 11) in 'Agda.Utils.Functor'
 100% (  2 /  2) in 'Agda.Termination.CutOff'
  25% (  1 /  4) in 'Agda.Utils.Fresh'
 100% (  2 /  2) in 'Agda.Utils.IO.Binary'
  56% (  9 / 16) in 'Agda.Utils.Tuple'
  73% (  8 / 11) in 'Agda.Utils.Update'
   0% (  0 /  1) in 'Agda.Packaging.Types'
   0% (  0 /  1) in 'Agda.Packaging.Monad'
   0% (  0 /  1) in 'Agda.Packaging.Database'
   0% (  0 /  1) in 'Agda.Packaging.Config'
Warning: Agda-2.3.3:Agda.Utils.QuickCheck: Could not find documentation for exported module: Test.QuickCheck
   0% (  0 /  4) in 'Agda.Utils.QuickCheck'
 100% ( 20 / 20) in 'Agda.Utils.TestHelpers'
  67% (  6 /  9) in 'Agda.Termination.Semiring'
  95% ( 39 / 41) in 'Agda.Utils.PartialOrd'
  95% ( 38 / 40) in 'Agda.Utils.ReadP'
 100% (  4 /  4) in 'Agda.Utils.IO.UTF8'
  71% (  5 /  7) in 'Agda.Utils.Function'
  79% ( 22 / 28) in 'Agda.Utils.Graph.AdjacencyMap'
   0% (  0 /  7) in 'Paths_Agda'
 100% (  3 /  3) in 'Agda.Utils.Time'
Warning: Agda-2.3.3:Agda.Utils.HashMap: Could not find documentation for exported module: HashMap
   0% (  0 /  1) in 'Agda.Utils.HashMap'
  67% (  4 /  6) in 'Agda.Utils.String'
   0% (  0 /  2) in 'Agda.Utils.Size'
  43% (  3 /  7) in 'Agda.Utils.Pretty'
 100% (  7 /  7) in 'Agda.Interaction.EmacsCommand'
 100% ( 16 / 16) in 'Agda.Utils.Maybe'
 100% (  4 /  4) in 'Agda.Utils.Impossible'
   0% (  0 /  2) in 'Agda.ImpossibleTest'
  68% ( 26 / 38) in 'Agda.Utils.List'
  83% ( 35 / 42) in 'Agda.Utils.Graph.AdjacencyMap.Unidirectional'
  88% ( 14 / 16) in 'Agda.Utils.Permutation'
  89% (  8 /  9) in 'Agda.Utils.FileName'
  68% ( 30 / 44) in 'Agda.Syntax.Position'
  50% ( 29 / 58) in 'Agda.Syntax.Common'
   0% (  0 /  9) in 'Agda.Compiler.JS.Syntax'
   0% (  0 / 10) in 'Agda.Compiler.JS.Pretty'
   0% (  0 / 19) in 'Agda.Compiler.JS.Substitution'
   0% (  0 / 35) in 'Agda.Compiler.JS.Parser'
  12% (  6 / 50) in 'Agda.Utils.Warshall'
 100% ( 12 / 12) in 'Agda.Interaction.Highlighting.Range'
  33% (  2 /  6) in 'Agda.Utils.Hash'
  71% ( 24 / 34) in 'Agda.Syntax.Parser.Monad'
  77% ( 23 / 30) in 'Agda.Syntax.Concrete.Name'
   0% (  0 / 14) in 'Agda.Compiler.JS.Case'
  38% (  3 /  8) in 'Agda.Utils.Suffix'
  62% (  8 / 13) in 'Agda.Syntax.Notation'
  68% ( 13 / 19) in 'Agda.Syntax.Fixity'
  56% ( 23 / 41) in 'Agda.Syntax.Abstract.Name'
   0% (  0 /  2) in 'Agda.Syntax.Literal'
   0% (  0 /  5) in 'Agda.Syntax.Parser.Tokens'
  88% (  7 /  8) in 'Agda.Utils.Either'
  60% (  6 / 10) in 'Agda.Utils.Map'
  76% ( 16 / 21) in 'Agda.Utils.Favorites'
   3% (  2 / 61) in 'Agda.Auto.NarrowingSearch'
  29% ( 14 / 48) in 'Agda.Auto.Syntax'
   0% (  0 / 44) in 'Agda.Auto.SearchControl'
   3% (  1 / 37) in 'Agda.Auto.Typecheck'
   0% (  0 / 37) in 'Agda.Auto.CaseSplit'
  50% (  1 /  2) in 'Agda.Version'
 100% ( 13 / 13) in 'Agda.Utils.Trie'
 100% (  7 /  7) in 'Agda.TypeChecking.Monad.Base.Benchmark'
  74% ( 20 / 27) in 'Agda.Utils.Monad'
  72% ( 13 / 18) in 'Agda.Syntax.Parser.Alex'
 100% ( 14 / 14) in 'Agda.Syntax.Parser.LookAhead'
 100% (  3 /  3) in 'Agda.Syntax.Parser.StringLiterals'
 100% (  6 /  6) in 'Agda.Syntax.Parser.Comments'
  86% ( 12 / 14) in 'Agda.Syntax.Parser.Lexer'
 100% ( 25 / 25) in 'Agda.Syntax.Parser.LexActions'
 100% (  7 /  7) in 'Agda.Syntax.Parser.Layout'
  93% ( 28 / 30) in 'Agda.Termination.SparseMatrix'
  68% ( 13 / 19) in 'Agda.Termination.Order'
  83% ( 19 / 23) in 'Agda.Termination.CallMatrix'
  82% ( 18 / 22) in 'Agda.Termination.CallGraph'
  50% (  3 /  6) in 'Agda.Termination.Termination'
  54% (  7 / 13) in 'Agda.TypeChecking.Coverage.SplitTree'
  57% ( 12 / 21) in 'Agda.Interaction.Options'
  51% ( 27 / 53) in 'Agda.Syntax.Concrete'
   7% (  1 / 15) in 'Agda.Syntax.Concrete.Pretty'
  79% ( 58 / 73) in 'Agda.Syntax.Scope.Base'
  27% (  4 / 15) in 'Agda.Syntax.Info'
 100% (  4 /  4) in 'Agda.Utils.Geniplate'
  40% ( 24 / 60) in 'Agda.Syntax.Abstract'
  70% (  7 / 10) in 'Agda.Syntax.Abstract.Views'
  53% ( 49 / 92) in 'Agda.Syntax.Internal'
  41% (  7 / 17) in 'Agda.TypeChecking.Free'
  17% (  2 / 12) in 'Agda.Compiler.Epic.Interface'
  50% (  9 / 18) in 'Agda.Compiler.Epic.AuxAST'
  20% (  2 / 10) in 'Agda.TypeChecking.CompiledClause'
  83% (  5 /  6) in 'Agda.Syntax.Internal.Defs'
  33% (  1 /  3) in 'Agda.Syntax.Internal.Generic'
  58% (  7 / 12) in 'Agda.Syntax.Internal.Pattern'
  59% ( 10 / 17) in 'Agda.TypeChecking.Coverage.Match'
 100% (  5 /  5) in 'Agda.Syntax.Concrete.Generic'
  96% ( 27 / 28) in 'Agda.Interaction.Highlighting.Precise'
  50% (  5 / 10) in 'Agda.Syntax.Concrete.Definitions'
  57% ( 13 / 23) in 'Agda.Syntax.Concrete.Operators.Parser'
 100% (  5 /  5) in 'Agda.Syntax.Parser.Parser'
  64% (  9 / 14) in 'Agda.Syntax.Parser'
  67% (  2 /  3) in 'Agda.Interaction.Exceptions'
  35% ( 60 /170) in 'Agda.TypeChecking.Monad.Base'
  41% ( 28 / 68) in 'Agda.TypeChecking.Substitute'
  50% (  2 /  4) in 'Agda.TypeChecking.Abstract'
   5% (  2 / 37) in 'Agda.TypeChecking.Test.Generators'
   3% (  4 /159) in 'Agda.TypeChecking.Monad.Builtin'
  93% ( 14 / 15) in 'Agda.Interaction.FindFile'
 100% (  8 /  8) in 'Agda.Interaction.Response'
  76% ( 29 / 38) in 'Agda.TypeChecking.Monad.State'
  28% (  7 / 25) in 'Agda.Interaction.Options.Lenses'
  58% ( 21 / 36) in 'Agda.TypeChecking.Monad.Options'
 100% ( 11 / 11) in 'Agda.TypeChecking.Monad.Benchmark'
  21% (  3 / 14) in 'Agda.Syntax.Translation.AbstractToConcrete'
  65% ( 32 / 49) in 'Agda.Syntax.Scope.Monad'
   0% (  0 /  6) in 'Agda.TypeChecking.Monad.Sharing'
   0% (  0 /  2) in 'Agda.Syntax.Abstract.Copatterns'
  62% ( 10 / 16) in 'Agda.Syntax.Concrete.Operators'
  20% (  2 / 10) in 'Agda.TypeChecking.Monad.Trace'
  58% ( 11 / 19) in 'Agda.TypeChecking.Monad.Env'
  24% (  5 / 21) in 'Agda.Syntax.Translation.ConcreteToAbstract'
  50% (  1 /  2) in 'Agda.TypeChecking.LevelConstraints'
   0% (  0 /  2) in 'Agda.TypeChecking.Monad.Closure'
  33% (  1 /  3) in 'Agda.TypeChecking.Monad.Exception'
  32% (  6 / 19) in 'Agda.TypeChecking.Monad.Constraints'
  60% (  3 /  5) in 'Agda.TypeChecking.Monad.Open'
  79% ( 26 / 33) in 'Agda.TypeChecking.Monad.Context'
   6% (  1 / 18) in 'Agda.TypeChecking.Monad.Imports'
  32% ( 15 / 47) in 'Agda.TypeChecking.Monad.MetaVars'
  38% (  3 /  8) in 'Agda.TypeChecking.Monad.Mutual'
  50% ( 34 / 68) in 'Agda.TypeChecking.Monad.Signature'
  46% ( 16 / 35) in 'Agda.TypeChecking.Monad.SizedTypes'
 100% (  5 /  5) in 'Agda.TypeChecking.Monad.Statistics'
  94% ( 17 / 18) in 'Agda.TypeChecking.Monad'
  50% (  2 /  4) in 'Agda.Interaction.Monad'
   0% (  0 /  8) in 'Agda.Interaction.Highlighting.Dot'
 100% (  2 /  2) in 'Agda.Interaction.Highlighting.HTML'
  86% ( 18 / 21) in 'Agda.TypeChecking.Irrelevance'
 100% (  3 /  3) in 'Agda.Interaction.Highlighting.Emacs'
  40% (  2 /  5) in 'Agda.Syntax.Abstract.Pretty'
 100% (  3 /  3) in 'Agda.Compiler.CallCompiler'
 100% (  2 /  2) in 'Agda.Interaction.Highlighting.LaTeX'
   7% (  3 / 41) in 'Agda.Compiler.MAlonzo.Misc'
  67% (  2 /  3) in 'Agda.Compiler.MAlonzo.Encode'
  67% (  2 /  3) in 'Agda.Compiler.MAlonzo.Pretty'
   0% (  0 /  9) in 'Agda.Interaction.Highlighting.Vim'
  67% (  2 /  3) in 'Agda.TypeChecking.DropArgs'
   0% (  0 /  2) in 'Agda.Termination.RecCheck'
  11% (  1 /  9) in 'Agda.TypeChecking.Reduce.Monad'
  40% (  2 /  5) in 'Agda.TypeChecking.EtaContract'
   0% (  0 /  4) in 'Agda.TypeChecking.Forcing'
   0% (  0 /  2) in 'Agda.TypeChecking.MetaVars.Mention'
 100% (  3 /  3) in 'Agda.TypeChecking.Patterns.Abstract'
  42% ( 14 / 33) in 'Agda.TypeChecking.Reduce'
  71% ( 12 / 17) in 'Agda.TypeChecking.Telescope'
  75% ( 12 / 16) in 'Agda.TypeChecking.Datatypes'
  80% (  8 / 10) in 'Agda.TypeChecking.Tests'
  35% ( 12 / 34) in 'Agda.Compiler.Epic.CompileState'
  67% (  2 /  3) in 'Agda.Compiler.Epic.CaseOpts'
  75% (  3 /  4) in 'Agda.Compiler.Epic.ForceConstrs'
 100% (  3 /  3) in 'Agda.Compiler.Epic.Epic'
  67% (  4 /  6) in 'Agda.Compiler.Epic.NatDetection'
  53% ( 10 / 19) in 'Agda.Compiler.Epic.Primitive'
  21% (  3 / 14) in 'Agda.TypeChecking.Level'
   0% (  0 /  4) in 'Agda.TypeChecking.DisplayForm'
  25% (  1 /  4) in 'Agda.Syntax.Translation.InternalToAbstract'
   7% (  2 / 30) in 'Agda.TypeChecking.Pretty'
  33% (  2 /  6) in 'Agda.TypeChecking.Errors'
  83% ( 29 / 35) in 'Agda.TypeChecking.Records'
  12% (  2 / 16) in 'Agda.Compiler.HaskellTypes'
  56% (  5 /  9) in 'Agda.TypeChecking.Serialise'
  47% (  7 / 15) in 'Agda.Compiler.Epic.Erasure'
  12% (  3 / 25) in 'Agda.Compiler.Epic.Injection'
  50% (  4 /  8) in 'Agda.Compiler.Epic.Smashing'
  35% (  6 / 17) in 'Agda.TypeChecking.Rules.LHS.Problem'
  46% ( 24 / 52) in 'Agda.Termination.Monad'
  20% (  1 /  5) in 'Agda.Compiler.Epic.Static'
  86% (  6 /  7) in 'Agda.Compiler.Epic.FromAgda'
   5% (  1 / 21) in 'Agda.Compiler.MAlonzo.Primitives'
  25% (  1 /  4) in 'Agda.Termination.Inlining'
  60% ( 15 / 25) in 'Agda.TypeChecking.SizedTypes'
  75% (  3 /  4) in 'Agda.Termination.TermCheck'
  80% (  4 /  5) in 'Agda.TypeChecking.RecordPatterns'
  38% (  3 /  8) in 'Agda.TypeChecking.CompiledClause.Match'
  70% (  7 / 10) in 'Agda.TypeChecking.InstanceArguments'
  35% (  6 / 17) in 'Agda.TypeChecking.Constraints'
  45% ( 13 / 29) in 'Agda.TypeChecking.MetaVars.Occurs'
  56% ( 33 / 59) in 'Agda.TypeChecking.MetaVars'
  92% ( 12 / 13) in 'Agda.Interaction.Highlighting.Generate'
  50% (  1 /  2) in 'Agda.Tests'
 100% (  3 /  3) in 'Agda.TypeChecking.SyntacticEquality'
  88% ( 21 / 24) in 'Agda.TypeChecking.Polarity'
  67% (  4 /  6) in 'Agda.TypeChecking.Implicit'
  67% (  2 /  3) in 'Agda.TypeChecking.Rules.LHS.Instantiate'
  57% (  4 /  7) in 'Agda.TypeChecking.Patterns.Match'
  42% ( 10 / 24) in 'Agda.TypeChecking.Positivity'
  88% (  7 /  8) in 'Agda.TypeChecking.ProjectionLike'
   0% (  0 / 15) in 'Agda.TypeChecking.Quote'
  13% (  7 / 52) in 'Agda.TypeChecking.Primitive'
  17% (  1 /  6) in 'Agda.TypeChecking.Injectivity'
  56% ( 18 / 32) in 'Agda.TypeChecking.Conversion'
  39% ( 23 / 59) in 'Agda.TypeChecking.Rules.LHS.Unify'
  57% (  8 / 14) in 'Agda.Compiler.Epic.Forcing'
 100% (  3 /  3) in 'Agda.TypeChecking.CheckInternal'
  80% (  4 /  5) in 'Agda.TypeChecking.Rules.LHS.Split'
  89% (  8 /  9) in 'Agda.TypeChecking.Rules.Data'
  57% (  4 /  7) in 'Agda.TypeChecking.Rules.LHS.Implicit'
  50% (  3 /  6) in 'Agda.TypeChecking.With'
  67% (  4 /  6) in 'Agda.TypeChecking.Rules.LHS.ProblemRest'
  73% (  8 / 11) in 'Agda.TypeChecking.Rules.LHS'
  65% ( 13 / 20) in 'Agda.TypeChecking.Coverage'
  36% (  4 / 11) in 'Agda.TypeChecking.CompiledClause.Compile'
  50% (  1 /  2) in 'Agda.TypeChecking.Empty'
  70% ( 33 / 47) in 'Agda.TypeChecking.Rules.Term'
  67% (  2 /  3) in 'Agda.TypeChecking.Rules.Builtin'
 100% (  7 /  7) in 'Agda.TypeChecking.Rules.Builtin.Coinduction'
  75% (  3 /  4) in 'Agda.TypeChecking.Rules.Record'
  64% (  7 / 11) in 'Agda.TypeChecking.Rules.Def'
  82% ( 14 / 17) in 'Agda.TypeChecking.Rules.Decl'
  80% (  4 /  5) in 'Agda.TypeChecker'
  67% ( 14 / 21) in 'Agda.Interaction.Imports'
  12% (  4 / 32) in 'Agda.Compiler.MAlonzo.Compiler'
 100% (  2 /  2) in 'Agda.Compiler.Epic.Compiler'
   0% (  0 / 35) in 'Agda.Compiler.JS.Compiler'
  26% (  9 / 34) in 'Agda.Interaction.BasicOps'
  12% (  3 / 24) in 'Agda.Interaction.CommandLine.CommandLine'
  29% (  2 /  7) in 'Agda.Interaction.MakeCase'
   0% (  0 / 46) in 'Agda.Auto.Convert'
   0% (  0 /  2) in 'Agda.Auto.Auto'
  70% ( 33 / 47) in 'Agda.Interaction.InteractionTop'
  50% (  1 /  2) in 'Agda.Interaction.EmacsTop'
 100% (  6 /  6) in 'Agda.Main'
Warning: Agda.Utils.Maybe.Strict: could not find link destinations for:
    Data.Strict.Maybe.Maybe Data.Strict.Maybe.maybe Data.Strict.Maybe.Just Data.Strict.Maybe.Nothing Data.Strict.Maybe.fromMaybe
Warning: Agda.TypeChecking.Monad.Debug: could not find link destinations for:
    Control.Monad.IO.Class.MonadIO
Warning: Agda.Utils.BiMap: could not find link destinations for:
    Test.QuickCheck.Arbitrary.Arbitrary
Warning: Agda.Utils.Pointer: could not find link destinations for:
    Data.Hashable.Class.Hashable
Warning: Agda.Utils.Functor: could not find link destinations for:
    Data.Functor.Identity.Identity Data.Functor.Compose.Compose
Warning: Agda.Utils.Fresh: could not find link destinations for:
    Control.Monad.State.Class.MonadState Control.Monad.Reader.Class.MonadReader
Warning: Agda.Utils.Update: could not find link destinations for:
    Data.Functor.Identity.Identity Agda.Utils.Update.EndoFun
Warning: Agda.Utils.QuickCheck: could not find link destinations for:
    Test.QuickCheck.Test.Result Test.QuickCheck.Property.Testable Test.QuickCheck.Test.Args
Warning: Agda.Utils.TestHelpers: could not find link destinations for:
    Test.QuickCheck.Arbitrary.Arbitrary Test.QuickCheck.Gen.Gen
Warning: Agda.Termination.Semiring: could not find link destinations for:
    Test.QuickCheck.Arbitrary.Arbitrary
Warning: Agda.Utils.PartialOrd: could not find link destinations for:
    Test.QuickCheck.Arbitrary.Arbitrary Agda.Termination.Order.Unknown Test.QuickCheck.Property.Property Test.QuickCheck.Modifiers.NonEmptyList Test.QuickCheck.All.quickCheckAll
Warning: Agda.Utils.Graph.AdjacencyMap: could not find link destinations for:
    Test.QuickCheck.Arbitrary.Arbitrary Test.QuickCheck.Gen.Gen
Warning: Agda.Utils.List: could not find link destinations for:
    Test.QuickCheck.Property.Property
Warning: Agda.Utils.Graph.AdjacencyMap.Unidirectional: could not find link destinations for:
    Test.QuickCheck.Arbitrary.Arbitrary Test.QuickCheck.Arbitrary.CoArbitrary Test.QuickCheck.Gen.Gen
Warning: Agda.Utils.FileName: could not find link destinations for:
    Test.QuickCheck.Arbitrary.Arbitrary
Warning: Agda.Syntax.Position: could not find link destinations for:
    Agda.Syntax.Position.SrcFile Test.QuickCheck.Arbitrary.Arbitrary
Warning: Agda.Syntax.Common: could not find link destinations for:
    Test.QuickCheck.Arbitrary.CoArbitrary Test.QuickCheck.Arbitrary.Arbitrary Data.Generics.Geniplate.UniverseBi Data.Hashable.Class.Hashable
Warning: Agda.Utils.Warshall: could not find link destinations for:
    Control.Monad.Trans.State.Lazy.State Test.QuickCheck.Gen.Gen Test.QuickCheck.Property.Property
Warning: Agda.Interaction.Highlighting.Range: could not find link destinations for:
    Test.QuickCheck.Arbitrary.CoArbitrary Test.QuickCheck.Arbitrary.Arbitrary
Warning: Agda.Syntax.Parser.Monad: could not find link destinations for:
    Control.Monad.State.Class.MonadState Control.Monad.Error.Class.MonadError
Warning: Agda.Syntax.Concrete.Name: could not find link destinations for:
    Test.QuickCheck.Arbitrary.CoArbitrary Test.QuickCheck.Arbitrary.Arbitrary
Warning: Agda.Syntax.Abstract.Name: could not find link destinations for:
    Data.Hashable.Class.Hashable Data.Generics.Geniplate.UniverseBi Control.Monad.State.Class.MonadState
Warning: Agda.Utils.Favorites: could not find link destinations for:
    Test.QuickCheck.Arbitrary.CoArbitrary Test.QuickCheck.Arbitrary.Arbitrary Test.QuickCheck.All.quickCheckAll
Warning: Agda.Auto.NarrowingSearch: could not find link destinations for:
    Control.Monad.Trans.State.Lazy.StateT
Warning: Agda.Auto.SearchControl: could not find link destinations for:
    Control.Monad.Trans.State.Lazy.StateT
Warning: Agda.Utils.Trie: could not find link destinations for:
    Data.Strict.Maybe.Maybe
Warning: Agda.Utils.Monad: could not find link destinations for:
    Control.Monad.Trans.Error.Error Control.Monad.Error.Class.MonadError Control.Monad.State.Class.MonadState
Warning: Agda.Syntax.Parser.StringLiterals: could not find link destinations for:
    Agda.Syntax.Parser.StringLiterals.readNum
Warning: Agda.Termination.SparseMatrix: could not find link destinations for:
    Test.QuickCheck.Arbitrary.CoArbitrary Test.QuickCheck.Arbitrary.Arbitrary Test.QuickCheck.Gen.Gen Agda.Termination.SparseMatrix.supSize Agda.Termination.SparseMatrix.Transpose Agda.Termination.SparseMatrix.zipAssocWith Agda.Termination.SparseMatrix.interAssocWith
Warning: Agda.Termination.Order: could not find link destinations for:
    Agda.Termination.Order.Unknown Test.QuickCheck.Arbitrary.CoArbitrary Test.QuickCheck.Arbitrary.Arbitrary Agda.Termination.Order.maxO
Warning: Agda.Termination.CallMatrix: could not find link destinations for:
    Test.QuickCheck.Arbitrary.Arbitrary Test.QuickCheck.Arbitrary.CoArbitrary Test.QuickCheck.Gen.Gen
Warning: Agda.TypeChecking.Coverage.SplitTree: could not find link destinations for:
    Test.QuickCheck.Arbitrary.Arbitrary
Warning: Agda.Syntax.Info: could not find link destinations for:
    Data.Generics.Geniplate.UniverseBi
Warning: Agda.Utils.Geniplate: could not find link destinations for:
    Data.Generics.Geniplate.instanceUniverseBiT Data.Generics.Geniplate.universeBi Data.Generics.Geniplate.instanceTransformBiMT Data.Generics.Geniplate.transformBiM
Warning: Agda.Syntax.Abstract: could not find link destinations for:
    Data.Generics.Geniplate.UniverseBi
Warning: Agda.Syntax.Internal: could not find link destinations for:
    Data.Generics.Geniplate.UniverseBi
Warning: Agda.Syntax.Internal.Defs: could not find link destinations for:
    Control.Monad.Trans.Reader.ReaderT Control.Monad.Trans.Writer.Lazy.Writer
Warning: Agda.Interaction.Highlighting.Precise: could not find link destinations for:
    Test.QuickCheck.Arbitrary.CoArbitrary Test.QuickCheck.Arbitrary.Arbitrary
Warning: Agda.Syntax.Concrete.Definitions: could not find link destinations for:
    Agda.Syntax.Concrete.Definitions.TerminationCheck Agda.Syntax.Concrete.Definitions.DataRecOrFun Control.Monad.Trans.Error.Error Control.Monad.Trans.State.Lazy.StateT Agda.Syntax.Concrete.Definitions.NiceEnv
Warning: Agda.Syntax.Parser: could not find link destinations for:
    Control.Monad.Error.Class.MonadError
Warning: Agda.TypeChecking.Monad.Base: could not find link destinations for:
    Control.Monad.State.Class.MonadState Control.Monad.IO.Class.MonadIO Data.HashMap.Base.HashMap Control.Monad.Reader.Class.MonadReader Control.Monad.Trans.Error.Error Control.Monad.Error.Class.MonadError Control.Monad.Trans.Reader.Reader Control.Monad.Trans.Class.MonadTrans Control.Monad.Trans.Error.ErrorT Control.Monad.Trans.Writer.Lazy.WriterT
Warning: Agda.TypeChecking.Test.Generators: could not find link destinations for:
    Test.QuickCheck.Arbitrary.Arbitrary Test.QuickCheck.Gen.Gen Test.QuickCheck.Property.Property
Warning: Agda.TypeChecking.Monad.Builtin: could not find link destinations for:
    Control.Monad.IO.Class.MonadIO
Warning: Agda.TypeChecking.Monad.Options: could not find link destinations for:
    Control.Monad.IO.Class.MonadIO Control.Monad.Reader.Class.MonadReader
Warning: Agda.Syntax.Translation.AbstractToConcrete: could not find link destinations for:
    Control.Monad.Trans.Reader.ReaderT
Warning: Agda.Syntax.Scope.Monad: could not find link destinations for:
    Control.Monad.Trans.Class.MonadTrans Control.Monad.Trans.State.Lazy.StateT
Warning: Agda.TypeChecking.Monad.Sharing: could not find link destinations for:
    Control.Monad.Trans.Class.MonadTrans
Warning: Agda.Syntax.Abstract.Copatterns: could not find link destinations for:
    Agda.Syntax.Abstract.Copatterns.groupClauses
Warning: Agda.Syntax.Concrete.Operators: could not find link destinations for:
    Agda.Syntax.Concrete.Operators.FlatScope
Warning: Agda.TypeChecking.Monad.Env: could not find link destinations for:
    Control.Monad.Reader.Class.MonadReader
Warning: Agda.TypeChecking.Monad.Exception: could not find link destinations for:
    Control.Monad.Trans.Error.Error Control.Monad.State.Class.MonadState Control.Monad.Reader.Class.MonadReader Control.Monad.Error.Class.MonadError Control.Monad.Trans.Class.MonadTrans Control.Monad.IO.Class.MonadIO Control.Monad.Trans.Writer.Lazy.WriterT Control.Monad.Trans.Reader.ReaderT
Warning: Agda.TypeChecking.Monad.Signature: could not find link destinations for:
    Control.Monad.Reader.Class.MonadReader
Warning: Agda.Interaction.Monad: could not find link destinations for:
    System.Console.Haskeline.InputT.InputT
Warning: Agda.Interaction.Highlighting.Dot: could not find link destinations for:
    Control.Monad.Trans.State.Lazy.StateT
Warning: Agda.Compiler.MAlonzo.Misc: could not find link destinations for:
    Language.Haskell.Exts.Syntax.ModuleName Language.Haskell.Exts.Syntax.Name Language.Haskell.Exts.Syntax.QName Language.Haskell.Exts.Syntax.Exp Language.Haskell.Exts.Syntax.Decl Language.Haskell.Exts.Syntax.Type
Warning: Agda.Compiler.MAlonzo.Encode: could not find link destinations for:
    Language.Haskell.Exts.Syntax.ModuleName
Warning: Agda.Compiler.MAlonzo.Pretty: could not find link destinations for:
    Language.Haskell.Exts.Pretty.Pretty Data.Generics.Geniplate.TransformBi Language.Haskell.Exts.Syntax.ModuleName Language.Haskell.Exts.Syntax.QName Language.Haskell.Exts.Syntax.Module Language.Haskell.Exts.Syntax.Exp
Warning: Agda.TypeChecking.EtaContract: could not find link destinations for:
    Control.Monad.Reader.Class.MonadReader
Warning: Agda.TypeChecking.Reduce: could not find link destinations for:
    Data.Hashable.Class.Hashable Data.HashMap.Base.HashMap
Warning: Agda.TypeChecking.Tests: could not find link destinations for:
    Test.QuickCheck.Property.Property
Warning: Agda.Compiler.Epic.CompileState: could not find link destinations for:
    Control.Monad.Trans.State.Lazy.StateT
Warning: Agda.TypeChecking.Serialise: could not find link destinations for:
    Data.Hashable.Class.Hashable Data.HashMap.Base.HashMap Data.HashTable.IO.CuckooHashTable Data.HashTable.IO.BasicHashTable Data.HashTable.IO.LinearHashTable Agda.TypeChecking.Serialise.nodeMemo
Warning: Agda.Compiler.Epic.Erasure: could not find link destinations for:
    Control.Monad.Trans.State.Lazy.StateT
Warning: Agda.Compiler.Epic.Injection: could not find link destinations for:
    Control.Monad.Trans.Reader.ReaderT
Warning: Agda.TypeChecking.Rules.LHS.Problem: could not find link destinations for:
    Control.Monad.Trans.Error.Error
Warning: Agda.Termination.Monad: could not find link destinations for:
    Control.Monad.Trans.Reader.ReaderT Control.Monad.IO.Class.MonadIO Control.Monad.State.Class.MonadState Control.Monad.Reader.Class.MonadReader Control.Monad.Error.Class.MonadError
Warning: Agda.Compiler.MAlonzo.Primitives: could not find link destinations for:
    Language.Haskell.Exts.Syntax.Decl Language.Haskell.Exts.Syntax.ModuleName Language.Haskell.Exts.Syntax.Exp
Warning: Agda.Termination.Inlining: could not find link destinations for:
    Agda.Termination.Inlining.withExprClauses Agda.Termination.Inlining.inlinedClauses
Warning: Agda.Termination.TermCheck: could not find link destinations for:
    Agda.Termination.TermCheck.makeCM Agda.Termination.TermCheck.compareArgs Agda.Termination.TermCheck.addGuardedness
Warning: Agda.TypeChecking.RecordPatterns: could not find link destinations for:
    Agda.TypeChecking.RecordPatterns.VarPat Agda.TypeChecking.RecordPatterns.DotPat Agda.TypeChecking.RecordPatterns.RecPatM Agda.TypeChecking.RecordPatterns.translatePattern
Warning: Agda.TypeChecking.MetaVars: could not find link destinations for:
    Control.Monad.Trans.Error.Error Control.Monad.Trans.Error.ErrorT
Warning: Agda.Interaction.Highlighting.Generate: could not find link destinations for:
    Agda.Interaction.Highlighting.Generate.NameKinds Agda.Interaction.Highlighting.Generate.nameToFile
Warning: Agda.TypeChecking.Positivity: could not find link destinations for:
    Control.Monad.Trans.Reader.Reader
Warning: Agda.TypeChecking.Rules.LHS.Unify: could not find link destinations for:
    Control.Monad.Trans.Reader.ReaderT Control.Monad.Trans.Writer.Lazy.WriterT Control.Monad.Trans.State.Lazy.StateT Control.Monad.IO.Class.MonadIO Control.Monad.State.Class.MonadState Control.Monad.Reader.Class.MonadReader Control.Monad.Writer.Class.MonadWriter Control.Monad.Trans.Error.Error
Warning: Agda.Compiler.Epic.Forcing: could not find link destinations for:
    Control.Monad.Trans.Class.MonadTrans
Warning: Agda.TypeChecking.Rules.Term: could not find link destinations for:
    Control.Monad.Trans.Error.Error Control.Monad.Trans.Error.ErrorT
Warning: Agda.Compiler.MAlonzo.Compiler: could not find link destinations for:
    Language.Haskell.Exts.Syntax.ImportDecl Language.Haskell.Exts.Syntax.Decl Language.Haskell.Exts.Syntax.Pat Language.Haskell.Exts.Syntax.Exp Control.Monad.Trans.Reader.ReaderT Language.Haskell.Exts.Syntax.Literal Language.Haskell.Exts.Syntax.ConDecl Language.Haskell.Exts.Syntax.Module Language.Haskell.Exts.Extension.Extension Data.Generics.Geniplate.TransformBi Language.Haskell.Exts.Syntax.ModuleName Language.Haskell.Exts.Pretty.Pretty
Warning: Agda.Auto.Convert: could not find link destinations for:
    Control.Monad.State.Class.MonadState Control.Monad.Trans.State.Lazy.StateT Control.Monad.Trans.Error.ErrorT
Warning: Agda.Interaction.InteractionTop: could not find link destinations for:
    Control.Monad.Trans.State.Lazy.StateT Control.Monad.State.Class.MonadState Control.Monad.Trans.Class.lift Control.Monad.IO.Class.liftIO Control.Monad.Trans.Error.ErrorT Data.Functor.Identity.Identity
Documentation created: dist/doc/html/Agda/index.html
Preprocessing executable 'agda-mode' for Agda-2.3.3...
Preprocessing executable 'agda' for Agda-2.3.3...

Change History

Changed 9 months ago by Fūzetsu

  • owner set to Fūzetsu
  • status changed from new to assigned

I'll have a look, 2.5GB is sub-optimal especially if GHC can do with less where the bulk of tho work is.

Changed 8 months ago by Fūzetsu

  • version changed from 2.13.2.1 to 2.15.0

I should add that while I didn't have the opportunity to investigate exactly why this happens, I can confirm such high memory usage with the git version of Haddock.

Note: See TracTickets for help on using tickets.