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.
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.
coq_makefile calls coqdep on all files at once
you can try
make -k redir_if_ok='> "$@"' to ignore coqdep errors
How does that work? Looks like magic to me :-)
it hacks the error handling in the generated makefile
for a more stable solution please report an issue on github
Last updated: Sep 23 2023 at 07:01 UTC