wip line counts

Author: samuelgruetter

loc/PrintLibraries.txt

@@ -0,0 +1,231 @@
+Logical Path / Physical path:
+Rewriter /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rewriter/src/Rewriter
+Rewriter.Language /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rewriter/src/Rewriter/Language
+Rewriter.Rewriter /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rewriter/src/Rewriter/Rewriter
+Rewriter.Rewriter.Examples /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rewriter/src/Rewriter/Rewriter/Examples
+Rewriter.Rewriter.Examples.PerfTesting /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rewriter/src/Rewriter/Rewriter/Examples/PerfTesting
+Rewriter.Util /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rewriter/src/Rewriter/Util
+Rewriter.Util.Bool /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rewriter/src/Rewriter/Util/Bool
+Rewriter.Util.FMapPositive /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rewriter/src/Rewriter/Util/FMapPositive
+Rewriter.Util.ListUtil /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rewriter/src/Rewriter/Util/ListUtil
+Rewriter.Util.Logic /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rewriter/src/Rewriter/Util/Logic
+Rewriter.Util.MSetPositive /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rewriter/src/Rewriter/Util/MSetPositive
+Rewriter.Util.Sigma /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rewriter/src/Rewriter/Util/Sigma
+Rewriter.Util.Strings /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rewriter/src/Rewriter/Util/Strings
+Rewriter.Util.Strings.Parse /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rewriter/src/Rewriter/Util/Strings/Parse
+Rewriter.Util.Tactics /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rewriter/src/Rewriter/Util/Tactics
+Rewriter.Util.Tactics2 /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rewriter/src/Rewriter/Util/Tactics2
+Rewriter.Util.Tactics2.Constr /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rewriter/src/Rewriter/Util/Tactics2/Constr
+Rewriter.Util.Tactics2.Constr.Unsafe /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rewriter/src/Rewriter/Util/Tactics2/Constr/Unsafe
+Rewriter.Util.plugins /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rewriter/src/Rewriter/Util/plugins
+riscv /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/deps/riscv-coq/src/riscv
+riscv.Examples /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples
+riscv.Examples.smt /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/smt
+riscv.Platform /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform
+riscv.Proofs /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs
+riscv.Spec /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec
+riscv.Utility /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility
+compiler /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/compiler/src/compiler
+compiler.util /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/compiler/src/compiler/util
+bedrock2Examples /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/bedrock2/src/bedrock2Examples
+bedrock2 /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/bedrock2/src/bedrock2
+bedrock2.Map /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/bedrock2/src/bedrock2/Map
+Rupicola /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/src/Rupicola
+Rupicola.Examples /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/src/Rupicola/Examples
+Rupicola.Examples.Assoc /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/src/Rupicola/Examples/Assoc
+Rupicola.Examples.CMove /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/src/Rupicola/Examples/CMove
+Rupicola.Examples.CRC32 /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/src/Rupicola/Examples/CRC32
+Rupicola.Examples.CapitalizeThird /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/src/Rupicola/Examples/CapitalizeThird
+Rupicola.Examples.Cells /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/src/Rupicola/Examples/Cells
+Rupicola.Examples.IO /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/src/Rupicola/Examples/IO
+Rupicola.Examples.KVStore /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/src/Rupicola/Examples/KVStore
+Rupicola.Examples.LinkedList /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/src/Rupicola/Examples/LinkedList
+Rupicola.Examples.Net /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/src/Rupicola/Examples/Net
+Rupicola.Examples.Net.IPChecksum /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/src/Rupicola/Examples/Net/IPChecksum
+Rupicola.Examples.Nondeterminism /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/src/Rupicola/Examples/Nondeterminism
+Rupicola.Examples.RevComp /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/src/Rupicola/Examples/RevComp
+Rupicola.Examples.Swap /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/src/Rupicola/Examples/Swap
+Rupicola.Examples.Tree /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/src/Rupicola/Examples/Tree
+Rupicola.Examples.Uppercase /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/src/Rupicola/Examples/Uppercase
+Rupicola.Examples.Utf8 /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/src/Rupicola/Examples/Utf8
+Rupicola.Examples.fnv1a64 /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/src/Rupicola/Examples/fnv1a64
+Rupicola.Examples.murmur3 /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/src/Rupicola/Examples/murmur3
+Rupicola.Lib /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/src/Rupicola/Lib
+Rupicola.Lib.ControlFlow /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/src/Rupicola/Lib/ControlFlow
+coqutil /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/deps/coqutil/src/coqutil
+coqutil.Datatypes /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes
+coqutil.Ltac2Lib /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/deps/coqutil/src/coqutil/Ltac2Lib
+coqutil.Macros /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/deps/coqutil/src/coqutil/Macros
+coqutil.Map /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/deps/coqutil/src/coqutil/Map
+coqutil.Sorting /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/deps/coqutil/src/coqutil/Sorting
+coqutil.Tactics /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics
+coqutil.Word /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/deps/coqutil/src/coqutil/Word
+coqutil.Z /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/rupicola/bedrock2/deps/coqutil/src/coqutil/Z
+Coqprime /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/coqprime/src/Coqprime
+Coqprime.List /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/coqprime/src/Coqprime/List
+Coqprime.N /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/coqprime/src/Coqprime/N
+Coqprime.PrimalityTest /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/coqprime/src/Coqprime/PrimalityTest
+Coqprime.Tactic /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/coqprime/src/Coqprime/Tactic
+Coqprime.Z /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/coqprime/src/Coqprime/Z
+Coqprime.elliptic /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/coqprime/src/Coqprime/elliptic
+Coqprime.examples /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/coqprime/src/Coqprime/examples
+Coqprime.examples.t100 /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/coqprime/src/Coqprime/examples/t100
+Coqprime.examples.t125 /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/coqprime/src/Coqprime/examples/t125
+Coqprime.examples.t150 /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/coqprime/src/Coqprime/examples/t150
+Coqprime.examples.t175 /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/coqprime/src/Coqprime/examples/t175
+Coqprime.examples.t200 /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/coqprime/src/Coqprime/examples/t200
+Coqprime.examples.t225 /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/coqprime/src/Coqprime/examples/t225
+Coqprime.examples.t25 /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/coqprime/src/Coqprime/examples/t25
+Coqprime.examples.t250 /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/coqprime/src/Coqprime/examples/t250
+Coqprime.examples.t50 /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/coqprime/src/Coqprime/examples/t50
+Coqprime.examples.t75 /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/coqprime/src/Coqprime/examples/t75
+Coqprime.num /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/coqprime/src/Coqprime/num
+Coqprime.num.extraction /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/coqprime/src/Coqprime/num/extraction
+Crypto /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src
+Crypto.AbstractInterpretation /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/AbstractInterpretation
+Crypto.Algebra /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Algebra
+Crypto.Arithmetic /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Arithmetic
+Crypto.Arithmetic.BarrettReduction /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Arithmetic/BarrettReduction
+Crypto.Arithmetic.MontgomeryReduction /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Arithmetic/MontgomeryReduction
+Crypto.ArithmeticCPS /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/ArithmeticCPS
+Crypto.Assembly /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Assembly
+Crypto.Assembly.Parse /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Assembly/Parse
+Crypto.Assembly.Parse.Examples /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Assembly/Parse/Examples
+Crypto.Assembly.WithBedrock /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Assembly/WithBedrock
+Crypto.Bedrock /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Bedrock
+Crypto.Bedrock.End2End /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Bedrock/End2End
+Crypto.Bedrock.End2End.Poly1305 /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Bedrock/End2End/Poly1305
+Crypto.Bedrock.End2End.RupicolaCrypto /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Bedrock/End2End/RupicolaCrypto
+Crypto.Bedrock.End2End.X25519 /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Bedrock/End2End/X25519
+Crypto.Bedrock.Field /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Bedrock/Field
+Crypto.Bedrock.Field.Common /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Bedrock/Field/Common
+Crypto.Bedrock.Field.Common.Arrays /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Bedrock/Field/Common/Arrays
+Crypto.Bedrock.Field.Common.Names /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Bedrock/Field/Common/Names
+Crypto.Bedrock.Field.Interface /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Bedrock/Field/Interface
+Crypto.Bedrock.Field.Stringification /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Bedrock/Field/Stringification
+Crypto.Bedrock.Field.Synthesis /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Bedrock/Field/Synthesis
+Crypto.Bedrock.Field.Synthesis.Examples /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Bedrock/Field/Synthesis/Examples
+Crypto.Bedrock.Field.Synthesis.Generic /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Bedrock/Field/Synthesis/Generic
+Crypto.Bedrock.Field.Synthesis.New /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Bedrock/Field/Synthesis/New
+Crypto.Bedrock.Field.Translation /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Bedrock/Field/Translation
+Crypto.Bedrock.Field.Translation.Parameters /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Bedrock/Field/Translation/Parameters
+Crypto.Bedrock.Field.Translation.Proofs /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Bedrock/Field/Translation/Proofs
+Crypto.Bedrock.Field.Translation.Proofs.ValidComputable /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Bedrock/Field/Translation/Proofs/ValidComputable
+Crypto.Bedrock.Group /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Bedrock/Group
+Crypto.Bedrock.Group.ScalarMult /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Bedrock/Group/ScalarMult
+Crypto.Bedrock.Specs /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Bedrock/Specs
+Crypto.Bedrock.Standalone /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Bedrock/Standalone
+Crypto.Curves /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Curves
+Crypto.Curves.Edwards /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Curves/Edwards
+Crypto.Curves.Edwards.XYZT /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Curves/Edwards/XYZT
+Crypto.Curves.Montgomery /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Curves/Montgomery
+Crypto.Curves.TableMult /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Curves/TableMult
+Crypto.Curves.Weierstrass /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Curves/Weierstrass
+Crypto.ExtractionHaskell /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/ExtractionHaskell
+Crypto.ExtractionJsOfOCaml /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/ExtractionJsOfOCaml
+Crypto.ExtractionOCaml /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/ExtractionOCaml
+Crypto.Fancy /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Fancy
+Crypto.Language /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Language
+Crypto.PerfTesting /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/PerfTesting
+Crypto.Primitives /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Primitives
+Crypto.PushButtonSynthesis /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/PushButtonSynthesis
+Crypto.Rewriter /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Rewriter
+Crypto.Rewriter.Passes /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Rewriter/Passes
+Crypto.Rewriter.PerfTesting /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Rewriter/PerfTesting
+Crypto.Rewriter.PerfTesting.Specific /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Rewriter/PerfTesting/Specific
+Crypto.Rewriter.PerfTesting.Specific.generated /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Rewriter/PerfTesting/Specific/generated
+Crypto.Spec /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Spec
+Crypto.Spec.Test /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Spec/Test
+Crypto.Stringification /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Stringification
+Crypto.UnsaturatedSolinasHeuristics /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/UnsaturatedSolinasHeuristics
+Crypto.Util /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util
+Crypto.Util.Bool /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/Bool
+Crypto.Util.Decidable /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/Decidable
+Crypto.Util.ErrorT /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/ErrorT
+Crypto.Util.FSets /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/FSets
+Crypto.Util.FSets.FMapTrie /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/FSets/FMapTrie
+Crypto.Util.ListUtil /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/ListUtil
+Crypto.Util.Logic /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/Logic
+Crypto.Util.MSets /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/MSets
+Crypto.Util.MSets.FMapPositive /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/MSets/FMapPositive
+Crypto.Util.MSets.MSetPositive /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/MSets/MSetPositive
+Crypto.Util.NUtil /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/NUtil
+Crypto.Util.SideConditions /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/SideConditions
+Crypto.Util.Sigma /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/Sigma
+Crypto.Util.Sorting /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/Sorting
+Crypto.Util.Sorting.Sorted /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/Sorting/Sorted
+Crypto.Util.Strings /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/Strings
+Crypto.Util.Strings.Parse /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/Strings/Parse
+Crypto.Util.Strings.Show /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/Strings/Show
+Crypto.Util.Structures /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/Structures
+Crypto.Util.Structures.Equalities /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/Structures/Equalities
+Crypto.Util.Structures.Orders /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/Structures/Orders
+Crypto.Util.Tactics /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/Tactics
+Crypto.Util.Telescope /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/Telescope
+Crypto.Util.ZRange /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/ZRange
+Crypto.Util.ZUtil /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/ZUtil
+Crypto.Util.ZUtil.Div /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/ZUtil/Div
+Crypto.Util.ZUtil.Divide /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/ZUtil/Divide
+Crypto.Util.ZUtil.Hints /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/ZUtil/Hints
+Crypto.Util.ZUtil.Land /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/ZUtil/Land
+Crypto.Util.ZUtil.Modulo /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/ZUtil/Modulo
+Crypto.Util.ZUtil.Tactics /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/ZUtil/Tactics
+Crypto.Util.ZUtil.Tactics.PullPush /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/ZUtil/Tactics/PullPush
+Crypto.Util.ZUtil.ZSimplify /home/sam/git/fiat-crypto-garagedoor-loc-coq-8.18.0/src/Util/ZUtil/ZSimplify
+<> /home/sam/.opam/WithCoq8180/lib/coq/user-contrib
+Ltac2 /home/sam/.opam/WithCoq8180/lib/coq/user-contrib/Ltac2
+Coq /home/sam/.opam/WithCoq8180/lib/coq/theories
+Coq.Arith /home/sam/.opam/WithCoq8180/lib/coq/theories/Arith
+Coq.Array /home/sam/.opam/WithCoq8180/lib/coq/theories/Array
+Coq.Bool /home/sam/.opam/WithCoq8180/lib/coq/theories/Bool
+Coq.Classes /home/sam/.opam/WithCoq8180/lib/coq/theories/Classes
+Coq.Compat /home/sam/.opam/WithCoq8180/lib/coq/theories/Compat
+Coq.FSets /home/sam/.opam/WithCoq8180/lib/coq/theories/FSets
+Coq.Floats /home/sam/.opam/WithCoq8180/lib/coq/theories/Floats
+Coq.Init /home/sam/.opam/WithCoq8180/lib/coq/theories/Init
+Coq.Lists /home/sam/.opam/WithCoq8180/lib/coq/theories/Lists
+Coq.Logic /home/sam/.opam/WithCoq8180/lib/coq/theories/Logic
+Coq.MSets /home/sam/.opam/WithCoq8180/lib/coq/theories/MSets
+Coq.NArith /home/sam/.opam/WithCoq8180/lib/coq/theories/NArith
+Coq.Numbers /home/sam/.opam/WithCoq8180/lib/coq/theories/Numbers
+Coq.Numbers.Cyclic /home/sam/.opam/WithCoq8180/lib/coq/theories/Numbers/Cyclic
+Coq.Numbers.Cyclic.Abstract /home/sam/.opam/WithCoq8180/lib/coq/theories/Numbers/Cyclic/Abstract
+Coq.Numbers.Cyclic.Int31 /home/sam/.opam/WithCoq8180/lib/coq/theories/Numbers/Cyclic/Int31
+Coq.Numbers.Cyclic.Int63 /home/sam/.opam/WithCoq8180/lib/coq/theories/Numbers/Cyclic/Int63
+Coq.Numbers.Cyclic.ZModulo /home/sam/.opam/WithCoq8180/lib/coq/theories/Numbers/Cyclic/ZModulo
+Coq.Numbers.Integer /home/sam/.opam/WithCoq8180/lib/coq/theories/Numbers/Integer
+Coq.Numbers.Integer.Abstract /home/sam/.opam/WithCoq8180/lib/coq/theories/Numbers/Integer/Abstract
+Coq.Numbers.Integer.Binary /home/sam/.opam/WithCoq8180/lib/coq/theories/Numbers/Integer/Binary
+Coq.Numbers.Integer.NatPairs /home/sam/.opam/WithCoq8180/lib/coq/theories/Numbers/Integer/NatPairs
+Coq.Numbers.NatInt /home/sam/.opam/WithCoq8180/lib/coq/theories/Numbers/NatInt
+Coq.Numbers.Natural /home/sam/.opam/WithCoq8180/lib/coq/theories/Numbers/Natural
+Coq.Numbers.Natural.Abstract /home/sam/.opam/WithCoq8180/lib/coq/theories/Numbers/Natural/Abstract
+Coq.Numbers.Natural.Binary /home/sam/.opam/WithCoq8180/lib/coq/theories/Numbers/Natural/Binary
+Coq.Numbers.Natural.Peano /home/sam/.opam/WithCoq8180/lib/coq/theories/Numbers/Natural/Peano
+Coq.PArith /home/sam/.opam/WithCoq8180/lib/coq/theories/PArith
+Coq.Program /home/sam/.opam/WithCoq8180/lib/coq/theories/Program
+Coq.QArith /home/sam/.opam/WithCoq8180/lib/coq/theories/QArith
+Coq.Reals /home/sam/.opam/WithCoq8180/lib/coq/theories/Reals
+Coq.Reals.Abstract /home/sam/.opam/WithCoq8180/lib/coq/theories/Reals/Abstract
+Coq.Reals.Cauchy /home/sam/.opam/WithCoq8180/lib/coq/theories/Reals/Cauchy
+Coq.Relations /home/sam/.opam/WithCoq8180/lib/coq/theories/Relations
+Coq.Setoids /home/sam/.opam/WithCoq8180/lib/coq/theories/Setoids
+Coq.Sets /home/sam/.opam/WithCoq8180/lib/coq/theories/Sets
+Coq.Sorting /home/sam/.opam/WithCoq8180/lib/coq/theories/Sorting
+Coq.Strings /home/sam/.opam/WithCoq8180/lib/coq/theories/Strings
+Coq.Structures /home/sam/.opam/WithCoq8180/lib/coq/theories/Structures
+Coq.Unicode /home/sam/.opam/WithCoq8180/lib/coq/theories/Unicode
+Coq.Vectors /home/sam/.opam/WithCoq8180/lib/coq/theories/Vectors
+Coq.Wellfounded /home/sam/.opam/WithCoq8180/lib/coq/theories/Wellfounded
+Coq.ZArith /home/sam/.opam/WithCoq8180/lib/coq/theories/ZArith
+Coq.btauto /home/sam/.opam/WithCoq8180/lib/coq/theories/btauto
+Coq.derive /home/sam/.opam/WithCoq8180/lib/coq/theories/derive
+Coq.extraction /home/sam/.opam/WithCoq8180/lib/coq/theories/extraction
+Coq.funind /home/sam/.opam/WithCoq8180/lib/coq/theories/funind
+Coq.micromega /home/sam/.opam/WithCoq8180/lib/coq/theories/micromega
+Coq.nsatz /home/sam/.opam/WithCoq8180/lib/coq/theories/nsatz
+Coq.omega /home/sam/.opam/WithCoq8180/lib/coq/theories/omega
+Coq.rtauto /home/sam/.opam/WithCoq8180/lib/coq/theories/rtauto
+Coq.setoid_ring /home/sam/.opam/WithCoq8180/lib/coq/theories/setoid_ring
+Coq.ssr /home/sam/.opam/WithCoq8180/lib/coq/theories/ssr
+Coq.ssrmatching /home/sam/.opam/WithCoq8180/lib/coq/theories/ssrmatching

loc/PrintLoadPath.txt

@@ -1,8 +1,24 @@
+# Usage:
+#
+# At the end of src/Bedrock/End2End/X25519/GarageDoorTop.v, insert the following commands:
+#
+# Set Printing Width 10000.
+# Print LoadPath.
+# Print Libraries.
+#
+# and copy-paste their outputs to loc/PrintLoadPath.txt and loc/PrintLibraries.txt, respectively.
+# Append '  Crypto.Bedrock.End2End.X25519.GarageDoorTop' to loc/PrintLibraries.txt.
+# Then, run
+# python3 loc/count.py
+
 import re
+import collections
+import subprocess
+from subprocess import PIPE
 
 def parseLoadPath():
     d = dict()
-    with open('PrintLoadPath.txt') as f:
+    with open('./loc/PrintLoadPath.txt') as f:
         for line in f:
             a = line.strip().split()
             if len(a) == 2:
@@ -11,30 +27,60 @@ def parseLoadPath():
 
 loadPath = parseLoadPath()
 
-def getLibraryList():
+def rootOfLogicalDir(logicalDir):
+    m = re.match(r'([^.]+)', logicalDir)
+    root = m[1]
+    # we treat the toplevel Ltac2 root as if it was under Coq
+    if root == 'Ltac2':
+        return 'Coq'
+    else:
+        return root
+
+# returns a dictionary that maps logical roots (eg Coq, bedrock2, riscv, Crypto, ...)
+# to lists of absolute paths
+def getLibraries():
     global loadPath
