IntersectMBO / IntersectMBO/formal-ledger-specifications
Typechecking time spent on OccursCheck is surprisingly high
- Dominant language
- Agda
- Stars
- 52
- Forks
- 20
- Avg merge
- 6d 14h
- Merged PRs (30d)
- 7
Description
Typechecking the file `src/Ledger/Specification/Epoch/Properties.agda` in commit 6f730a7a1bb23340ef02c6593e71bdd40d0b1597 produces the following times:
```
Total 179,952ms
Miscellaneous 19ms
Typing 4,709ms (129,551ms)
Typing.OccursCheck 85,722ms
Typing.CheckRHS 37,407ms
Typing.With 684ms
Typing.CheckLHS 279ms (657ms)
Typing.CheckLHS.UnifyIndices 378ms
Typing.InstanceSearch 5ms (332ms)
Typing.InstanceSearch.InitialCandidates 249ms
Typing.InstanceSearch.FilterCandidates 77ms
Typing.TypeSig 37ms
Deserialization 14,690ms (19,525ms)
Deserialization.Compaction 4,835ms
InterfaceInstantiateFull 8,958ms
DeadCode 2ms (6,900ms)
DeadCode.DeadCodeReachable 6,897ms
Positivity 5,423ms
Coverage 2,281ms (3,949ms)
Coverage.UnifyIndices 1,667ms
ProjectionLikeness 3,713ms
Termination 0ms (1,355ms)
Termination.RecCheck 1,355ms
Parsing 10ms (197ms)
Parsing.OperatorsExpr 141ms
Parsing.OperatorsPattern 46ms
Scoping 29ms (187ms)
Scoping.InverseScopeLookup 157ms
Import 151ms
Highlighting 17ms
```
applying the commit f10b4c29d05cc2af7f93d46b8fbcf4bcc4f098e8 this changes to:
```
Total 156,490ms
Miscellaneous 55ms
Deserialization 50,306ms (66,346ms)
Deserialization.Compaction 16,039ms
Typing 5,148ms (34,577ms)
Typing.CheckRHS 25,129ms
Typing.CheckLHS 434ms (1,674ms)
Typing.CheckLHS.UnifyIndices 1,240ms
Typing.OccursCheck 1,246ms
Typing.InstanceSearch 13ms (653ms)
Typing.InstanceSearch.InitialCandidates 420ms
Typing.InstanceSearch.FilterCandidates 219ms
Typing.With 632ms
Typing.TypeSig 91ms
Positivity 16,835ms
ProjectionLikeness 11,008ms
DeadCode 1ms (9,819ms)
DeadCode.DeadCodeReachable 9,817ms
Coverage 4,978ms (7,385ms)
Coverage.UnifyIndices 2,407ms
Termination 0ms (5,941ms)
Termination.RecCheck 5,940ms
InterfaceInstantiateFull 2,261ms
Parsing 13ms (1,327ms)
Parsing.OperatorsExpr 990ms
Parsing.OperatorsPattern 323ms
Import 448ms
Scoping 138ms (396ms)
Scoping.InverseScopeLookup 258ms
Highlighting 76ms
Injectivity 10ms
```
Time spent on OccursCheck is quite different. This might be an Agda feature/bug. Requires further investigation.
Contributor guide
Assessment
This issue has not been assessed yet.