Can we distinguish `apply?` from `apply`

[TentativeConvert]

As reported here, the tactic apply? can unintentionally solve levels of Robo that are supposed to be solved by applying apply manually. I’ve tried disabling apply? manually, e.g. with:

NewHiddenTactic «apply?»
DisabledTactic tauto «apply?»

But that does not appear to have any effect.

[joneugster]

I believe currently we trim any ? or ! from the tactic name, I think the reason behind this was to allow simp?. We should probably change that 👍

[TentativeConvert]

I'm not sure this is fixed. Running Robo with lean4game tag v4.22.0 locally, I can still use apply? (even with rules set to strict). I don't think the apply? tactic (with ?) is introduced anywhere in the game. I've also tried disabling it manually with in Implis/L05 with

DisabledTactic tauto «apply?»

and I can still use it in the game.

[joneugster]

I've tried it out now with v4.23.0 and it seems to me that this issue is now a complete duplicate of https://github.com/leanprover-community/lean4game/issues/302

i.e. the engine does distinguish apply from apply? but the info messages from dissallowed tactics are still displayed.

(please reopen once more if I'm mistaken)