Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Andrew Hirsch
Pirouette Coq Code
Commits
6f803820
Commit
6f803820
authored
Jun 29, 2021
by
Andrew Hirsch
Browse files
New timing report.
parent
12990f1a
Changes
1
Hide whitespace changes
Inline
Side-by-side
report.txt
View file @
6f803820
`cloc --by-file-by-lang . --exclude-lang=make,D`
54
text files.
classified 5
2
files 5
2
unique files.
6
9 files ignored.
72
text files.
classified
6
5 files
6
5 unique files.
9
2
files ignored.
github.com/AlDanial/cloc v 1.82 T=0.0
6
s (2
75.8
files/s, 2
87127.4
lines/s)
github.com/AlDanial/cloc v 1.82 T=0.0
7
s (2
67.1
files/s, 2
31208.2
lines/s)
------------------------------------------------------------------------------------------
File blank comment code
------------------------------------------------------------------------------------------
./ChoreographyCompiler.v 184 335 4146
./ConcurrentLambda.v 225 964 3584
./Choreography.v 1
71
42
1
1817
./Choreography.v 1
80
42
6
2002
./TreeLocationMap.v 96 3 1604
./RestrictedSemantics.v 34 29 5
96
./RestrictedSemantics.v 34 29 5
75
./TypedChoreography.v 27 6 475
./LambdaCalc.v 48 60 408
./FunLMap.v 49 71 316
./STLC.v 14 0 161
./LocationMap.v 36 4 156
./Expression.v 14 11 93
./NatLang.v 28 0 154
./TypedNatLang.v 18 0 123
./UnitypedLC.v 17 0 103
./TypedExpression.v 14 0 84
./Expression.v 14 23 81
./STLCSound.v 5 0 65
./SoundlyTypedChoreography.v 8 0 34
./SoundlyTypedNatLang.v 5 0 30
./SoundlyTypedExpression.v 3 0 14
./Locations.v 39 22
1
1
3
./Locations.v 39 22
2
1
2
------------------------------------------------------------------------------------------
SUM:
967
21
25
1
3566
SUM:
1044
21
43
1
4127
------------------------------------------------------------------------------------------
-------------------------------------------------------------------------------
Language files blank comment code
-------------------------------------------------------------------------------
Coq
16
967
21
25
1
3566
Coq
20
1044
21
43
1
4127
-------------------------------------------------------------------------------
SUM:
16
967
21
25
1
3566
SUM:
20
1044
21
43
1
4127
-------------------------------------------------------------------------------
`make pretty-timed`
...
...
@@ -41,42 +45,51 @@ SUM: 16 967 2125 13566
make[3]: Nothing to be done for 'real-all'.
Time | Peak Mem | File Name
-----------------------------------------------------
23m45.99
s | 158
7
98
16
ko | Total Time / Peak Mem
38m20.11
s | 15898
564
ko | Total Time / Peak Mem
-----------------------------------------------------
13m16.74s | 761400 ko | RestrictedSemantics.vo
5m29.38s | 15879816 ko | ChoreographyCompiler.vo
4m33.27s | 1120036 ko | ConcurrentLambda.vo
0m21.98s | 619172 ko | Choreography.vo
0m02.69s | 486940 ko | TypedChoreography.vo
0m00.40s | 355284 ko | STLCSound.vo
0m00.36s | 439868 ko | FunLMap.vo
0m00.36s | 344816 ko | LambdaCalc.vo
0m00.30s | 371820 ko | SoundlyTypedChoreography.vo
0m00.20s | 346944 ko | STLC.vo
0m00.12s | 238724 ko | LocationMap.vo
0m00.07s | 149696 ko | Locations.vo
0m00.05s | 82760 ko | Expression.vo
0m00.04s | 79764 ko | TypedExpression.vo
0m00.03s | 64336 ko | SoundlyTypedExpression.vo
14m35.58s | 795940 ko | Choreography.vo
13m03.24s | 741840 ko | RestrictedSemantics.vo
5m46.46s | 15898564 ko | ChoreographyCompiler.vo
4m50.19s | 1120196 ko | ConcurrentLambda.vo
0m02.33s | 491104 ko | TypedChoreography.vo
0m00.37s | 355184 ko | STLCSound.vo
0m00.36s | 344856 ko | LambdaCalc.vo
0m00.32s | 439800 ko | FunLMap.vo
0m00.27s | 373508 ko | SoundlyTypedChoreography.vo
0m00.23s | 347044 ko | STLC.vo
0m00.15s | 275532 ko | TypedNatLang.vo
0m00.14s | 243072 ko | NatLang.vo
0m00.12s | 238792 ko | LocationMap.vo
0m00.09s | 167228 ko | UnitypedLC.vo
0m00.08s | 149712 ko | Locations.vo
0m00.07s | 176468 ko | SoundlyTypedNatLang.vo
0m00.05s | 78420 ko | Expression.vo
0m00.04s | 79696 ko | TypedExpression.vo
0m00.03s | 64208 ko | SoundlyTypedExpression.vo
`make pretty-timed TIMING_REAL=1`
make[3]: Nothing to be done for 'real-all'.
Time | Peak Mem | File Name
-----------------------------------------------------
23m05.48
s | 158
80036
ko | Total Time / Peak Mem
38m26.06
s | 158
98564
ko | Total Time / Peak Mem
-----------------------------------------------------
12m29.64s | 761376 ko | RestrictedSemantics.vo
5m39.00s | 15880036 ko | ChoreographyCompiler.vo
4m31.76s | 1120148 ko | ConcurrentLambda.vo
0m20.37s | 619096 ko | Choreography.vo
0m02.21s | 487140 ko | TypedChoreography.vo
0m00.46s | 344884 ko | LambdaCalc.vo
0m00.45s | 355280 ko | STLCSound.vo
0m00.43s | 439744 ko | FunLMap.vo
0m00.36s | 371816 ko | SoundlyTypedChoreography.vo
0m00.29s | 346880 ko | STLC.vo
0m00.20s | 238784 ko | LocationMap.vo
0m00.12s | 149840 ko | Locations.vo
0m00.07s | 82944 ko | Expression.vo
0m00.07s | 79616 ko | TypedExpression.vo
0m00.05s | 64108 ko | SoundlyTypedExpression.vo
14m35.88s | 795940 ko | Choreography.vo
13m03.55s | 741840 ko | RestrictedSemantics.vo
5m50.33s | 15898564 ko | ChoreographyCompiler.vo
4m50.53s | 1120196 ko | ConcurrentLambda.vo
0m02.48s | 491104 ko | TypedChoreography.vo
0m00.48s | 355184 ko | STLCSound.vo
0m00.47s | 344856 ko | LambdaCalc.vo
0m00.46s | 439800 ko | FunLMap.vo
0m00.37s | 373508 ko | SoundlyTypedChoreography.vo
0m00.29s | 347044 ko | STLC.vo
0m00.23s | 275532 ko | TypedNatLang.vo
0m00.21s | 243072 ko | NatLang.vo
0m00.20s | 238792 ko | LocationMap.vo
0m00.14s | 176468 ko | SoundlyTypedNatLang.vo
0m00.14s | 167228 ko | UnitypedLC.vo
0m00.12s | 149712 ko | Locations.vo
0m00.07s | 78420 ko | Expression.vo
0m00.07s | 79696 ko | TypedExpression.vo
0m00.05s | 64208 ko | SoundlyTypedExpression.vo
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment
