Ban open holes and code comments

[fredrik-bakke]

Add a pre-commit hook that checks for miscellaneous Agda conventions. It can effectively ban

• --allow-unsolved-metas flags
• Agda holes
• Agda line comments
• Agda block comments

Resolves #714.

[fredrik-bakke]

Summary from the script:

Top offending files:
  src/finite-group-theory/transpositions.lagda.md: 1 violations
  src/foundation/fibered-maps.lagda.md: 1 violations
  src/foundation/slice.lagda.md: 1 violations
  src/group-theory/contravariant-pushforward-concrete-group-actions.lagda.md: 1 violations
  src/linear-algebra/multiplication-matrices.lagda.md: 1 violations
  src/elementary-number-theory/reduced-integer-fractions.lagda.md: 2 violations
  src/reflection/arguments.lagda.md: 2 violations
  src/elementary-number-theory/sums-of-natural-numbers.lagda.md: 3 violations
  src/group-theory/category-of-concrete-groups.lagda.md: 3 violations
  src/lists/lists-discrete-types.lagda.md: 3 violations
  src/type-theories/simple-type-theories.lagda.md: 3 violations
  src/synthetic-homotopy-theory/26-descent.lagda.md: 4 violations
  src/synthetic-homotopy-theory/infinite-cyclic-types.lagda.md: 4 violations
  src/finite-algebra/semisimple-commutative-finite-rings.lagda.md: 6 violations
  src/foundation/pullbacks.lagda.md: 6 violations
  src/foundation/strongly-extensional-maps.lagda.md: 6 violations
  src/finite-group-theory/groups-of-order-2.lagda.md: 10 violations
  src/primitives/floats.lagda.md: 11 violations
  src/reflection/definitions.lagda.md: 12 violations
  src/species/hasse-weil-species.lagda.md: 12 violations
  src/reflection/terms.lagda.md: 16 violations
  src/reflection/type-checking-monad.lagda.md: 28 violations
  src/structured-types/wild-monoids.lagda.md: 32 violations
  src/foundation/partitions.lagda.md: 33 violations
  src/lists/universal-property-lists-wild-monoids.lagda.md: 38 violations
  src/trees/undirected-trees.lagda.md: 38 violations
  src/univalent-combinatorics/repetitions-of-values.lagda.md: 48 violations
  src/reflection/group-solver.lagda.md: 62 violations

Total violations: 387

[fredrik-bakke]

We should probably try to merge all of the scripts related to analyzing Agda code into one at some point. #638

[fredrik-bakke]

I'm not sure what to do with these violations at the moment. I expect that this PR will have to sit for a while while we figure out what to do with them.

[fredrik-bakke]

I will close this PR for the moment, but we can continue any discussion related to this in #714.