Option for deactivating autoparams

Stream: mathlib4

[Adam Topaz]

Do we have some option that deactivates autoParams? I'm quite sure the answer is "no", so maybe this is a feature request. Can this be done without changing core?

The thing is, I'm running into some annoying issues which I'm quite sure are due to autoparams in parts of the category theory library. There are often times where I have to restart to server constantly when working on a file. I would like to be able to just deactivate autoparams (perhaps in a single decl with set_option ... in ...) to make the workflow smoother.

[Mario Carneiro]

you could override the problematic tactic

[Adam Topaz]

Ah good idea!

[Kevin Buzzard]

Is this issue fixed with lean4#2238 ?

[Scott Morrison]

Hmm, master on lean4 has been broken for a few days, so we are not getting nightlies.