-    l = []
-    with open('PrintLibraries.txt') as f:
+    libs = collections.defaultdict(list)
+    with open('./loc/PrintLibraries.txt') as f:
         for line in f:
             m = re.match(r'  (.*)\.([^.]+)', line.rstrip())
             if m:
                 logicalDir = m[1]
                 libName = m[2]
                 physicalDir = loadPath[logicalDir]
-                l.append(f'{physicalDir}/{libName}.v')
+                root = rootOfLogicalDir(logicalDir)
+                absPath = f'{physicalDir}/{libName}.v'
+                libs[root].append(absPath)
             else:
                 assert(line == "Loaded library files:\n")
-    return l
+    return libs
 
-def getRoots():
-    global loadPath
-    s = set()
-    for logicalDir in loadPath:
-        m = re.match(r'([^.]+)', logicalDir)
-        root = m[1]
-        if root != '<>':
-            s.add(m[1])
-    return s
-
-print('\n'.join(getLibraryList()))
-print(getRoots())
+def printLibraries():
+    for root, files in getLibraries().items():
+        print(f'{root}:')
+        for file in files:
+            print(f'  {file}')
+
+def cloc_list_of_coq_files(filePaths):
+    p = subprocess.Popen(['cloc', '--list-file=-', '--include-lang=Coq',
+                          '--csv', '--quiet', '--hide-rate'],
+                         stdout=PIPE, stdin=PIPE, stderr=PIPE, text=True)
+    (stdout_data, stderr_data) = p.communicate(input = '\n'.join(filePaths))
+    if stderr_data:
+        print(stderr_data)
+    #sample output:
+    #
+    #files,language,blank,comment,code,"github.com/AlDanial/cloc v 1.90"
+    #599,Coq,16445,8171,132933
+    #599,SUM,16445,8171,132933
+    a = stdout_data.split(',')
+    return int(a[-1]) # last number is the one we want
+
+printLibraries()
+
+def go():
+    for root, files in getLibraries().items():
+        c = cloc_list_of_coq_files(files)
+        print(f'{root}: {c}')
+
+go()

