aesop

Stream: mathlib4

[Scott Morrison]

@Jannis Limperg, it seems that declare_aesop_rule_sets is forgotten between files. I can file an issue with an example tomorrow.

[Jannis Limperg]

I'm investigating, no need for a test case. Thanks!

[Jannis Limperg]

Fixed.

[Scott Morrison]

@Jannis Limperg, if you have a chance to merge https://github.com/JLimperg/aesop/pull/32 that would be helpful; we need it to be able to bump mathlib4.

[Scott Morrison]

Oh, sorry, there is still a build error.

[Scott Morrison]

Fixed, by adding an unexpected .{0}

[Jannis Limperg]

Done, thanks! (The .{0} was actually on an unnecessary assumption.)

[Jannis Limperg]

Btw, if anyone wants maintainer rights for the Aesop repo, or if you want to move Aesop into leanprover-community, I'd be happy to do that.

[Mario Carneiro]

Hi @Jannis Limperg, can you send me maintainer rights for Aesop? I like to have maintainer rights for dependencies of mathlib so I can roll out traumatic nightly updates as atomically as possible.

[Mario Carneiro]

I think moving to leanprover-community isn't a requirement, seeing as quote4 and std4 are also not under leanprover-community

[Mario Carneiro]

but I don't have an issue with doing so if you would like to make it look more official

[Jannis Limperg]

Mario Carneiro said:

Hi Jannis Limperg, can you send me maintainer rights for Aesop? I like to have maintainer rights for dependencies of mathlib so I can roll out traumatic nightly updates as atomically as possible.

Done!

[Jannis Limperg]

Mario Carneiro said:

I think moving to leanprover-community isn't a requirement, seeing as quote4 and std4 are also not under leanprover-community

Okay then let's just keep it as it is for now.

[Moritz Doll]

one thing that would be nice is that aesop (and std4) could allow for downloading prebuild nightly-releases. I've looked a bit into the lake cloud release feature and it seems not to play well with what mathlib3 did before, but it should be very easy to use for dependencies, which would slightly decrease the build times

[Jannis Limperg]

I wasn't aware of this Lake functionality, but it looks really nice. I'll look into it.

[Heather Macbeth]

I am getting an error in Aesop/Tree/Data. I'm on

Lean (version 4.0.0-nightly-2022-12-22, commit a2f595911898, Release)

Std

a109889bf299f0d086f93a228e4c152f40ff5b0d

and Aesop

79127e2c0a6254eae99a1e919fdd6da8815189ff

(both seem to be the latest versions). Has anyone else seen it?

[Heather Macbeth]

The error:

instance [Nonempty Goal] : Nonempty (RappData Goal MVarCluster) :=
  ⟨{ id := default
     parent := Classical.ofNonempty
     children := default
     state := default
     isIrrelevant := default
     appliedRule := default
     scriptBuilder := default
     originalSubgoals := default
     successProbability := default
     metaState := default -- failed to synthesize instance Inhabited SavedState
     introducedMVars := default
     assignedMVars := default }⟩

[Lukas Miaskiwskyi]

I've been running into the same error during lake build on a freshly cloned mathlib4, only since today. Together with an error in Data.Int.Basic , which I am not sure is related:

Mathlib\Data\Int\Basic.lean:278:44: error: Declaration Int.toNat_add_toNat_neg_eq_nat_abs not found.

[Sebastian Ullrich]

That shouldn't happen, Gabriel linked mathlib4 to to his updated version of Aesop https://github.com/JLimperg/aesop/pull/37

[Sebastian Ullrich]

https://github.com/leanprover-community/mathlib4/commit/4b0358a2186132a387f3278f1519632cdbeb4c70#diff-d2bbbefe896fa3db86583f19e6fb402ed9ba755d564f4de97f398b0596f4c2b8L35-R37

[Heather Macbeth]

I wonder if the following is the problem: at some point this morning when I had run lake build, I received the message

% lake build
warning: manifest out of date: git url of dependency aesop changed, use `lake update` to update

so I followed its instructions:

% lake update
updating ./lake-packages/std to revision a109889bf299f0d086f93a228e4c152f40ff5b0d
aesop: URL has changed; deleting ./lake-packages/aesop and cloning again
cloning https://github.com/JLimperg/aesop to ./lake-packages/aesop

[Heather Macbeth]

Is there a command to undo my lake update?

[Sebastian Ullrich]

Reverting the changes to lake-manifest.json should do it

[Sebastian Ullrich]

I'm assuming Gabriel didn't update the Aesop URL in lakefile.lean since it was supposed to be a temporary change, but that warning is confusing, yeah

[Sebastian Ullrich]

Just ignore it for now, after reverting

[Heather Macbeth]

Thanks!

[Kevin Buzzard]

FWIW I just fell into the same trap. Thanks for the fix Sebastian!

[Riccardo Brasca]

I run the start_port.sh on freshly cloned mathlib4, and after running lake build I get

warning: manifest out of date: git url of dependency aesop changed, use `lake update` to update
error: no such file or directory (error code: 2)
  file: ./././Mathlib/Algebra/Group/Ulift.lean

(Ulift.lean is the file I wanted to port). Trying lake update doesn't help.

[Riccardo Brasca]

The same happens to CI: #1240.

[Sebastian Ullrich]

For the warning see above. The error is likely unrelated (edit: see PR).

[Riccardo Brasca]

Oh, I sorry, I just didn't read the error message. Thanks!

[Johan Commelin]

Do I understand correctly that in the near future we should go through all of mathlib and tag hundreds (thousands?) of lemmas as aesop-lemma? And that this will make aesop exponentially more powerful?
Or do I just not understand how aesop works?

[Scott Morrison]

Something like that. Possibly @[aesop] labels should be divided up in rule sets, but also possibly not. apply rules for aesop live in a discrimination tree (fast) and apply itself fails very fast.

[Heather Macbeth]

Scott Morrison said:

Something like that. Possibly @[aesop] labels should be divided up in rule sets, but also possibly not. apply rules for aesop live in a discrimination tree (fast) and apply itself fails very fast.

Not always ... do you remember this example?
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Slowly-failing.20solve-by-elim.20call/near/343143451

[Scott Morrison]

Good reminder! :-)