leanproject new

Stream: new members

[Horatiu Cheval]

After installing Lean4 following the basic setup I am no longer able to run leanproject new [PATH] to create a new lean project. It returns uncaught exception. It only works to create a Lean3 project if I run it from within the directory of an already existing Lean3 project. Is this what it should happen? What do I have to do in order to create a Lean3 projects now?

[Bryan Gin-ge Chen]

Probably setting elan's default Lean to Lean 4 is breaking things. Try elan default stable.

[Johan Commelin]

@Horatiu Cheval leanproject was designed for lean3, I would be surprised if it just works with lean4...

[Horatiu Cheval]

I see, I wasn't trying that. The problem was I was no longer able to use it for Lean3

[Horatiu Cheval]

But elan default stable fixed it.