loc/count.py

@@ -0,0 +1,10 @@
+Coq: 85495
+Crypto: 82198
+Coqprime: 5650
+coqutil: 11349
+bedrock2: 7411
+riscv: 6490
+compiler: 13958
+Rupicola: 8198
+Rewriter: 30124
+bedrock2Examples: 2359

loc/count.py.out

@@ -0,0 +1,24 @@
+## Garagedoor app (init, loop, initfn, loopfn) [Bedrock2]
+Crypto.Bedrock.End2End.X25519.GarageDoor
+Crypto.Bedrock.End2End.X25519.GarageDoorTop
+
+## Ethernet/LAN/SPI (lan9250_tx) [Bedrock2]
+134 lines of bedrock2Examples.LAN9250
+
+## Bedrock2 library functions (memswap, memequal, memconst) [Bedrock2]
+bedrock2Examples.memequal
+bedrock2Examples.memswap
+bedrock2Examples.memconst
+
+## Chacha20 (chacha20_block, quarter) [Rupicola]
+Crypto.Bedrock.End2End.RupicolaCrypto.ChaCha20
+
+## Montgomery ladder (x25519, x25519_base) [Bedrock2]
+Crypto.Bedrock.End2End.X25519.MontgomeryLadder
+Crypto.Bedrock.End2End.X25519.MontgomeryLadderProperties
+
+## Montgomery ladder (montladder, ladderstep) [Rupicola]
+Crypto.Bedrock.End2End.RupicolaCrypto.Spec
+
+## Modular inversion using addition-chain exponentiation (fe25519_inv) [simpl & Rupicola]
+Crypto.Bedrock.Group.AdditionChains