Caching within begin-end blocks

[dselsam]

As several of us discussed the other day, the following may become increasingly problematic as proofs get bigger and use more automation:

begin
  tac1, -- expensive
  tac2  -- calling tac2 causes tac1 to be run again
end

[leodemoura]

Here are more notes from our meeting:

• This is an issue when using Lean in an editor such as Emacs and VS Code, and we want to see the effect of our tactics (i.e., the resulting goal) after we type them.

• One possible solution is to create checkpoints between tactics for lemmas/theorems of the form

  lemma foo : T :=
  begin
  tac_1,
  tac_2,
  ...
  end

  This is not a complete solution since we may have begin ... end blocks nested in terms. @gebner pointed out we should only try to implement this solution after we refactor the parser.

[leodemoura]

Here is another possible solution:

• We add a tactical

  memoize (fingerprint : nat) (tac : tactic unit) : tactic unit

• This tactical would be introduced by the tactic_notation module. That is, tac_1 would become memoize H tac_1, where H is computed using the pre-term for tac_1 and the environment fingerprint.
• We add a cache to memoize tactic execution.
• memoize H_1 tac_1 would compute and fingerprint H_2 for the input tactic_state and check whether the cache contains an entry for H_1 and H_2. If it does, we reuse the result and skip tac_1. Otherwise, we execute tac_1 and cache the result.
• We ignore potential fingerprint collisions, and add a mechanism for disabling this mechanism.

[leodemoura]

Remark: the memoize based solution would also work for begin...end blocks nested in terms.

[gebner]

This is an issue when using Lean in an editor such as Emacs and VS Code, and we want to see the effect of our tactics (i.e., the resulting goal) after we type them.

Seeing the results should work just fine at the moment. The issue is the delay between typing and seeing the results.

@gebner pointed out we should only try to implement this solution after we refactor the parser.

This is mainly because I'd like to push the parser refactoring. :smile: My main concern is that we're beginning to encode a state machine into the parser/module_parser class.

At the moment the state machine already has quite a few states: before-imports/before-command/after-doc-string (probably missing a few cases). Not to mention all the extra state (sections/namespaces/etc.) stored in the environment.

Adding tactics as extra command-likes adds an additional in-lemma(tactic_state) state.

At this point I'm not sure if it wouldn't be easier to just store continuations, i.e. lambdas that continue parsing after the current position. I haven't put much thought into this though.

memoize

This would be nice for nested tactics block, I agree. Do you have an idea on how to handle metavariables and local constants for fingerprinting? Both use mk_fresh_name which changes between elaborations/parsing runs.

[leodemoura]

This would be nice for nested tactics block, I agree. Do you have an idea on how to handle metavariables and local constants for fingerprinting? Both use mk_fresh_name which changes between elaborations/parsing runs.

I am planning to ignore them in the figerprint computation.

[leodemoura]

@gebner I tried to work on this issue today because @Armael is starting to have performance problems similar to the one described by @dselsam in this issue. However, the trick describe in the previous comment does not really work (i.e., ignore the metavars and local ids computed using mk_fresh_name). Well, we can use the trick to retrieve the cached tactic_state S, but S is incompatible with the data stored in the elaborator object :( The elaborator contains references to locals and metavariables, but the cached S has completely different ids. So, to implement the memoization trick, I will have to fix the mk_fresh_name issue :(

[dselsam]

may become increasingly problematic

I thought I would mention that this is no longer a hypothetical concern for me. Even though I don't use any automation besides occasionally calling the simplifier to rewrite inside lambdas, most of the proofs in my current project are still too involved to work on interactively.

[leodemoura]

@dselsam Did you try to profile? Do you where the performance bottleneck is? Some performance bottlenecks are easy to fix.

The memoization trick I described above is a big change due to the issue I have described in my previous comment. So, another solution/workaround is to fix existing performance bottlenecks. We would not be addressing the issue described here, but we would be minimizing its effect.

[leodemoura]

The elaborator contains references to locals and metavariables, but the cached S has completely different ids. So, to implement the memoization trick, I will have to fix the mk_fresh_name issue :(

I tried to address this issue by implementing a procedure that would reset the mk_fresh_name counter and clear all thread local caches that would be affected by the reset. Unfortunately, this solution also has a problem. The internal fresh names are of the form <thread-id>.<id>, where <thread-id> is an unique name prefix we have for each thread, and <id> is computed using a thread local counter. Suppose we have

begin
  tac1, -- expensive
  tac2  -- calling tac2 causes tac1 to be run again
end

and we cached the tactic_state after executing tac1 on thread 1. The terms there contain internal names of the form <thread-1-id>.<id>. Now, suppose we try to execute the tactic block again, but this time we use thread 2. The internal names would be incompatible since we are expecting to have names of the form <thread-2-id>.<id>, but the cached tactic_state has names of the form <thread-1-id>.<id>.

We can address the issue above by writing a function that traverses the cached tactic_state and replaces the prefix <thread-old-id> with <thread-new-id> in the internal names. We have to reconstruct the metavar_context and all associated local_contexts. BTW, the object tactic_state contain user defined data, but they are not cached (so this part is fine). However, we would have to expose the translation procedure in the tactic framework, since users may create their own tactic monads on top of tactic_state. We should ignore this translation procedure for smt_tactic. It would be too much work to write the translation function above for smt_state.

@kha I think this translation function would be too hacky. Then, I considered another possibility. We do not include the prefix <thread-id> in names returned by mk_fresh_name. The motivation is that in most cases we use single thread to elaborate a declaration. I said "in most cases" because we have the task.delay primitive that allows us to use more than one thread. In the future, we may also add primitives proof procedures that use more than one thread. BTW, I just realized another problem, since more than one thread may be used to elaborate a term, in principle, we may have fresh names with more than one <thread-id> prefix. Now, consider the following bad scenario. We have a cached tactic_state object containing the names <thread-1-id>.1 and <thread-2-id>.1, and we are trying to reuse this object at thread 3. If we map both names to <thread-3-id>.1 we would have an invalid tactic_state object.

I see only two solutions at this point: 1) Close this issue, and tell users to break their proofs into smaller proofs if they experience this problem. 2) Remove mk_fresh_name, and add back the name_generator objects we had in Lean 2. This would be a major and painful change. https://github.com/leanprover/lean/blob/CADE25/src/util/name_generator.h

What do you think?