Zulip Chat Archive

Stream: general

Topic: with_local_environment


view this post on Zulip Reid Barton (May 21 2020 at 14:09):

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.)

view this post on Zulip Reid Barton (May 21 2020 at 15:14):

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

view this post on Zulip Patrick Massot (May 21 2020 at 15:15):

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

view this post on Zulip Patrick Massot (May 21 2020 at 15:16):

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

view this post on Zulip Reid Barton (May 21 2020 at 15:17):

I don't believe it is fixable

view this post on Zulip Reid Barton (May 21 2020 at 15:17):

But Gabriel is welcome to prove me wrong

view this post on Zulip Reid Barton (May 21 2020 at 15:25):

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?

view this post on Zulip Jannis Limperg (May 21 2020 at 15:30):

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.

view this post on Zulip Gabriel Ebner (May 21 2020 at 16:08):

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

view this post on Zulip Reid Barton (May 21 2020 at 17:44):

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.

view this post on Zulip Reid Barton (May 21 2020 at 17:49):

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.

view this post on Zulip Reid Barton (May 25 2020 at 20:07):

and also finally--do we really need both?

view this post on Zulip Jannis Limperg (May 26 2020 at 10:26):

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.


Last updated: May 14 2021 at 22:15 UTC