with_local_environment

Stream: general

[Reid Barton]

Is there a combinator like with_local_goals which lets me scope modifications to the environment? (In my case, I am interested in setting attributes for the scope of a single tactic.)

[Reid Barton]

I found a relatively painless way to reimplement my continuity tactic: use apply_rules, but locally make continuous irreducible, to work around the apply bug.
https://github.com/rwbarton/lean-homotopy-theory/commit/ce83a76df05505f53101d420cc08b0597ceea552

[Patrick Massot]

Do we know if Gabriel has a slot in next week's release of Lean to fix the apply bug?

[Patrick Massot]

(Gabriel, you've been very dangerously raising our expectations recently)

[Reid Barton]

I don't believe it is fixable

[Reid Barton]

But Gabriel is welcome to prove me wrong

[Reid Barton]

But on the subject of this topic, my implementation is a bit crude because (1) in principle, continuous might not be semireducible in the first place, in which case restoring it is wrong; (2) I'm not sure what happens if the inner tactic (tidy cfg') fails with an exception which is caught somewhere outside--can I end up in a state where continuous is irreducible?

[Jannis Limperg]

I guess you could do the bracket thing:

• Check if continuous is semireducible.
• Set continuous to semireducible.
• Try to run the inner tactic; capture its result or the thrown exception. (The combinator for this might not exist yet, but should be implementable.)
• Restore the previous 'semireducibility' of continuous.
• Return the result of the inner tactic or rethrow the exception.

[Gabriel Ebner]

I'm not sure what the apply bug is, is this the one fixed in apply'?

[Reid Barton]

The bug where apply guesses wrong how many _s to insert, which I described here. apply' fixes it in a rather heavy-handed way, which I'm not sure is suitable for general use.

[Reid Barton]

Jannis Limperg said:

• Try to run the inner tactic; capture its result or the thrown exception. (The combinator for this might not exist yet, but should be implementable.)

Looks like there is interaction_monad.bracket for this.

[Reid Barton]

and also finally--do we really need both?

[Jannis Limperg]

finally seems to be a special case of bracket, so the implementation could be simplified. It's used only once in mathlib, so 'need' is a strong word. However, finally seems like the more fundamental combinator; bracket x y z = x >> finally y z.