Incrementality Call for Testing

Stream: lean4

[Sebastian Ullrich]

As announced in the community meeting today, lean4#3940 "incremental elaboration of definition headers, bodies, and tactics" is nearing merge and inclusion in Lean 4.9.0. As this is a major change to the elaboration infrastructure, preliminary testing to smooth out landing this feature would be greatly appreciated!

Instructions: Please first read the PR description of lean4#3940 to understand what should and should not yet work at this point. The testing toolchain Kha/lean4:incr-tactic-v2 is compatible with Lean 4.8.0-rc1, so you should be able to use it as your lean-toolchain in any project on that version without further changes to your code (unless you depend on very specific elaboration API details). For Mathlib in particular, there is a branch incr-tactic-fixes-toolchain based on Tuesday's master that builds and comes with a cache. So you could e.g. transfer or start some work there and then cherry-pick it back onto master before pushing.

What to test: Obviously any regression in behavior is noteworthy. Other than that, the goal is that writing tactic proofs should be more efficient. If you feel Lean jumps back up after a change more than you think it should, that is also valuable information. More combinators such as tactic have will likely be added to the supported list in lean4#3940 later but the immediate goal is to support the combinators that people spend ~90% of the time in. A more general solution that supports all combinators out of the box may appear at some later date.

On an operational note, I am on vacation next week but hopefully nothing is so fundamentally broken that testing cannot commence without me :) .

[Patrick Massot]

Thanks a lot Sebastian!

[Patrick Massot]

Is it expected that different fields of a structure do not appear to be incremental?

[Sebastian Ullrich]

Using where?

[Patrick Massot]

Specifically I’m looking at https://github.com/leanprover-community/mathlib4/blob/incr-tactic-fixes-toolchain/Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean#L238 which is an awfully slow declaration. Modifying the last line of the last field clearly still takes forever.

[Patrick Massot]

Yes, using where.

[Patrick Massot]

By the way, if you want to experiment with profiling tools, this declaration is a great exemple of things going wrong.

[Sebastian Ullrich]

I see how incrementality would be useful here. At the same time, structure instance notation is already a very complex elaborator that I'm wary of further touching. I'll have to think about that.

[Sebastian Ullrich]

For example, unlike induction cases, structure instance fields are not/cannot necessarily be elaborated in order, so changing a field may affect fields above it. Which doesn't make it impossible to implement, just hard.

[Patrick Massot]

I had no idea changing a field can influence a previous field. When does that happen?

[Sebastian Ullrich]

With dependent types. Which usually are not the ones you would fill with tactics, no

[Henrik Böving]

Patrick Massot said:

I had no idea changing a field can influence a previous field. When does that happen?

say:

structure Foo where
  n : Nat
  xs : Array Nat
  h : n < xs.size
  foo : <some statement involving xs[i]'h>

if h is changed you have to take a look at foo again

[Patrick Massot]

Henrik, this is not affecting a previous field, right?

[Sebastian Ullrich]

You may specify these fields in any order when you construct a Foo. I think.

[Patrick Massot]

I never realized that!

[Patrick Massot]

I would totally be in favor of disallowing this if it makes anything easier to implement. I think very few users would notice any difference, because I guess very few people rely on this feature.

[Henrik Böving]

but that means that if i use the { x := , y :=, ...} notation I have to think about the order of fields, that sounds rather annoying

[Sebastian Ullrich]

To give a bit more context, according to the all-Mathlib profile I posted some time ago, about 8% + 2% of total time is spent in tactics in def/instance, so making them work in more than := by ... wasn't a top priority

[Patrick Massot]

I don’t say it should a top priority, I’m simply testing stuff as was asked, and reported the first thing that I saw that didn’t seem to work.

[Patrick Massot]

Henrik I don’t have this ordering issue because I use code actions to build the skeleton.

[Henrik Böving]

We have a code action for that? Or is that some batteries/mathlib thing

[Michael Rothgang]

Sebastian Ullrich said:

With dependent types. Which usually are not the ones you would fill with tactics, no

Asking a naive question: Lean cannot tell quickly if these are involved, right? (If one could, this seems like a natural potential fast path to add. Obviously, you will know much better if this is worthwhile architecturally.)

[Eric Wieser]

I think the field elaboration order becomes even more complicated when you consider default values, which can be derived from later fields

[Utensil Song]

e.g. if incremental elab is brought into a structure with default fields, it might affect fixes like lean4#3152 .

[Kevin Buzzard]

