Stéphane Desarzens (Aug 09 2021 at 08:44): 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.
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.
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
Ali Caglayan (Aug 09 2021 at 11:01):How does that work? Looks like magic to me :-)
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: Apr 20 2024 at 13:01 UTC