0
$\begingroup$

I want to initialize a lean project but the folder I have already exists. How do I do this?

e.g.,

# -- Go to a folder where you want to create a project in a subfolder my_project, and type lake +leanprover/lean4:nightly-2023-02-04 new my_project math.
cd $HOME
lake +leanprover/lean4:nightly-2023-02-04 new my_project math

but I get the following error

~ ❯ mkdir my_project
mkdir: my_project: File exist

I do not want to alter the contents or move my_project, but have the lake command do whatever it needs to do even if the folder exists. I do not want to move the contents out of my_project etc. Just that lake +leanprover/lean4:nightly-2023-02-04 new my_project math works even if the folder exists.

Improve this question
$\endgroup$
2
  • $\begingroup$ Change my_project to any name you want that doesn't match an existing directory. $\endgroup$
    – François G. Dorais
    Commented Feb 23 at 2:45
  • $\begingroup$ What do you want to happen if my_project contains files whose names are the same as project system files which lake wants to create as part of the process of creating a new project? What do you want to happen if my_project is already a git repo? My instinct is that you should solve these questions yourself by renaming my_project to foo, using lake to create my_project and then copying the files from foo back into my_project, being very careful if there are any name clashes. $\endgroup$
    – Kevin Buzzard
    Commented Feb 24 at 15:37

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.