Slow build times #348
Description
Waiting for Strata build times takes up a significant chunk of the time it takes me to develop on Strata. This is despite using incremental builds and multiple repositories so I have to switch branches less and get more build cache hits. I think a good start is to reduce the uncached build time. After lake clean, it takes me about 6 minutes to build Strata locally.
lake build Strata -v > StrataBuildOutputs 311.71s user 103.99s system 175% cpu 3:56.88 total
lake build 753.98s user 177.11s system 260% cpu 5:57.51 total
One of the pieces of work the first call does that the second does not is build .c files. Some .lean files, like Init.lean, elaborate to a large C file (82K lines), and building that can take a long time (~100 seconds).
Here follow file specific build times. The .c.o files are build times from compiling c to .c.o, which is something that does not happen when using the Lean IDE, so you might want to ignore those.
100s Strata.DDM.BuiltinDialects.Init:c.o (with exports)
74s Strata.Languages.Core.Factory
67s Strata.Languages.Core.SMTEncoder:c.o (with exports)
29s Strata.Languages.Python.PythonDialect
22s Strata.DL.SMT.DDMTransform.Parse
21s Strata.Transform.CallElimCorrect
21s Strata.DL.SMT.DDMTransform.Parse:c.o (with exports)
16s Strata.DL.Lambda.LTy
15s Strata.Languages.Core.SMTEncoder
14s Strata.DL.SMT.Op
14s Strata.DL.Lambda.LExpr
14s Strata.DDM.Ion
14s Strata.DDM.AST
12s Strata.DL.Lambda.LExprTypeEnv
12s Strata.DL.Lambda.LExprEval
11s Strata.Languages.Python.PythonDialect:c.o (with exports)
10s Strata.Languages.Python.Regex.ReToCore
10s Strata.Languages.Python.PythonToCore
10s Strata.Languages.Python.CorePrelude
10s Strata.Languages.Core.DDMTransform.Translate:c.o (with exports)
10s Strata.DL.SMT.Function
10s Strata.DL.Lambda.LTyUnify
10s Strata.DDM.TaggedRegions
10s Strata.DDM.Elab.Core
9.8s Strata.Languages.Core.CmdType
9.7s Strata.Languages.Core.StatementSemantics
9.7s Strata.DDM.Util.Ion.Lean
9.6s StrataTest.Backends.CBMC.CoreToCProverGOTO
9.6s Strata.Languages.Core.WF
9.6s Strata.Languages.Core.OldExpressions
9.5s Strata.Languages.Laurel.LiftExpressionAssignments
9.3s Strata.Languages.Python.PyFactory
9.3s Strata.DL.Imperative.StmtSemantics
9.2s Strata.Languages.Python.PythonToCore:c.o (with exports)
9.2s Strata.Languages.Laurel.LaurelToCoreTranslator
9.2s Strata.DL.SMT.Term
9.1s Strata.Languages.Laurel.LaurelFormat
9.1s Strata.DL.Lambda.Reflect
9.1s Strata.DL.Lambda.LExprTypeSpec
9.1s Strata.DDM.Integration.Lean.ToExpr
9.0s Strata.DL.Util.StringGen
9.0s Strata.DDM.Integration.Lean.Gen
8.9s Strata.Languages.Python.Regex.ReParser
8.9s Strata.DL.Imperative.Stmt
8.8s Strata.Languages.Core.Env
8.8s Strata.DDM.Elab.DialectM
8.8s Strata.Backends.CBMC.Common
8.6s StrataTest.Internal.InternalCorePrelude
8.6s Strata.Languages.Core.FunctionType
8.6s Strata.Languages.Core.CallGraph
8.5s Strata.DL.Imperative.MetaData
8.5s Strata
8.4s StrataTest.Backends.CBMC.SimpleAdd.SimpleAdd
8.4s Strata.Languages.Core.CmdEval
8.3s Strata.DL.Lambda.IntBoolFactory
8.3s Strata.DL.Lambda.Factory
8.2s Strata.DL.Lambda.Scopes
8.2s Strata.DL.Imperative.StmtSemanticsSmallStep
8.2s Strata.DDM.Integration.Categories
8.1s Strata.Languages.Core.DDMTransform.Parse
8.1s Strata.DL.Lambda.TypeFactory
8.1s Strata.DL.Imperative.NondetStmtSemantics
8.0s Strata.Languages.Core.DDMTransform.Translate
7.9s Strata.Languages.Core.Procedure
7.9s Strata.DL.Util.Maps
7.8s Strata.Languages.Core.TypeDecl
7.8s Strata.Languages.Core.Function
7.8s Strata.DL.Imperative.CmdSemantics
7.7s Strata.Transform.LoopElim
7.7s Strata.Transform.DetToNondetCorrect
7.7s Strata.Languages.Core.CoreGen
7.7s Strata.DL.Lambda.LState
7.7s Strata.DL.Imperative.NondetStmt
7.7s Strata.DDM.Format
7.6s Strata.Languages.Core.Axiom
7.6s Strata.DDM.Util.Decimal
7.5s Strata.DL.SMT.TermType
7.5s Strata.DDM.Util.Graph.Tarjan
7.4s Strata.DL.Imperative.EvalError
7.4s Strata.DDM.Integration.Java.Gen
7.2s Strata.Languages.Laurel.HeapParameterization
7.2s Strata.DL.Imperative.HasVars
7.1s Strata.Languages.Laurel.Laurel
7.0s Strata.Transform.CoreTransform
7.0s Strata.DL.Lambda.Identifiers
6.9s Strata.Languages.Python.FunctionSignatures
6.9s Strata.DL.Imperative.EvalContext
6.9s Strata.DDM.Util.Ion.Deserialize
6.9s Strata.DDM.Ion:c.o (with exports)
6.9s Strata.Backends.CBMC.GOTO.Type
6.8s Strata.DL.Lambda.LExprT
6.8s Strata.DDM.Util.Ion.SymbolTable
6.7s StrataTest.Backends.CBMC.LambdaToCProverGOTO
6.7s Strata.Languages.C_Simp.C_Simp
6.7s Strata.DL.Util.Nodup
6.7s Strata.DL.Imperative.TypeContext
6.7s Strata.DDM.Util.Array
6.6s Strata.DL.Imperative.CmdType
6.6s Strata.DL.Imperative.CmdEval
6.6s Strata.Backends.CBMC.GOTO.SourceLocation
6.5s Strata.Languages.Core.Verifier
6.5s Strata.Languages.Core.Identifiers
6.5s Strata.DL.Util.List
6.5s Strata.DL.SMT.CexParser
6.5s Strata.DDM.Parser
6.4s Strata.DL.Util.Map
6.3s Strata.Languages.Core.ProcedureType
6.3s Strata.Languages.Core.Expressions
6.3s Strata.DL.Lambda.Semantics
6.2s Strata.Languages.Core.StatementEval
6.2s Strata.Languages.C_Simp.DDMTransform.Translate
6.2s Strata.DL.Util.ListUtils
6.2s Strata.DL.SMT.Solver
6.2s Strata.DDM.Elab.Env
6.1s Strata.Transform.DetToNondet
6.1s Strata.DL.Util.DecidableEq
6.1s Strata.DL.Lambda.MetaData
6.1s Strata.DL.Lambda.LExprWF
6.0s Strata.Transform.ProcedureInlining
6.0s Strata.Transform.CallElim
6.0s Strata.Languages.Core.StatementType
6.0s Strata.DDM.Integration.Lean.OfAstM
6.0s Strata.Backends.CBMC.GOTO.Instruction
5.9s Strata.DDM.Elab.Tree
5.9s Strata.Backends.CBMC.CoreToCBMC
5.8s StrataTest.Internal.InternalFunctionSignatures
5.8s Strata.Languages.Core.ProgramType
5.8s Strata.Languages.Core.ProcedureEval
5.8s Strata.DDM.Util.Ion
5.7s Strata.Languages.Laurel.Grammar.LaurelGrammar
5.7s Strata.Languages.Core.Options
5.7s Strata.DL.Util.Counter
5.7s Strata.DDM.Util.Lean
5.7s Strata.DDM.Util.Ion.Env
5.6s Strata.Languages.Core.Program
5.6s Strata.DL.Util.ListMap
5.6s Strata.DL.SMT.Factory
5.6s Strata.DDM.Util.ByteArray
5.6s Strata.DDM.Integration.Lean.GenTrace
5.5s Strata.DDM.Util.PrattParsingTables
5.5s Strata.DDM.Util.Ion.Serialize
5.5s Strata.DDM.BuiltinDialects.StrataDDL:c.o (with exports)
5.4s Strata.Languages.Python.Python
5.4s Strata.DL.Util.Relations
5.4s Strata.DL.Imperative.PureExpr
5.4s Strata.DDM.Util.List
5.4s Strata.DDM.Util.DecimalRat
5.3s StrataCoreToGoto
5.3s Strata.DDM.Integration.Lean.HashCommands
5.3s Strata.DDM.BuiltinDialects.Init
5.3s Strata.Backends.CBMC.GOTO.Expr
5.2s Strata.Languages.Core.ProgramEval
5.2s Strata.Languages.C_Simp.DDMTransform.Parse
5.1s Strata.DDM.Util.Ion.AST
5.1s Strata.DDM.Util.Fin
5.1s Strata.DDM.AST.Datatype
5.0s Strata.Util.IO
5.0s Strata.DL.SMT.Basic
5.0s Strata.DDM.Util.Nat
5.0s Strata.DDM.HNF
4.9s Strata.Languages.Laurel.Grammar.ConcreteToAbstractTreeTranslator
4.8s Strata.DL.Util.LabelGen
4.8s Strata.DDM.Util.Vector
4.7s Strata.DDM.Integration.Lean.Gen:c.o (with exports)
4.6s Strata.Languages.Core.Statement
4.6s Strata.DDM.BuiltinDialects.StrataDDL
4.5s Strata.Languages.Core.StatementType:c.o (with exports)
4.5s Strata.DDM.BuiltinDialects.StrataHeader
4.5s Strata.DDM.BuiltinDialects.BuiltinM
4.4s StrataTest.Backends.CBMC.ToCProverGOTO
4.4s StrataMain
4.4s Strata.DL.Imperative.SemanticsProps
4.3s Strata.Languages.Python.CorePrelude:c.o (with exports)
4.2s Strata.DL.SMT.DDMTransform.Translate
4.2s Strata.DL.Lambda.Lambda
4.2s Strata.DDM.Elab
4.2s Strata.DDM.AST:c.o (with exports)
4.1s Strata.DDM.Util.Ion.JSON
4.1s Strata.DDM.Integration.Lean.BoolConv
4.0s Strata.DL.Lambda.LExprType
4.0s Strata.DL.Imperative.Cmd
4.0s Strata.DDM.Util.String
4.0s Strata.DDM.Util.Format
4.0s Strata.DDM.BuiltinDialects
4.0s Strata.Backends.CBMC.GOTO.Program
4.0s Strata.Backends.CBMC.GOTO.Code
3.7s Strata.Languages.Core.Core
3.7s Strata.DDM.Integration.Lean.Env
3.6s Strata.DL.Imperative.Imperative
3.6s Strata.Backends.CBMC.GOTO.InstToJson
3.5s Strata.DDM.Integration.Lean
3.4s Strata.DL.Imperative.SMTUtils
3.4s Strata.DDM.Elab.DialectM:c.o (with exports)
3.3s Strata.DDM.Elab.LoadedDialects
3.3s Strata.DDM.Elab.Core:c.o (with exports)
3.2s Strata.DL.Lambda.LExpr:c.o (with exports)
3.1s Strata.DL.Imperative.ToCProverGOTO
3.1s Strata.DDM.Elab.SyntaxElab
3.1s Strata.Backends.CBMC.CProver
3.0s Strata.DL.SMT.Encoder
2.9s Strata.Languages.Core.FunctionType:c.o (with exports)
2.9s Strata.DDM.Elab.DeclM
2.8s Strata.Languages.Core.CmdType:c.o (with exports)
2.8s Strata.DL.SMT.SMT
2.4s Strata.DL.Lambda.LExprT:c.o (with exports)
2.2s Strata.Languages.Laurel.LaurelToCoreTranslator:c.o (with exports)
2.2s Strata.Languages.Core.Program:c.o (with exports)
2.1s strata:exe
2.0s StrataCoreToGoto:exe
2.0s Strata.Languages.C_Simp.DDMTransform.Translate:c.o (with exports)
1.9s Strata.Languages.Core.Factory:c.o (with exports)
1.9s Strata.Languages.Core.DDMTransform.Parse:c.o (with exports)
1.9s Strata.DDM.Util.Ion.Lean:c.o (with exports)
1.8s Strata.Backends.CBMC.Common:c.o (with exports)
1.7s Strata.DL.SMT.Op:c.o (with exports)
1.6s Strata.Languages.Core.Verifier:c.o (with exports)
1.6s Strata.DL.Lambda.LExprTypeEnv:c.o (with exports)
1.5s Strata.Languages.Laurel.Grammar.ConcreteToAbstractTreeTranslator:c.o (with exports)
1.5s Strata.DDM.Elab.Tree:c.o (with exports)
1.4s Strata.Languages.Core.Env:c.o (with exports)
1.4s Strata.DDM.Util.Ion.Deserialize:c.o (with exports)
1.3s Strata.Languages.Laurel.Laurel:c.o (with exports)
1.3s Strata.Languages.Core.ProgramType:c.o (with exports)
1.2s Strata.DDM.Format:c.o (with exports)
1.1s Strata.DDM.Parser:c.o (with exports)
1.1s Strata.DDM.Integration.Lean.ToExpr:c.o (with exports)
1.1s Strata.Backends.CBMC.GOTO.InstToJson:c.o (with exports)
1.0s Strata.Languages.Core.StatementEval:c.o (with exports)
1.0s Strata.Languages.Core.ProcedureType:c.o (with exports)
1.0s Strata.DL.SMT.Encoder:c.o (with exports)
946ms Strata.DDM.Integration.Java.Gen:c.o (with exports)
929ms StrataMain:c.o (with exports)
909ms Strata.DDM.Util.Ion.Serialize:c.o (with exports)
900ms StrataTest.Backends.CBMC.CoreToCProverGOTO:c.o (with exports)
889ms Strata.DDM.Elab:c.o (with exports)
852ms Strata.Languages.Core.Procedure:c.o (with exports)
837ms Strata.Languages.Core.Identifiers:c.o (with exports)
831ms Strata.DDM.Util.Ion.AST:c.o (with exports)
826ms Strata.Languages.Core.ProgramEval:c.o (with exports)
785ms Strata.DL.Lambda.TypeFactory:c.o (with exports)
757ms Strata.DDM.Integration.Lean.HashCommands:c.o (with exports)
738ms Strata.Languages.Python.Regex.ReParser:c.o (with exports)
698ms Strata.Transform.ProcedureInlining:c.o (with exports)
697ms Strata.DDM.Elab.DeclM:c.o (with exports)
694ms Strata.Backends.CBMC.GOTO.Expr:c.o (with exports)
690ms Strata.Languages.Laurel.HeapParameterization:c.o (with exports)
686ms Strata.Backends.CBMC.CoreToCBMC:c.o (with exports)
671ms Strata.Languages.Laurel.Grammar.LaurelGrammar:c.o (with exports)
667ms Strata.DL.SMT.Solver:c.o (with exports)
653ms Strata.DDM.Util.ByteArray:c.o (with exports)
596ms Strata.DL.Lambda.LTy:c.o (with exports)
575ms Strata.Languages.C_Simp.DDMTransform.Parse:c.o (with exports)
571ms Strata.DL.Lambda.LTyUnify:c.o (with exports)
559ms Strata.DL.Imperative.MetaData:c.o (with exports)
559ms Strata.Backends.CBMC.GOTO.Type:c.o (with exports)
558ms Strata.Languages.Core.Statement:c.o (with exports)
541ms Strata.DDM.Integration.Lean.OfAstM:c.o (with exports)
529ms Strata.DL.SMT.CexParser:c.o (with exports)
524ms Strata.DDM.Util.Ion:c.o (with exports)
518ms Strata.DL.SMT.Term:c.o (with exports)
501ms StrataTest.Backends.CBMC.LambdaToCProverGOTO:c.o (with exports)
494ms Strata.DL.Lambda.Reflect:c.o (with exports)
483ms Strata.DL.Imperative.Stmt:c.o (with exports)
471ms Strata.Backends.CBMC.GOTO.Code:c.o (with exports)
463ms Strata.DDM.Util.Ion.Env:c.o (with exports)
455ms Strata.Transform.CoreTransform:c.o (with exports)
454ms Strata.DL.Imperative.CmdType:c.o (with exports)
443ms Strata.DDM.Util.Ion.JSON:c.o (with exports)
439ms Strata.DL.Lambda.LExprWF:c.o (with exports)
434ms Strata.Languages.Core.StatementWF:c.o (with exports)
427ms Strata.Languages.Laurel.LiftExpressionAssignments:c.o (with exports)
426ms Strata.DL.SMT.Factory:c.o (with exports)
423ms Strata.DL.Lambda.Factory:c.o (with exports)
397ms Strata.DDM.TaggedRegions:c.o (with exports)
396ms Strata.DDM.Elab.SyntaxElab:c.o (with exports)
384ms Strata.DL.Lambda.LExprEval:c.o (with exports)
381ms Strata.Transform.CallElimCorrect:c.o (with exports)
365ms Strata.Languages.Core.OldExpressions:c.o (with exports)
361ms Strata.Languages.Core.Core:c.o (with exports)
355ms Strata.DDM.Elab.LoadedDialects:c.o (with exports)
349ms Strata.DL.Imperative.SMTUtils:c.o (with exports)
343ms Strata.Backends.CBMC.GOTO.SourceLocation:c.o (with exports)
342ms Strata.Languages.Core.ProgramWF:c.o (with exports)
338ms Strata.DL.Lambda.LState:c.o (with exports)
334ms Strata.DL.SMT.TermType:c.o (with exports)
332ms Strata.DL.Util.Map:c.o (with exports)
320ms Strata.DL.Imperative.ToCProverGOTO:c.o (with exports)
319ms Strata.Languages.Core.CallGraph:c.o (with exports)
318ms Strata.Languages.Laurel.LaurelFormat:c.o (with exports)
310ms Strata.DL.SMT.DDMTransform.Translate:c.o (with exports)
310ms Strata.DDM.AST.Datatype:c.o (with exports)
307ms Strata.Languages.Core.TypeDecl:c.o (with exports)
303ms Strata.DL.Util.DecidableEq:c.o (with exports)
300ms Strata.DDM.Integration.Lean.Env:c.o (with exports)
298ms Strata.Backends.CBMC.GOTO.Instruction:c.o (with exports)
295ms Strata.DL.Lambda.Scopes:c.o (with exports)
283ms Strata.DL.Imperative.EvalError:c.o (with exports)
283ms Strata.DDM.Util.Graph.Tarjan:c.o (with exports)
279ms Strata.DDM.Util.Ion.SymbolTable:c.o (with exports)
268ms Strata.Languages.Core.CmdEval:c.o (with exports)
261ms Strata.DL.Lambda.IntBoolFactory:c.o (with exports)
260ms Strata.DL.Lambda.Identifiers:c.o (with exports)
256ms Strata.DDM.BuiltinDialects.BuiltinM:c.o (with exports)
250ms Strata.DL.Imperative.CmdEval:c.o (with exports)
247ms Strata.DL.Util.ListMap:c.o (with exports)
246ms Strata.Languages.Core.ProcedureEval:c.o (with exports)
246ms Strata.DL.Util.Maps:c.o (with exports)
245ms Strata.DL.Imperative.Cmd:c.o (with exports)
244ms Strata.DL.Imperative.EvalContext:c.o (with exports)
243ms Strata.Languages.C_Simp.C_Simp:c.o (with exports)
232ms Strata.DDM.Util.Lean:c.o (with exports)
227ms StrataTest.Backends.CBMC.SimpleAdd.SimpleAdd:c.o (with exports)
225ms Strata.Languages.Python.FunctionSignatures:c.o (with exports)
221ms StrataTest.Backends.CBMC.ToCProverGOTO:c.o (with exports)
213ms Strata.Languages.Python.Regex.ReToCore:c.o (with exports)
206ms Strata.DL.SMT.Function:c.o (with exports)
206ms Strata.DDM.Integration.Categories:c.o (with exports)
204ms Strata.Languages.Python.PyFactory:c.o (with exports)
186ms Strata.DL.Util.Counter:c.o (with exports)
186ms Strata.DDM.Util.Decimal:c.o (with exports)
179ms Strata.DDM.Util.DecimalRat:c.o (with exports)
177ms Strata.Backends.CBMC.GOTO.Program:c.o (with exports)
172ms Strata.DL.Util.ListUtils:c.o (with exports)
166ms Strata.DL.Lambda.LExprTypeSpec:c.o (with exports)
164ms Strata.Transform.LoopElim:c.o (with exports)
164ms Strata.DDM.Util.Format:c.o (with exports)
157ms Strata.DL.Imperative.NondetStmt:c.o (with exports)
153ms Strata.DL.Util.LabelGen:c.o (with exports)
150ms Strata.Languages.Core.StatementSemanticsProps:c.o (with exports)
150ms Strata.DDM.Util.String:c.o (with exports)
138ms Strata.Transform.CallElim:c.o (with exports)
137ms Strata.DDM.Util.PrattParsingTables:c.o (with exports)
133ms Strata.Languages.Core.WF:c.o (with exports)
132ms Strata.Languages.Core.Options:c.o (with exports)
132ms Strata.DL.Util.Relations:c.o (with exports)
128ms Strata.DL.Util.StringGen:c.o (with exports)
127ms Strata.DDM.Elab.Env:c.o (with exports)
125ms Strata.DDM.BuiltinDialects.StrataHeader:c.o (with exports)
123ms Strata.DL.Util.List:c.o (with exports)
123ms Strata.DL.Lambda.Lambda:c.o (with exports)
123ms Strata.DDM.Integration.Lean.BoolConv:c.o (with exports)
122ms Strata.Languages.Core.Expressions:c.o (with exports)
122ms Strata.DL.SMT.Basic:c.o (with exports)
122ms Strata.DDM.BuiltinDialects:c.o (with exports)
121ms Strata.DL.Imperative.StmtSemanticsSmallStep:c.o (with exports)
119ms Strata.Languages.Core.StatementSemantics:c.o (with exports)
119ms Strata.DL.Lambda.MetaData:c.o (with exports)
117ms Strata.Languages.Core.Axiom:c.o (with exports)
111ms Strata.DDM.HNF:c.o (with exports)
110ms Strata.DL.SMT.SMT:c.o (with exports)
110ms Strata.DDM.Util.Fin:c.o (with exports)
107ms Strata.Transform.DetToNondetCorrect:c.o (with exports)
107ms Strata.DL.Lambda.Semantics:c.o (with exports)
106ms Strata.Languages.Core.CoreGen:c.o (with exports)
106ms Strata.DDM.Util.List:c.o (with exports)
104ms StrataCoreToGoto:c.o (with exports)
104ms Strata.DL.Imperative.HasVars:c.o (with exports)
101ms Strata.DL.Imperative.CmdSemantics:c.o (with exports)
101ms Strata.DDM.Util.Vector:c.o (with exports)
98ms Strata.DL.Imperative.NondetStmtSemantics:c.o (with exports)
96ms Strata.DDM.Integration.Lean.GenTrace:c.o (with exports)
95ms Strata.Transform.DetToNondet:c.o (with exports)
95ms Strata.DDM.Util.Nat:c.o (with exports)
94ms Strata.DL.Util.Nodup:c.o (with exports)
93ms Strata.DL.Imperative.PureExpr:c.o (with exports)
92ms Strata.DDM.Util.Array:c.o (with exports)
90ms Strata.Util.IO:c.o (with exports)
89ms Strata.DL.Imperative.StmtSemantics:c.o (with exports)
88ms Strata.DL.Imperative.TypeContext:c.o (with exports)
84ms Strata.DDM.Integration.Lean:c.o (with exports)
82ms Strata.DL.Imperative.SemanticsProps:c.o (with exports)
80ms Strata.Languages.Core.Function:c.o (with exports)
74ms Strata.DL.Imperative.Imperative:c.o (with exports)
74ms Strata.Backends.CBMC.CProver:c.o (with exports)
68ms Strata.Languages.Python.Python:c.o (with exports)
68ms Strata.DL.Lambda.LExprType:c.o (with exports)
67ms StrataTest.Internal.InternalCorePrelude:c.o (with exports)
65ms StrataTest.Internal.InternalFunctionSignatures:c.o (with exports)
63ms Strata:c.o (with exports)
62ms Strata.Languages.Core.ProcedureWF:c.o (with exports)