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
31bf98b9
Commit
31bf98b9
authored
Jun 27, 2021
by
Andrew Hirsch
Browse files
Added a report containing some statistics about the Coq implementation.
parent
01f809c7
Changes
1
Hide whitespace changes
Inline
Side-by-side
report.txt
0 → 100644
View file @
31bf98b9
`cloc --by-file-by-lang . --exclude-lang=make,D`
54 text files.
classified 52 files 52 unique files.
69 files ignored.
github.com/AlDanial/cloc v 1.82 T=0.06 s (275.8 files/s, 287127.4 lines/s)
------------------------------------------------------------------------------------------
File blank comment code
------------------------------------------------------------------------------------------
./ChoreographyCompiler.v 184 335 4146
./ConcurrentLambda.v 225 964 3584
./Choreography.v 171 421 1817
./TreeLocationMap.v 96 3 1604
./RestrictedSemantics.v 34 29 596
./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
./TypedExpression.v 14 0 84
./STLCSound.v 5 0 65
./SoundlyTypedChoreography.v 8 0 34
./SoundlyTypedExpression.v 3 0 14
./Locations.v 39 221 13
------------------------------------------------------------------------------------------
SUM: 967 2125 13566
------------------------------------------------------------------------------------------
-------------------------------------------------------------------------------
Language files blank comment code
-------------------------------------------------------------------------------
Coq 16 967 2125 13566
-------------------------------------------------------------------------------
SUM: 16 967 2125 13566
-------------------------------------------------------------------------------
`make pretty-timed`
make[3]: Nothing to be done for 'real-all'.
Time | Peak Mem | File Name
-----------------------------------------------------
23m45.99s | 15879816 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
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