CompCert icon indicating copy to clipboard operation
CompCert copied to clipboard

Published 20 hours ago • verified publisher icon AbsInt

improved auto goal selection

Open mrhaandi opened this issue 2 years ago • 2 comments

Improves robustness in case of stronger (e)auto (see coq/#16293).

mrhaandi avatar Jul 18 '22 12:07 mrhaandi

@xavierleroy I did check that this PR compiles both before and after https://github.com/coq/coq/pull/16293. The main reason for the proposed changes is that fixing bugs in auto may allow it to solve more goals. Non-monotone use of automation such as tac1; auto. tac2. may, therefore, break.

mrhaandi avatar Jul 22 '22 16:07 mrhaandi

@mrhaandi : thanks for the PR and the pointers. The discussion of the "antipattern" is interesting. I'd like to seize the opportunity to clean up some of the scripts touched by this PR, so I'll leave it open for a few weeks. But please go ahead with making (e)auto stronger in Coq, knowing that CompCert will be adapted accordingly.

xavierleroy avatar Jul 25 '22 08:07 xavierleroy

@xavierleroy coq/coq#16293 is basically pending on this overlay. It's not strictly urgent but there is always the risk of other devs introducing incompabilities with that PR, so I believe it'd be better to merge this PR quickly.

ppedrot avatar Sep 05 '22 08:09 ppedrot

Generally speaking I prefer when Coq is changed and then CompCert is adjusted to the change, rather than doing things in the opposite order. But if this is really blocking for the Coq change, I'll merge this PR and make a mental note to check again when the Coq changes enter alpha or beta stage.

xavierleroy avatar Sep 08 '22 13:09 xavierleroy

Isn't it better to write backwards compatible patches, though? That way no CI is ever broken.

ppedrot avatar Sep 09 '22 08:09 ppedrot