Stream: Coq devs & plugin devs

Topic: DELETE_ON_ERROR flipped logic


view this post on Zulip Paolo Giarrusso (Mar 31 2022 at 14:25):

I'm trying to make sense of https://github.com/coq/coq/pull/14238; according to the changelog, it enables . DELETE_ON_ERROR by default

view this post on Zulip Paolo Giarrusso (Mar 31 2022 at 14:26):

but the logic seems backward, even if the "double negation" in the comment are confusing:

# set KEEP_ERROR to prevent make from deleting files produced by failing rules.
# For instance if coqc creates a .vo but then fails to native compile,
# the .vo will be deleted unless KEEP_ERROR is nonempty.
# May confuse make so use only for debugging.
KEEP_ERROR?=
ifneq (,$(KEEP_ERROR))
.DELETE_ON_ERROR:
endif

view this post on Zulip Paolo Giarrusso (Mar 31 2022 at 14:28):

after double-negation elimination, this reads to me as:

# set KEEP_ERROR to tell make to keep files produced by failing rules.
[...]
set KEEP_ERROR to a default value
if KEEP_ERROR is _not_ default # Backwards!
<delete outputs of failing rules>
endif

view this post on Zulip Paolo Giarrusso (Mar 31 2022 at 14:46):

I also double-checked if sth funky was going on, but I think not:

$ cat > Make.test << 'EOF'
KEEP_ERROR?=
ifneq (,$(KEEP_ERROR))
$(info "We should set DELETE_ON_ERROR")
.DELETE_ON_ERROR:
else
$(warning "Bug: By default, we do NOT set DELETE_ON_ERROR")
endif
all:
EOF
$ make -f Make.test
Make.test:6: "Bug: By default, we do NOT set DELETE_ON_ERROR"
make: Nothing to be done for 'all'.

view this post on Zulip Paolo Giarrusso (Mar 31 2022 at 14:48):

Submitted https://github.com/coq/coq/pull/15880.


Last updated: Feb 05 2023 at 20:03 UTC