Should minimization failures be better signposted?

[JasonGross]

We got feedback (from @herbelin ?)

• Could it be indicated in the github comment posting the minimizations whether the minimization relies on external files, and, if easy to know, on which?

We already include this information, for example this comment says:

Partially Minimized Coq File (could not inline Equations.Prop.DepElim)

and the fifth line of the comment header in the tfile says:

Modules that could not be inlined: Equations.Prop.DepElim

By contrast, complete minimization says:

Minimized Coq File (consider adding this file to the test-suite)

Should this information be flagged more loudly somehow?

[Zimmi48]

Should this information be flagged more loudly somehow?

The bot could for instance say in one case: "I managed to produce a reduced and fully standalone test case."
And in the other: "I didn't manage to produce a fully standalone test case. Here are the modules that I did not manage to inline: ... Here is the partially minimized file: ..."

[herbelin]

As you like. From my point of view, I think it is ok as it is currently (now that I know how to interpret the information).