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):
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):
elan default stable fixed it.
Last updated: May 08 2021 at 10:12 UTC