mkVSU external function check does not give useful error message

[andrew-appel]

In the mkComponent tactic, the following line does not give a useful error when it fails:

apply (@forallb_isSomeGfunExternal_e _); reflexivity.

The error message should be something like, "Each of the functions in the E component of the VSU should be a CompCert 'External' function, but at least one is not..." or even better, say which ones are not.

Instead, the error message is,

Unable to unify "true" with
 "forallb
    (fun i : positive =>
     isSomeGfunExternal (Maps.PTree.get i (QP.prog_defs p)))
    (map fst your_VSU_E_list)".

[andrew-appel]

Also, the line

intros; simpl; split; trivial; try (solve [ lookup_tac ]).

does not give a useful error message if the internal_specs contains an identifier not present in the IntIDs of the compilation unit.

[andrew-appel]

Also, when the second argument internal_specs of mkVSU does not match the Gprog of one a body_ lemma that's an argument to solve_SF_internal , then Coq just freezes for a long time rather than having solve_SF_internal give a useful error message.

[andrew-appel]

Also, when the argument to solve_SF_internal is a nonexistent lemma, the error message is misleading:

solve_SF_internal did not entirely succeed, because xkldsklfj does not exactly match this subgoal