Make interpretation of references with maximal implicit arguments in Ltac functions the same in strict and non-strict mode #17084
Conversation
|
@coqbot run full ci |
|
The job library:ci-fiat_crypto_legacy has failed in allow failure mode |
|
🔴 CI failures at commit 3c99cec without any failure in the test-suite ✔️ Corresponding jobs for the base commit 64e93b1 succeeded ❔ Ask me to try to extract minimal test cases that can be added to the test-suite 🏃
|
|
For the record, here is a reduced form of the cause of failure in iris_example (whose primary cause is in autosubst): Ltac is_succ s :=
match s with
| S ?n => constr:(Some n)
| 0 => None
end.
Goal True.
match is_succ 0 with
| Some _ => idtac "some"
| _ => idtac "none"
end.In master, I would say that the PR behavior is what was implicitly expected, so that both branches of |
|
The failure in vst and fiat-crypto are of the following form: Ltac apply' f := apply f.
Ltac g := apply' eq_refl.
Goal 0=0.
g. (* fails with the PR due to the implicit argument of eq_refl being non inferable *)I see two possible fixes at the level of the script:
and two at the level of Coq, therefore needing no change in the scripts:
Note: For the record, verdi-raft now includes a backwards compatible patch. |
|
The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed. |
This was the case in non-strict mode (via interpretation at runtime), but, in strict mode, it was instead the reference without its maximal implicit arguments. The main impact is on "class_apply" which we reformulate as a tactic notation to ensure that its argument is always interpreted as a term.
3c99cec to
b67680d
Compare
|
@coqbot run full ci |
|
The job library:ci-fiat_crypto_legacy has failed in allow failure mode |
|
🔴 CI failures at commit b67680d without any failure in the test-suite ✔️ Corresponding jobs for the base commit fc4ff97 succeeded ❔ Ask me to try to extract minimal test cases that can be added to the test-suite 🏃
|
|
So what do we do with this? Write overlays and merge? |
|
I support this PR, so indeed in my opinion writing the overlays is the way to go. |
… impargs. This was the case in non-strict mode (via interpretation at runtime), but, in strict mode, it was instead the reference without its maximal implicit arguments. Also deprecate the old strict mode internalization. For compat with enabling the option, the main impact is on "class_apply" which we reformulate as a tactic notation to ensure that its argument is always interpreted as a term. Replaces rocq-prover#17084 in a more backward compatible way. Co-authored-by: Hugo Herbelin <herbelin@users.noreply.github.com>
… impargs. This was the case in non-strict mode (via interpretation at runtime), but, in strict mode, it was instead the reference without its maximal implicit arguments. Also deprecate the old strict mode internalization. For compat with enabling the option, the main impact is on "class_apply" which we reformulate as a tactic notation to ensure that its argument is always interpreted as a term. Replaces rocq-prover#17084 in a more backward compatible way. Co-authored-by: Hugo Herbelin <herbelin@users.noreply.github.com>
|
Replaced by #20682 which provides a deprecation phase |
… impargs. This was the case in non-strict mode (via interpretation at runtime), but, in strict mode, it was instead the reference without its maximal implicit arguments. Also deprecate the old strict mode internalization. For compat with enabling the option, the main impact is on "class_apply" which we reformulate as a tactic notation to ensure that its argument is always interpreted as a term. Replaces rocq-prover#17084 in a more backward compatible way. Co-authored-by: Hugo Herbelin <herbelin@users.noreply.github.com>
… impargs. This was the case in non-strict mode (via interpretation at runtime), but, in strict mode, it was instead the reference without its maximal implicit arguments. Also deprecate the old strict mode internalization. For compat with enabling the option, the main impact is on "class_apply" which we reformulate as a tactic notation to ensure that its argument is always interpreted as a term. Replaces rocq-prover#17084 in a more backward compatible way. Co-authored-by: Hugo Herbelin <herbelin@users.noreply.github.com>
As shown in #16935, the interpretation of references in Ltac functions happens to be different in strict mode (i.e., in practice, non interactively) and in non-strict mode (i.e., in practice, interactively) regarding the insertion or not of maximal implicit arguments.
This comment at #16935 suggested to align the strict mode on the non-strict mode and this is what the PR does.
In particular, this ensures than in a configuration such as:
where
gevaluates an Ltac function applied to a reference in strict mode and this reference has inferable maximal implicit arguments, the implicit arguments are indeed inserted, as iff ahad been given directly.I did not find other cases where the change of semantics is observable (i.e. the maximal implicit arguments need to be solvable by type class inference, otherwise it fails with an unresolved implicit arguments anyway). In the stdlib, the only occurrence of such pattern is
class_apply(which plays the role offabove) and the compatibility can be preserved by turningclass_applyinto a tactic definition.