asyncI

Stream: condensed mathematics

[Johan Commelin]

I've added a file hacks_and_tricks.asyncI with the help of @Gabriel Ebner

$ time lean --make src/for_mathlib/derived/K_projective.lean

real    1m25.932s
user    1m36.875s
sys     0m3.854s
------
$ time lean --make src/for_mathlib/derived/K_projective_async.lean

real    0m59.830s
user    1m28.652s
sys     0m3.774s

[Johan Commelin]

The idea is that you can wrap subgoals that do not depend on any metavariables with asyncI like so:

  asyncI
  { my_sub_proof,
    foobar },

[Johan Commelin]

And then Lean will check those subgoals in parallel

[Johan Commelin]

It also works for proof obligations in records, like so:

@[simps]
def Ext0 : 𝒦ᵒᵖ ⥤ 𝒦 ⥤ Ab :=
{ obj := λ X, preadditive_yoneda.flip.obj (opposite.op $ X.unop.replace),
  map := λ X₁ X₂ f, preadditive_yoneda.flip.map (lift (X₂.unop.π ≫ f.unop) X₁.unop.π).op,
  map_id' := by asyncI { -- ASYNC!!
    intros X,
    ext Y e,
    dsimp [preadditive_yoneda, preadditive_yoneda_obj],
    change _ ≫ e = e,
    simp only [category.comp_id, id_apply],
    convert category.id_comp _,
    symmetry,
    apply lift_unique,
    simp, },
  map_comp' := by asyncI { -- ASYNC!!
    intros X₁ X₂ X₃ f g,
    ext Y e,
    dsimp,
    simp only [comp_apply, linear_map.to_add_monoid_hom_coe,
      preadditive_yoneda_obj_map_apply, quiver.hom.unop_op],
    change _ ≫ e = _ ≫ _ ≫ e,
    conv_rhs { rw ← category.assoc },
    congr' 1,
    symmetry,
    apply lift_unique,
    simp } }

[Johan Commelin]

So far, I've only used this in K_projective.lean. But I suppose there are plenty files that can benefit from this.

[Johan Commelin]

lean#706 is fixing Lean so that async works well with the instance cache. Once that PR lands, and LTE moves to the next version of Lean, we can drop the hacks file, and replace all asyncI with async.

[Johan Commelin]

I haven't tested, but I think we can now write asyncI { slow subproof } instead of using the sorry { slow subproof } trick. And then goals below it should still be responsive quickly.

[Sebastien Gouezel]

Is that crazy to imagine that this could be done automatically everywhere? (I mean, when you open braces, Lean checks whether there are metavariables in the current goal, and if there are none it runs the block in an async way)?

[Johan Commelin]

Probably not for Lean 3. I imagine it would take quite some work to implement that.
cc @Mario Carneiro

[Johan Commelin]

afaik, Lean 4 already does something like that

[Mario Carneiro]

No metavariables in the current goal is not sufficient, right? I mean the metavariable could appear in other goals, so resolving it could affect your other proof branches nondeterministically

[Mario Carneiro]

plus any tactic can call result and watch it change in real time

[Mario Carneiro]

considering that this is a rather fundamental change to goal management, I am inclined to agree with Johan and say "unlikely in lean 3, possible (but still unlikely) in lean 4"

[Mario Carneiro]

well, it's probably possible to do something like this in lean 3 if you don't mind random unlikely heisenbugs

[Johan Commelin]

@Mario Carneiro But if you only apply this to metavariables that are Props, then this "affect your other proof branches nondeterministically" shouldn't cause problems right?

[Mario Carneiro]

the problem is a lot more fundamental than that; what if you check that a metavariable is assigned, see that it is not and make a branching decision based on that (while another thread assigns it behind you), and then assign it and boom you get a conflict. Assuming that the local context updates are being done in a threadsafe way it's not undefined behavior but it could still lead to nondeterministic failure

[Johan Commelin]

Sure, but realistically, why would you branch on whether a certain proof obligation has been solved?

[Mario Carneiro]

because it was a goal and you were asked to solve the first goal

[Mario Carneiro]

and lean cleans up assigned metavariables in the goal list

[Johan Commelin]

I think that there is a theoretical model for goal management / ATP where this is not a problem.

[Mario Carneiro]

I agree, and I also think this model is not lean 3 or even lean 4

[Mario Carneiro]

it's probably closer to the HOL model where the goals are tracked through the type system

[Mario Carneiro]

One approach that could work in the lean 3 model (but is still a lot of work to implement) is that we launch a task at any focus block regardless of any dependencies, and this immediately assigns the metavariable with a task<expr> macro which is forced to a value (i.e. made serial again) if any downstream tasks need to ask what expression was assigned there