aristotle task for command palette

Stream: PR reviews

[Kim Morrison]

feat: add Aristotle task for command palette #30842

I would like to start being able to conveniently use Aristotle! Could we please have a review/decision on this?

[Oliver Nash]

I'm in favour. I've used Aristotle a bit and found it useful and this would make me use it more.

[Christian Merten]

To me it seems odd to maintain a .vscode/tasks.json that invokes a third party tool, of which the interface is not under mathlibs control.
Maybe Harmonic would instead like to provide a VS code extension that makes the task in this PR available.

[Yaël Dillies]

I agree with Christian, although I would be okay with adding the task in the meantime

[Eric Wieser]

Or just (have Harmonic) add documentation to tell users to put this in the file which "Tasks: Open User Tasks" opens in VSCode

[Kim Morrison]

But then no one uses it...?

I really dislike doing any custom setup for my Lean installation, because it means I then have a feature than >90% of people will be missing.

(I do agree this argument doesn't completely apply here, as one has to sign up for an API key to make this work.)

[Kim Morrison]

My understanding is that Harmonic are intending to do more in this direction. I'd still like to have this in the meantime.

[Anatole Dedecker]

But should we be the ones maintaining it? To me it feels out of scope.

[Kevin Buzzard]

Kim Morrison said:

But then no one uses it...?

I really dislike doing any custom setup for my Lean installation, because it means I then have a feature than >90% of people will be missing.

(I do agree this argument doesn't completely apply here, as one has to sign up for an API key to make this work.)

I have claude code pro set up on my repos so I have a feature which >90% of people are missing, is this any different?

[Nick_adfor]

I've tried to prove by Aristotle but failed. In fact I do not have the ability to check how Aristotle works. I may think not all the coders can check how Aristotle works and develop it : (