Stream: Coq users

Topic: coqdep lax error handling


view this post on Zulip Stéphane Desarzens (Aug 09 2021 at 08:44):

When merge conflicts arise during git-rebase or git-merge, the conflict-markers often create syntax errors. Coqdep then won't generate a dependency file and to step through a file with conflicts, it is necessary to manually build its dependencies in the correct order. This is a lot of work on large projects.

Is there a way to call coqdep (from coq-makefile) so that it ignores files with syntax errors and generates a dependency file for all the other/non-problematic files? Maybe also leaving all files depending on erroneous files.

view this post on Zulip Ali Caglayan (Aug 09 2021 at 10:34):

Is this a problem with make? If coqdep is being called on each file seperately, you can probably pass make -k which will try to build as many tasks as possible not stopping at errors.

view this post on Zulip Gaëtan Gilbert (Aug 09 2021 at 10:57):

coq_makefile calls coqdep on all files at once
you can try make -k redir_if_ok='> "$@"' to ignore coqdep errors

view this post on Zulip Ali Caglayan (Aug 09 2021 at 11:01):

How does that work? Looks like magic to me :-)

view this post on Zulip Gaëtan Gilbert (Aug 09 2021 at 11:03):

it hacks the error handling in the generated makefile
for a more stable solution please report an issue on github


Last updated: Feb 08 2023 at 23:03 UTC