tooling to update a project's toolchain?

Stream: new members

[Jens Petersen]

Is there any tool to update the lean-toolchain file in a project?

I suppose the simplest way to override toolchain is elan run <toolchain> lake build, etc, right?
Is there is any way to force/choose the default elan toolchain? I hope that's the right question

[Ruben Van de Velde]

You can change the toolchain file with your favourite text editor. Using elan in the way you suggest is strongly recommended against

[Jens Petersen]

Okay but I think it would be nice to have a update-toolchain command.
Also I might want to try building my project against different versions?

[Ruben Van de Velde]

I'm afraid that's currently not really realistic for a project of any size

[Jens Petersen]

Sorta unrelated question, but I see many projects (eg on reservoir) using lean-toolchain with leanprover/lean4:v4.13.0 etc, whereas lake new currently generates just 4.13.0.
I know they are basically similar/equivalent, but is the latter now considered the preferred format?

[Ruben Van de Velde]

This always confuses me too - I haven't figured out the answer yet