make is very noisy even when there is nothing to be done
JasonGross opened this issue · 2 comments
JasonGross commented
I see
coq_makefile -f _CoqProject INSTALLDEFAULTROOT = coqutil /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Macros/symmetry.v /home/jgross/Docu
ments/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Macros/unique.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Macros/subst.v /hom
e/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Word/Interface.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Word/
LittleEndian.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Word/Properties.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqut
il/src/coqutil/Word/Naive.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Map/Interface.v /home/jgross/Documents/repos/fiat-crypto/bedrock2
/deps/coqutil/src/coqutil/Map/Solver.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Map/SlowGoals.v /home/jgross/Documents/repos/fiat-cryp
to/bedrock2/deps/coqutil/src/coqutil/Map/Z_keyed_SortedListMap.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Map/SortedList.v /home/jgros
s/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Map/Funext.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Map/SortedListWo
rd.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Map/SortedListString.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/sr
c/coqutil/Map/TestLemmas.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Map/Properties.v /home/jgross/Documents/repos/fiat-crypto/bedrock2
/deps/coqutil/src/coqutil/Map/Empty_set_keyed_map.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Map/SortedListString_test.v /home/jgross/
Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Map/TestGoals.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Z/PushPullMod.v
/home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Z/ZLib.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Z/bitbla
st.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Z/div_to_equations.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/
coqutil/Z/HexNotation.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Z/Lia.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coquti
l/src/coqutil/Z/div_mod_to_equations.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Z/BitOps.v /home/jgross/Documents/repos/fiat-crypto/be
drock2/deps/coqutil/src/coqutil/Tactics/rdelta.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Tactics/syntactic_unify.v /home/jgross/Docum
ents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Tactics/letexists.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Tactics/autoforw
ard.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Tactics/Tactics.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/co
qutil/Tactics/destr.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Tactics/eabstract.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/d
eps/coqutil/src/coqutil/Tactics/simpl_rewrite.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/sanity.v /home/jgross/Documents/repos/fiat-cr
ypto/bedrock2/deps/coqutil/src/coqutil/dlet.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Decidable.v /home/jgross/Documents/repos/fiat-c
rypto/bedrock2/deps/coqutil/src/coqutil/Datatypes/PropSet.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Datatypes/PrimitivePair.v /home/j
gross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Datatypes/HList.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Datatyp
es/String.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Datatypes/Prod.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/s
rc/coqutil/Datatypes/List.v /home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src/coqutil/Datatypes/Option.v -o Makefile.coq.all
every time I run make, and it's a bit unpleasant. Please suppress the output, at least whenever VERBOSE
is empty.
(You can copy this snipped to allow conditional showing/hiding:
VERBOSE?=
SHOW := $(if $(VERBOSE),@true "",@echo "")
HIDE := $(if $(VERBOSE),,@)
and then do
foo:
$(SHOW)short description
$(HIDE)verbose actual command
samuelgruetter commented
Are you sure you're using the latest version? I think I fixed that yesterday in 079ca2b
JasonGross commented
I guess bedrock2 and/or fiat-crypto are using an outdated version