IntersectMBO / IntersectMBO/formal-ledger-specifications

Typechecking time spent on OccursCheck is surprisingly high

Open
#850 4 comments 0 reactions 0 assignees View on GitHub
investigation possibly difficult
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

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.