search

mit-plv / coqutil

Coq library for tactics, basic definitions, sets, maps
MIT License
41 stars 24 forks source link

make is very noisy even when there is nothing to be done #15

Closed JasonGross closed 5 years ago

JasonGross commented 5 years ago

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 5 years ago

Are you sure you're using the latest version? I think I fixed that yesterday in https://github.com/mit-plv/coqutil/commit/079ca2badc7aa4feacc27599cadda702d0c4c888

JasonGross commented 5 years ago

I guess bedrock2 and/or fiat-crypto are using an outdated version