Zulip Chat Archive

Stream: new members

Topic: leanproject new


Horatiu Cheval (Mar 03 2021 at 16:05):

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 (Mar 03 2021 at 16:13):

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

Johan Commelin (Mar 03 2021 at 16:17):

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

Horatiu Cheval (Mar 03 2021 at 16:19):

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

Horatiu Cheval (Mar 03 2021 at 16:20):

But elan default stable fixed it.


Last updated: Dec 20 2023 at 11:08 UTC