Run make to update template-coq/gen-src/cRelationClasses.mli.orig

[JasonGross]

Is this change expected? Is this file supposed to be checked in? What's going on here?

[mattam82]

It looks like the extraction changed somehow? The .orig file doesn't need to be checked in, you're right.

[yforster]

Can we let the patch command fail if the patch is not applicable? If not, it might make sense to keep the orig file and fail if it is not correct anymore

I hunted a problem for about an hour the other day where the issue was that extraction changed and the patch silently failed, resulting in a compilation error that I couldn't make sense of

[JasonGross]

Does changing
https://github.com/MetaCoq/metacoq/blob/ca64d7236c22a438496d0360385f62216ef0a2ca/template-coq/update_plugin.sh#L22-L23
with

-    patch -N -p0 < extraction.patch
-    patch -N -p0 < specFloat.patch
+    patch -N -p0 < extraction.patch || exit $?
+    patch -N -p0 < specFloat.patch || exit $?

work?

[yforster]

Is that different to || exit? But the idea seems to be the right one to enforce a failure on a failing patch

[JasonGross]

Is that different to || exit? But the idea seems to be the right one to enforce a failure on a failing patch

I think it's the same

[mattam82]

I guess we can just remove the .orig file now

[mattam82]

Is this still relevant?

[JasonGross]

The .orig file still exists, but it seems to no longer be the case that make changes it, so, idk, maybe not?