Patrick Massot said:

Specifically I’m looking at https://github.com/leanprover-community/mathlib4/blob/incr-tactic-fixes-toolchain/Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean#L238 which is an awfully slow declaration. Modifying the last line of the last field clearly still takes forever.

One issue with FiberwiseLinear (at least on that branch) is

import Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear

-- set_option trace.Meta.Tactic.simp true

noncomputable section

open Set TopologicalSpace

open scoped Manifold Topology

variable {𝕜 B F : Type*} [TopologicalSpace B]
variable [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F]

namespace FiberwiseLinear

variable {φ φ' : B → F ≃L[𝕜] F} {U U' : Set B}

set_option trace.profiler true
def smoothFiberwiseLinear' : StructureGroupoid (B × F) where
  members :=
    ⋃ (φ : B → F ≃L[𝕜] F) (U : Set B) (hU : IsOpen U)
      (hφ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => φ x : B → F →L[𝕜] F) U)
      (h2φ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => (φ x).symm : B → F →L[𝕜] F) U),
        {e | e.EqOnSource (FiberwiseLinear.partialHomeomorph φ hU hφ.continuousOn h2φ.continuousOn)}
  trans' := by
    simp only [mem_iUnion] -- this line is 22 seconds on my machine!
    sorry

I'm very surprised to see a simp only take so long, but I don't really understand the traces.

[Henrik Böving]

The trace says "I am solving about 500 defeq problems that are all fast on their own but 500 is just a bit much" I think

[Sébastien Gouëzel]

IB is not defined here, are you missing a variable line?

[Kevin Buzzard]

The code works for me on that branch. Let me try and get it working on master.

[Sébastien Gouëzel]

On master, I need to add the line

variable {EB : Type*} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type*}
  [TopologicalSpace HB] [ChartedSpace HB B] {IB : ModelWithCorners 𝕜 EB HB}

Otherwise, IB is not defined so it doesn't really make sense.

[Kevin Buzzard]

import Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear

-- set_option trace.Meta.Tactic.simp true

noncomputable section

open Set TopologicalSpace

open scoped Manifold Topology

variable {𝕜 B F : Type} [TopologicalSpace B]
variable [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F]

namespace FiberwiseLinear

variable {φ φ' : B → F ≃L[𝕜] F} {U U' : Set B}

variable {EB : Type*} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type*}
  [TopologicalSpace HB] [ChartedSpace HB B] {IB : ModelWithCorners 𝕜 EB HB}

set_option trace.profiler true
def smoothFiberwiseLinear' : StructureGroupoid (B × F) where
  members :=
    ⋃ (φ : B → F ≃L[𝕜] F) (U : Set B) (hU : IsOpen U)
      (hφ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => φ x : B → F →L[𝕜] F) U)
      (h2φ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => (φ x).symm : B → F →L[𝕜] F) U),
        {e | e.EqOnSource (FiberwiseLinear.partialHomeomorph φ hU hφ.continuousOn h2φ.continuousOn)}
  trans' := by
    simp only [mem_iUnion] -- this line is only 3 seconds on master
    sorry
  symm' := sorry
  id_mem' := sorry
  locality' := sorry
  mem_of_eqOnSource' := sorry

[Kevin Buzzard]

Yeah there's something weird going on here but it's about the variables, I think my example is bad.

[Sébastien Gouëzel]

With the right variable line, I get roughly the same time on master and on the branch for your snippet.

[Kevin Buzzard]

