## Stream: metaprogramming / tactics

### Topic: instances for meta defs

#### Yakov Pechersky (Oct 08 2020 at 19:29):

Does the following make sense?

import init.meta.interactive

meta instance {state : Type} : functor (interaction_monad state) :=
{ map := λ _ _, interaction_monad_fmap,
map_const := λ _ _ x, interaction_monad_fmap (λ _, x) }


or is that not useful, won't be accessible to the typeclass system?

#### Yakov Pechersky (Oct 08 2020 at 19:35):

I guess it could be something, since there is a meta instance of monad in interaction_monad.lean

#### Yakov Pechersky (Oct 08 2020 at 19:35):

But I don't understand why interaction_monad.result is a separate defn

#### Reid Barton (Oct 08 2020 at 20:12):

It already exists as a consequence of the monad instance

#### Reid Barton (Oct 08 2020 at 20:12):

Yakov Pechersky said:

But I don't understand why interaction_monad.result is a separate defn

As opposed to what?

#### Yakov Pechersky (Oct 08 2020 at 20:29):

I guess what I'm trying to understand is whether interactive_monad.result can itself be a monad or a functor. Or something similar. In lean#476, is there a way to simplify the following:

  (λ s, match found with
| (success r s') :=  (success r s)
| (exception f p s') := (exception f p s)
end),


#### Yakov Pechersky (Oct 08 2020 at 20:29):

Which as I understand, is just replacing the state in found

#### Eric Wieser (Oct 08 2020 at 21:14):

I wonder if something in https://github.com/leanprover-community/lean/blob/master/library/init/control/except.lean is what I'm after

#### Mario Carneiro (Oct 08 2020 at 22:01):

@Yakov Pechersky There are combinators that will do most of the variations on that kind of function, but you might want to do different things with the state, e.g. rolling it back in success case but not failure

#### Eric Wieser (Oct 08 2020 at 22:19):

Oh you might have found a bug in my PR then

#### Eric Wieser (Oct 08 2020 at 22:19):

I wasn't really thinking about state rollbacks

#### Eric Wieser (Oct 08 2020 at 22:20):

But maybe it doesn't matter because the caller does the rollback anyway?

What PR?

lean#476

#### Eric Wieser (Oct 09 2020 at 14:21):

It looks like the operations I'm looking for are

-- capture / pack the result of a tactic
meta def capture {α : Type*} (t : tactic α) : tactic (tactic_result α) :=
λ s, match t s with
| (success r s') := success (success r s') s'
| (exception f p s') := success (exception f p s') s'
end

-- release / rethrow / unpack a captured result
meta def release {α : Type*} (t : tactic_result α) : tactic α :=
match t with
| (success r s') := return r
| e := λ s, e
end


Do these exist already under other names? If not, are the names I propose sensible?

#### Reid Barton (Oct 09 2020 at 14:25):

capture is similar to try_core, but returns more information. I think returning the tactic_state is generally not desirable though

#### Eric Wieser (Oct 09 2020 at 14:25):

The sole purpose of capture is to put the result through release later

#### Reid Barton (Oct 09 2020 at 14:25):

In particular I'm skeptical about the | e := λ s, e case

#### Eric Wieser (Oct 09 2020 at 14:27):

Which is equivalent to | (exception f p s') := λ s, (exception f p s'), right? Presumably you're worried the second s' should be s?

#### Reid Barton (Oct 09 2020 at 14:37):

Eric Wieser said:

Which is equivalent to | (exception f p s') := λ s, (exception f p s'), right? Presumably you're worried the second s' should be s?

I'm definitely less worried if the second s' is s.

#### Reid Barton (Oct 09 2020 at 14:37):

Because then you can write it using normal tactic functions.

#### Eric Wieser (Oct 09 2020 at 14:38):

That would give an incorrect error message though. I want to see the tactic state at the point the error happened, not at the point that ext_simplify_core did its cleanup after that

#### Eric Wieser (Oct 09 2020 at 14:38):

(whatever that cleanup may be)

#### Eric Wieser (Oct 09 2020 at 14:38):

I don't believe the tactic state in exception is used for anything other than diagnostics

#### Eric Wieser (Oct 09 2020 at 14:38):

Trying to continue from an error state by extracting and using the s of exception would be foolish in any situation - if you recover from an error, you should resume from a known-good state (ie, the beginning of a try)

#### Reid Barton (Oct 09 2020 at 14:42):

Well this all hurts my head

#### Reid Barton (Oct 09 2020 at 14:42):

I think maybe only 80 lines will not be enough? :upside_down:

#### Reid Barton (Oct 09 2020 at 14:42):

Can you just use mutable variables somehow?

#### Reid Barton (Oct 09 2020 at 14:45):

I really think that whatever you are trying to do should be possible without this weird non-chronological control flow

#### Eric Wieser (Oct 09 2020 at 14:45):

This isn't non-chronological

#### Eric Wieser (Oct 09 2020 at 14:46):

This is just a rewind, which is exactly what try {} already does - the only difference is I'm rewinding to an error state, not to the pre-error state

#### Reid Barton (Oct 09 2020 at 14:46):

Isn't it? You're saving an intermediate state and using it later, after more things might have affected the state in the meantime

#### Eric Wieser (Oct 09 2020 at 14:46):

My claim is that nothing uses that state

#### Reid Barton (Oct 09 2020 at 14:46):

Yeah but try doesn't give you an object to use in totally uncontrolled ways

#### Reid Barton (Oct 09 2020 at 14:47):

So then you must not need it, right? :upside_down:

#### Eric Wieser (Oct 09 2020 at 14:47):

Sorry, my claim is that the only user of the third argument to exception is the debug window printout

#### Eric Wieser (Oct 09 2020 at 14:47):

And for that use case, the old state is the one that matters

#### Reid Barton (Oct 09 2020 at 14:48):

And you can't just capture the debug window output locally in a thunk or something?

#### Eric Wieser (Oct 09 2020 at 14:48):

Isn't that debug window output exactly tactic_state?

#### Eric Wieser (Oct 09 2020 at 14:48):

(I don't know the answer to this)

#### Reid Barton (Oct 09 2020 at 14:49):

but what you want to do doesn't seem impossible

#### Eric Wieser (Oct 09 2020 at 14:49):

What I want to do would be impossible in the IO monad

ok, I give up

#### Eric Wieser (Oct 09 2020 at 14:50):

If I have a print_with_commas some_monad that ignores errors in some_monad and keeps printing commas, there's nothing I can do to stop those commas being printed

#### Eric Wieser (Oct 09 2020 at 14:50):

But in the tactic monad, I can (and need to) rollback time to before the commas are printed. try {} is also not possible in the IO monad

#### Eric Wieser (Oct 09 2020 at 15:10):

Thanks for the feedback, anyway - I'll see if I can make the intent clearer

#### Reid Barton (Oct 09 2020 at 15:24):

I still think it would be better to fix the API of ext_simplify_core so that it doesn't swallow all exceptions--this might fix other bugs at the same time.

#### Eric Wieser (Oct 09 2020 at 15:25):

My main resistance to that is ext_simplify_core being written in C++

#### Eric Wieser (Oct 09 2020 at 15:26):

But yes, I suppose the signature of the pre and postcallbacks to ext_simplify_core could be changed from returning tactic (α × expr × option expr × bool) to returning tactic \$ option (α × expr × option expr × bool), where none in the new version means monadic failure means together

#### Eric Wieser (Oct 09 2020 at 15:29):

But that requires changing every single caller of ext_simplify_core, which is something I don't feel at all comfortable doing.

#### Eric Wieser (Oct 09 2020 at 16:07):

I've updated the PR code with some more comments, and the PR description to summarize the alternative I describe above.

#### Mario Carneiro (Oct 10 2020 at 01:09):

Eric Wieser said:

But that requires changing every single caller of ext_simplify_core, which is something I don't feel at all comfortable doing.

There aren't that many, because it's a very unwieldy API

#### Eric Wieser (Oct 10 2020 at 07:12):

There are a fair number of transitive callers that would change too

#### Eric Wieser (Oct 10 2020 at 07:16):

Would a suitable compromise be to:

• Define a wrapper, ext_simplify_core_strict, which does the monad tricks currently in the PR
• Change find and for to use this def instead
• Slowly convert other callers to use the new API over multiple PRs
• Change the C++ API to make ext_simplify_core_strict the default behavior, once all callers are changed

I don't want to have to perform a massive refactor to fix an annoying bug - I'd prefer to fix the bug first, and leave breadcrumbs for someone more competent to perform the refactor

#### Eric Wieser (Oct 13 2020 at 10:18):

(note that this was merged in the end, and @Gabriel Ebner pointed out that ext_simplify_core not only discards errors, but rolls back any changes to the tactic state)

Last updated: May 09 2021 at 23:10 UTC