make is very noisy, even when there's nothing to be done

[JasonGross]

See also mit-plv/coqutil#15; it's the same problem in the submakefiles here

[JasonGross]

Though also I don't want to see

coqc -q -Q src/bedrock2 bedrock2 -Q ../deps/coqutil/src/coqutil coqutil  special/BytedumpTest.v > special/BytedumpTest.out.tmp0
head -c $(($(wc -c < special/BytedumpTest.out.tmp0 | xargs) - 1)) special/BytedumpTest.out.tmp0 > special/BytedumpTest.out.tmp
rm special/BytedumpTest.out.tmp0
hexdump < /dev/null && \
        hexdump -C special/BytedumpTest.golden.bin > special/BytedumpTest.golden.hex && \
        hexdump -C special/BytedumpTest.out.tmp > special/BytedumpTest.out.hex && \
        diff -u special/BytedumpTest.golden.hex special/BytedumpTest.out.hex && \
        rm special/BytedumpTest.golden.hex special/BytedumpTest.out.hex || true
diff -u special/BytedumpTest.golden.bin special/BytedumpTest.out.tmp
mv special/BytedumpTest.out.tmp special/BytedumpTest.out

every single time I build

[samuelgruetter]

@andres-erbsen could you please take care of the BytedumpTest.out related stuff? I don't understand it well and why it's so many commands...

[JasonGross]

Note that you can just hide them all except when VERBOSE=1, and simply print out testing bytedump or something

[JasonGross]

Note that there is also the issue of

coq_makefile -f _CoqProject INSTALLDEFAULTROOT = bedrock2  /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Scalars.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/NotationsCustomEntry.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/MetricLogging.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/BasicC64Semantics.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Syntax.v /home/$gross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/BasicCSyntax.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/FE310CSemantics$v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Lift1Prop.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/ZNamesSyn$ax.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/TailRecursion.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Tr$cePredicate.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/string2ident.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bed$ock2/Map/SeparationLogic.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Map/Separation.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/b$drock2/src/bedrock2/Map/FDSepLog.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Byte.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bed$ock2/src/bedrock2/Markers.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Memory.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2$src/bedrock2/Examples/ArrayLoadStore.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Examples/ARPResponder.v /home/jgross/Documents/repos/fia$-crypto/bedrock2/bedrock2/src/bedrock2/Examples/lightbulb_spec.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Examples/MultipleReturnValues.$ /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Examples/Trace.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Examp$es/bsearch.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Examples/SPI.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedr$ck2/Examples/chacha20.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Examples/StructAccess.v /home/jgross/Documents/repos/fiat-crypto/bedroc$2/bedrock2/src/bedrock2/Examples/LAN9250.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Examples/FE310CompilerDemo.v /home/jgross/Documents/$epos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Examples/lightbulb.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Examples/Demos.v /home/jgr$ss/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Examples/ipow.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Examples/ARPRespo$derProofs.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Examples/swap.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedr$ck2/Semantics.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Array.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2$ProgramLogic.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/AbsintWordToZ.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/b$drock2/StringNamesSyntax.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/ToCString.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedroc$2/src/bedrock2/StructNotations.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/ptsto_bytes.v /home/jgross/Documents/repos/fiat-crypto/bedrock$/bedrock2/src/bedrock2/ReversedListNotations.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/WeakestPrecondition.v /home/jgross/Documents/rep$s/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Hexdump.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/div10.v /home/jgross/Documents/repos/fia$
-crypto/bedrock2/bedrock2/src/bedrock2/Variables.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/BasicC32Semantics.v /home/jgross/Documents/r$
pos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Structs.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Bytedump.v /home/jgross/Documents/repo$
/fiat-crypto/bedrock2/bedrock2/src/bedrock2/NotationsInConstr.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/Notations.v /home/jgross/Docume$
ts/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/WeakestPreconditionProperties.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src/bedrock2/ChangeSeman$
icsParams.v -o Makefile.coq.all

which could use a similar fix as in mit-plv/coqutil@079ca2b