(and it's more like 3 seconds than 20 seconds! But still 3 seconds is a long time...)

[Richard Copley]

Something seems to go wrong with LSP error highlighting with the leanprover/lean4-pr-releases:pr-release-3940 toolchain in a few cases.
In this example, "this is not real lean" in the last line does not get a red wavy underline. (It does with leanprover/lean4:v4.8.0-rc1.)

import Init

def xxx (n : Nat) (h : 0 < n) : (k : Nat) ×' (0 ≤ k ∧ k < n) :=
  if hzero : n = 0 then (Nat.not_succ_le_zero 0 (hzero ▸ h)).elim
  else if h₁ : n < 2 then
    ⟨0, by exact ⟨Nat.zero_le 0, h⟩⟩
  else ⟨1, this is not real lean⟩

#print axioms xxx -- 'xxx' depends on axioms: [sorryAx]

[Sebastian Ullrich]

Thanks, this looks similar to the issue Kevin found. I can reproduce.

[Sebastian Ullrich]

There is a new toolchain Kha/lean4:incr-tactic-v2 that should fix these missing errors. Pull the new commit on the Mathlib branch to get it.

[Bolton Bailey]

I got the new Kha/lean4:incr-tactic-v2 toolchain working for my project with the very long theorem compile times. You can see me using it here. The orange bar steps down through the tactics one at a time, but that seems to be the only part that works - is it supposed to be the case that even a single call to something like suffices makes it impossible for the orange bar to restart halfway through a proof?

[Bolton Bailey]

After massaging this, I don' t think that was the problem. Here is a zip file of a shorter video I recorded - it seems like the orange bar steps up too far for lemma but not for example (not sure what would cause that).
2024-05-12-06-29-23.mkv.zip

[Richard Copley]

Sebastian Ullrich said:

There is a new toolchain Kha/lean4:incr-tactic-v2 that should fix these missing errors. Pull the new commit on the Mathlib branch to get it.

Looks good, thanks.

[Tobias Grosser]

Hi @Sebastian Ullrich, I just played with this incremental tactics and it works great in most cases. Thank you for merging this!

[Tobias Grosser]

I also run into some strange behavior. It seems to me that while changing the name of a tactic that I wrote or replacing this tactic with another tactic preserves the saved state. However, commenting a call to a tactic with -- and dropping this comment leads to a full recomputation.

[Tobias Grosser]

I found trace.Elab.reuse to trace this behavior and get the following output:

[Tobias Grosser]

reuse stopped:
(Command.declValSimple
 "":8493:":=":8495:" "
 (Term.byTactic
  "":8496:"by":8498:"\n  "
  (Tactic.tacticSeq
   (Tactic.tacticSeq1Indented
    [(Tactic.unfold
      "":8501:"unfold":8507:" "
      ["":8508:`and_sequence_40_lhs:8527:" " "":8528:`and_sequence_40_rhs:8547:"\n  "]
      [])
     []
     (tacticSimp_alive_peephole "":8550:"simp_alive_peephole":8569:"\n  ")
     []
     (tacticSimp_alive_undef "":8572:"simp_alive_undef":8588:"\n  ")
     []
     (tacticSimp_alive_ops "":8591:"simp_alive_ops":8605:"\n  --simp_alive_case_bash\n  ")
     []
     (tacticSimp_alive_case_bash "":8633:"simp_alive_case_bash":8653:"\n  ")
     []
     (tacticAlive_auto "":8656:"alive_auto":8666:"\n")])))
 (Termination.suffix [] [])
 []) !=
(Command.declValSimple
 "":8493:":=":8495:" "
 («term_-_»
  (Term.byTactic
   "":8496:"by":8498:"\n  "
   (Tactic.tacticSeq
    (Tactic.tacticSeq1Indented
     [(Tactic.unfold
       "":8501:"unfold":8507:" "
       ["":8508:`and_sequence_40_lhs:8527:" " "":8528:`and_sequence_40_rhs:8547:"\n  "]
       [])
      []
      (tacticSimp_alive_peephole "":8550:"simp_alive_peephole":8569:"\n  ")
      []
      (tacticSimp_alive_undef "":8572:"simp_alive_undef":8588:"\n  ")
      []
      (tacticSimp_alive_ops "":8591:"simp_alive_ops":8605:"\n  ")
      []])))
  "":8608:"-":8609:""
  (Term.app
   "":8609:`simp_alive_case_bash:8629:"\n  "
   ["":8632:`simp_alive_case_bash:8652:"\n  " "":8655:`alive_auto:8665:"\n"]))
 (Termination.suffix [] [])
 [])

[Tobias Grosser]

On the file: SSA/Projects/InstCombine/ScalingTest.lean in https://github.com/opencompl/ssa/pull/314.

[Tobias Grosser]

For what its worth, I am not sure the trace output explains to me clearly why the reuse stopped.

[Sebastian Ullrich]

Thanks for testing! This should be fixed with lean#4268

[Tobias Grosser]

Wow, what a turnaround.

[Tobias Grosser]

I will wait 2-3 days until this pops up in mathlib, but the fix seems generic enough that I am confident it will work. Thank you again for making this happen.

[Tobias Grosser]

We will be testing this from then on!

[Tobias Grosser]

Also, out of interest, is there a significant cost involved in restoring state or is the 'cost' one pays just the tactics that need to be rerun?

[Sebastian Ullrich]

Restoring the state should be effectively free, checking when to restore should be insignificant