the build output contains a lot of noise

[andres-erbsen]

let's try to reduce it as we refactor files?

[JasonGross]

Some of the noise is as described in #105.

Some of the other noise is things like:

Warning: Notation "_ /\ _" was already used in scope type_scope.
[notation-overridden,parsing]

In fiat-crypto, we just disable this warning with OTHERFLAGS += -w "-notation-overridden" passed along to Coq's makefile, because currently there's no way of getting this warning only in legitimate cases (see coq/coq#4962 and coq/coq#5593).

More noise is due to the fact that coq_makefile is given a list of absolute paths to .v files. This is unnecessary, and you can give all the paths relative to the directory that the Makefile is in, which would make each line shorter and more readable

It looks like some files have tactics with unused intro patterns, where you just need to fix the tactic. (This one is actually basically reasonable to make into a global error, to enforce good coding style.)

File "/home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/ptsto_bytes.v", line 141, characters 6-173:
Warning: Unused introduction patterns: R IH [unused-intro-pattern,tactics]
/home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Examples/ARPResponder (real: 0.59, user: 0.49, sys: 0.09, mem: 399408 ko)
File "/home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/ptsto_bytes.v", line 153, characters 6-132:
Warning: Unused introduction patterns: R IH [unused-intro-pattern,tactics]
/home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/ptsto_bytes (real: 9.48, user: 9.31, sys: 0.16, mem: 564600 ko)
COQC /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Scalars.v
File "/home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Scalars.v", line 180, characters 4-51:
Warning: Unused introduction pattern: ? [unused-intro-pattern,tactics]
File "/home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Scalars.v", line 180, characters 4-51:
Warning: Unused introduction pattern: ? [unused-intro-pattern,tactics]
File "/home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Scalars.v", line 194, characters 4-51:
Warning: Unused introduction pattern: ? [unused-intro-pattern,tactics]
File "/home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Scalars.v", line 194, characters 4-51:
Warning: Unused introduction pattern: ? [unused-intro-pattern,tactics]
File "/home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Scalars.v", line 194, characters 4-51:
Warning: Unused introduction pattern: ? [unused-intro-pattern,tactics]
File "/home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Scalars.v", line 194, characters 4-51:
Warning: Unused introduction pattern: ? [unused-intro-pattern,tactics]

Some files also emit large blocks of code; perhaps you want to Redirect the output or else target those files specially?