You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.54System time (seconds):9.91PercentofCPU this job got:89%Elapsed (wall clock) time (h:mm:ss or m:ss):5:26.72Average shared text size (kbytes):0Average unshared data size (kbytes):0Average stack size (kbytes):0Average total size (kbytes):0Maximum resident set size (kbytes):11120448Average resident set size (kbytes):0Major (requiring I/O) page faults:578Minor (reclaiming a frame) page faults:3759501Voluntary context switches:14902Involuntary context switches:31922Swaps:0File system inputs:176104File system outputs:356088Socket messages sent:0Socket messages received:0Signals delivered:0Page size (bytes):4096Exit status:0
Size of documentation produced: 8m of .html
$ haddock --versionHaddock version 2.13.2, (c) SimonMarlow2006Ported to use the GHCAPI by DavidWaern2006-2008
Here the full output:
$/usr/bin/time --verbose cabal haddockRunningHaddock 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.1Haddock coverage:Warning:Agda-2.3.3:Agda.Utils.Maybe.Strict:Couldnot find documentation for exported module:Data.Strict.Maybe90% ( 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:Couldnot find documentation for exported module:Test.QuickCheck0% ( 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:Couldnot find documentation for exported module:HashMap0% ( 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.MaybeData.Strict.Maybe.maybeData.Strict.Maybe.JustData.Strict.Maybe.NothingData.Strict.Maybe.fromMaybe
Warning:Agda.TypeChecking.Monad.Debug: could not find link destinations for:Control.Monad.IO.Class.MonadIOWarning:Agda.Utils.BiMap: could not find link destinations for:Test.QuickCheck.Arbitrary.ArbitraryWarning:Agda.Utils.Pointer: could not find link destinations for:Data.Hashable.Class.HashableWarning:Agda.Utils.Functor: could not find link destinations for:Data.Functor.Identity.IdentityData.Functor.Compose.ComposeWarning:Agda.Utils.Fresh: could not find link destinations for:Control.Monad.State.Class.MonadStateControl.Monad.Reader.Class.MonadReaderWarning:Agda.Utils.Update: could not find link destinations for:Data.Functor.Identity.IdentityAgda.Utils.Update.EndoFunWarning:Agda.Utils.QuickCheck: could not find link destinations for:Test.QuickCheck.Test.ResultTest.QuickCheck.Property.TestableTest.QuickCheck.Test.ArgsWarning:Agda.Utils.TestHelpers: could not find link destinations for:Test.QuickCheck.Arbitrary.ArbitraryTest.QuickCheck.Gen.GenWarning:Agda.Termination.Semiring: could not find link destinations for:Test.QuickCheck.Arbitrary.ArbitraryWarning:Agda.Utils.PartialOrd: could not find link destinations for:Test.QuickCheck.Arbitrary.ArbitraryAgda.Termination.Order.UnknownTest.QuickCheck.Property.PropertyTest.QuickCheck.Modifiers.NonEmptyListTest.QuickCheck.All.quickCheckAll
Warning:Agda.Utils.Graph.AdjacencyMap: could not find link destinations for:Test.QuickCheck.Arbitrary.ArbitraryTest.QuickCheck.Gen.GenWarning:Agda.Utils.List: could not find link destinations for:Test.QuickCheck.Property.PropertyWarning:Agda.Utils.Graph.AdjacencyMap.Unidirectional: could not find link destinations for:Test.QuickCheck.Arbitrary.ArbitraryTest.QuickCheck.Arbitrary.CoArbitraryTest.QuickCheck.Gen.GenWarning:Agda.Utils.FileName: could not find link destinations for:Test.QuickCheck.Arbitrary.ArbitraryWarning:Agda.Syntax.Position: could not find link destinations for:Agda.Syntax.Position.SrcFileTest.QuickCheck.Arbitrary.ArbitraryWarning:Agda.Syntax.Common: could not find link destinations for:Test.QuickCheck.Arbitrary.CoArbitraryTest.QuickCheck.Arbitrary.ArbitraryData.Generics.Geniplate.UniverseBiData.Hashable.Class.HashableWarning:Agda.Utils.Warshall: could not find link destinations for:Control.Monad.Trans.State.Lazy.StateTest.QuickCheck.Gen.GenTest.QuickCheck.Property.PropertyWarning:Agda.Interaction.Highlighting.Range: could not find link destinations for:Test.QuickCheck.Arbitrary.CoArbitraryTest.QuickCheck.Arbitrary.ArbitraryWarning:Agda.Syntax.Parser.Monad: could not find link destinations for:Control.Monad.State.Class.MonadStateControl.Monad.Error.Class.MonadErrorWarning:Agda.Syntax.Concrete.Name: could not find link destinations for:Test.QuickCheck.Arbitrary.CoArbitraryTest.QuickCheck.Arbitrary.ArbitraryWarning:Agda.Syntax.Abstract.Name: could not find link destinations for:Data.Hashable.Class.HashableData.Generics.Geniplate.UniverseBiControl.Monad.State.Class.MonadStateWarning:Agda.Utils.Favorites: could not find link destinations for:Test.QuickCheck.Arbitrary.CoArbitraryTest.QuickCheck.Arbitrary.ArbitraryTest.QuickCheck.All.quickCheckAll
Warning:Agda.Auto.NarrowingSearch: could not find link destinations for:Control.Monad.Trans.State.Lazy.StateTWarning:Agda.Auto.SearchControl: could not find link destinations for:Control.Monad.Trans.State.Lazy.StateTWarning:Agda.Utils.Trie: could not find link destinations for:Data.Strict.Maybe.MaybeWarning:Agda.Utils.Monad: could not find link destinations for:Control.Monad.Trans.Error.ErrorControl.Monad.Error.Class.MonadErrorControl.Monad.State.Class.MonadStateWarning: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.CoArbitraryTest.QuickCheck.Arbitrary.ArbitraryTest.QuickCheck.Gen.GenAgda.Termination.SparseMatrix.supSize Agda.Termination.SparseMatrix.TransposeAgda.Termination.SparseMatrix.zipAssocWith Agda.Termination.SparseMatrix.interAssocWith
Warning:Agda.Termination.Order: could not find link destinations for:Agda.Termination.Order.UnknownTest.QuickCheck.Arbitrary.CoArbitraryTest.QuickCheck.Arbitrary.ArbitraryAgda.Termination.Order.maxO
Warning:Agda.Termination.CallMatrix: could not find link destinations for:Test.QuickCheck.Arbitrary.ArbitraryTest.QuickCheck.Arbitrary.CoArbitraryTest.QuickCheck.Gen.GenWarning:Agda.TypeChecking.Coverage.SplitTree: could not find link destinations for:Test.QuickCheck.Arbitrary.ArbitraryWarning:Agda.Syntax.Info: could not find link destinations for:Data.Generics.Geniplate.UniverseBiWarning: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.UniverseBiWarning:Agda.Syntax.Internal: could not find link destinations for:Data.Generics.Geniplate.UniverseBiWarning:Agda.Syntax.Internal.Defs: could not find link destinations for:Control.Monad.Trans.Reader.ReaderTControl.Monad.Trans.Writer.Lazy.WriterWarning:Agda.Interaction.Highlighting.Precise: could not find link destinations for:Test.QuickCheck.Arbitrary.CoArbitraryTest.QuickCheck.Arbitrary.ArbitraryWarning:Agda.Syntax.Concrete.Definitions: could not find link destinations for:Agda.Syntax.Concrete.Definitions.TerminationCheckAgda.Syntax.Concrete.Definitions.DataRecOrFunControl.Monad.Trans.Error.ErrorControl.Monad.Trans.State.Lazy.StateTAgda.Syntax.Concrete.Definitions.NiceEnvWarning:Agda.Syntax.Parser: could not find link destinations for:Control.Monad.Error.Class.MonadErrorWarning:Agda.TypeChecking.Monad.Base: could not find link destinations for:Control.Monad.State.Class.MonadStateControl.Monad.IO.Class.MonadIOData.HashMap.Base.HashMapControl.Monad.Reader.Class.MonadReaderControl.Monad.Trans.Error.ErrorControl.Monad.Error.Class.MonadErrorControl.Monad.Trans.Reader.ReaderControl.Monad.Trans.Class.MonadTransControl.Monad.Trans.Error.ErrorTControl.Monad.Trans.Writer.Lazy.WriterTWarning:Agda.TypeChecking.Test.Generators: could not find link destinations for:Test.QuickCheck.Arbitrary.ArbitraryTest.QuickCheck.Gen.GenTest.QuickCheck.Property.PropertyWarning:Agda.TypeChecking.Monad.Builtin: could not find link destinations for:Control.Monad.IO.Class.MonadIOWarning:Agda.TypeChecking.Monad.Options: could not find link destinations for:Control.Monad.IO.Class.MonadIOControl.Monad.Reader.Class.MonadReaderWarning:Agda.Syntax.Translation.AbstractToConcrete: could not find link destinations for:Control.Monad.Trans.Reader.ReaderTWarning:Agda.Syntax.Scope.Monad: could not find link destinations for:Control.Monad.Trans.Class.MonadTransControl.Monad.Trans.State.Lazy.StateTWarning:Agda.TypeChecking.Monad.Sharing: could not find link destinations for:Control.Monad.Trans.Class.MonadTransWarning: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.FlatScopeWarning:Agda.TypeChecking.Monad.Env: could not find link destinations for:Control.Monad.Reader.Class.MonadReaderWarning:Agda.TypeChecking.Monad.Exception: could not find link destinations for:Control.Monad.Trans.Error.ErrorControl.Monad.State.Class.MonadStateControl.Monad.Reader.Class.MonadReaderControl.Monad.Error.Class.MonadErrorControl.Monad.Trans.Class.MonadTransControl.Monad.IO.Class.MonadIOControl.Monad.Trans.Writer.Lazy.WriterTControl.Monad.Trans.Reader.ReaderTWarning:Agda.TypeChecking.Monad.Signature: could not find link destinations for:Control.Monad.Reader.Class.MonadReaderWarning:Agda.Interaction.Monad: could not find link destinations for:System.Console.Haskeline.InputT.InputTWarning:Agda.Interaction.Highlighting.Dot: could not find link destinations for:Control.Monad.Trans.State.Lazy.StateTWarning:Agda.Compiler.MAlonzo.Misc: could not find link destinations for:Language.Haskell.Exts.Syntax.ModuleNameLanguage.Haskell.Exts.Syntax.NameLanguage.Haskell.Exts.Syntax.QNameLanguage.Haskell.Exts.Syntax.ExpLanguage.Haskell.Exts.Syntax.DeclLanguage.Haskell.Exts.Syntax.TypeWarning:Agda.Compiler.MAlonzo.Encode: could not find link destinations for:Language.Haskell.Exts.Syntax.ModuleNameWarning:Agda.Compiler.MAlonzo.Pretty: could not find link destinations for:Language.Haskell.Exts.Pretty.PrettyData.Generics.Geniplate.TransformBiLanguage.Haskell.Exts.Syntax.ModuleNameLanguage.Haskell.Exts.Syntax.QNameLanguage.Haskell.Exts.Syntax.ModuleLanguage.Haskell.Exts.Syntax.ExpWarning:Agda.TypeChecking.EtaContract: could not find link destinations for:Control.Monad.Reader.Class.MonadReaderWarning:Agda.TypeChecking.Reduce: could not find link destinations for:Data.Hashable.Class.HashableData.HashMap.Base.HashMapWarning:Agda.TypeChecking.Tests: could not find link destinations for:Test.QuickCheck.Property.PropertyWarning:Agda.Compiler.Epic.CompileState: could not find link destinations for:Control.Monad.Trans.State.Lazy.StateTWarning:Agda.TypeChecking.Serialise: could not find link destinations for:Data.Hashable.Class.HashableData.HashMap.Base.HashMapData.HashTable.IO.CuckooHashTableData.HashTable.IO.BasicHashTableData.HashTable.IO.LinearHashTableAgda.TypeChecking.Serialise.nodeMemo
Warning:Agda.Compiler.Epic.Erasure: could not find link destinations for:Control.Monad.Trans.State.Lazy.StateTWarning:Agda.Compiler.Epic.Injection: could not find link destinations for:Control.Monad.Trans.Reader.ReaderTWarning:Agda.TypeChecking.Rules.LHS.Problem: could not find link destinations for:Control.Monad.Trans.Error.ErrorWarning:Agda.Termination.Monad: could not find link destinations for:Control.Monad.Trans.Reader.ReaderTControl.Monad.IO.Class.MonadIOControl.Monad.State.Class.MonadStateControl.Monad.Reader.Class.MonadReaderControl.Monad.Error.Class.MonadErrorWarning:Agda.Compiler.MAlonzo.Primitives: could not find link destinations for:Language.Haskell.Exts.Syntax.DeclLanguage.Haskell.Exts.Syntax.ModuleNameLanguage.Haskell.Exts.Syntax.ExpWarning: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.VarPatAgda.TypeChecking.RecordPatterns.DotPatAgda.TypeChecking.RecordPatterns.RecPatMAgda.TypeChecking.RecordPatterns.translatePattern
Warning:Agda.TypeChecking.MetaVars: could not find link destinations for:Control.Monad.Trans.Error.ErrorControl.Monad.Trans.Error.ErrorTWarning:Agda.Interaction.Highlighting.Generate: could not find link destinations for:Agda.Interaction.Highlighting.Generate.NameKindsAgda.Interaction.Highlighting.Generate.nameToFile
Warning:Agda.TypeChecking.Positivity: could not find link destinations for:Control.Monad.Trans.Reader.ReaderWarning:Agda.TypeChecking.Rules.LHS.Unify: could not find link destinations for:Control.Monad.Trans.Reader.ReaderTControl.Monad.Trans.Writer.Lazy.WriterTControl.Monad.Trans.State.Lazy.StateTControl.Monad.IO.Class.MonadIOControl.Monad.State.Class.MonadStateControl.Monad.Reader.Class.MonadReaderControl.Monad.Writer.Class.MonadWriterControl.Monad.Trans.Error.ErrorWarning:Agda.Compiler.Epic.Forcing: could not find link destinations for:Control.Monad.Trans.Class.MonadTransWarning:Agda.TypeChecking.Rules.Term: could not find link destinations for:Control.Monad.Trans.Error.ErrorControl.Monad.Trans.Error.ErrorTWarning:Agda.Compiler.MAlonzo.Compiler: could not find link destinations for:Language.Haskell.Exts.Syntax.ImportDeclLanguage.Haskell.Exts.Syntax.DeclLanguage.Haskell.Exts.Syntax.PatLanguage.Haskell.Exts.Syntax.ExpControl.Monad.Trans.Reader.ReaderTLanguage.Haskell.Exts.Syntax.LiteralLanguage.Haskell.Exts.Syntax.ConDeclLanguage.Haskell.Exts.Syntax.ModuleLanguage.Haskell.Exts.Extension.ExtensionData.Generics.Geniplate.TransformBiLanguage.Haskell.Exts.Syntax.ModuleNameLanguage.Haskell.Exts.Pretty.PrettyWarning:Agda.Auto.Convert: could not find link destinations for:Control.Monad.State.Class.MonadStateControl.Monad.Trans.State.Lazy.StateTControl.Monad.Trans.Error.ErrorTWarning:Agda.Interaction.InteractionTop: could not find link destinations for:Control.Monad.Trans.State.Lazy.StateTControl.Monad.State.Class.MonadStateControl.Monad.Trans.Class.lift Control.Monad.IO.Class.liftIO Control.Monad.Trans.Error.ErrorTData.Functor.Identity.IdentityDocumentation created: dist/doc/html/Agda/index.html
Preprocessing executable 'agda-mode' for Agda-2.3.3...Preprocessing executable 'agda' for Agda-2.3.3...
The text was updated successfully, but these errors were encountered:
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.
I think the best way to fix this issue once and for all is to write out the information Haddock produces for each module to disk, then read that information back again when doing the renaming and the generation of HTML.
Original reporter: andreas.abel@
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):
Size of documentation produced: 8m of .html
Here the full output:
The text was updated successfully, but these errors were encountered: