error: no such file or directory
Seasawher opened this issue · 4 comments
Running lake -Kenv=dev build MyPackage:docs as described in the README gives the error in the title.
That is far too little information to reproduce or fix anything, can you elaborate further on at least:
- What is your package?
- How does your lakefile look?
- What is your lean version?
If you can publish your package can I get a link to it so I can debug on my end?
Thank you for your reply.
Please see https://github.com/Seasawher/lean-math-workshop/tree/feature/doc-gen4 and use gitpod to setup.
If I clone that branch and run the same command as you:
λ lake -Kenv=dev build Tutorial:docs
error: unknown library facet `docs`
This error happens because this branch is not at all configured to work with doc-gen4 as described in the README. If I follow the 3 steps from the README I will get an actual error:
error: no such file or directory (error code: 2)
file: ./././Tutorial.lean
Which I assume is the one that you were actually seeing yourself? The interesting part of this error is of course which file is missing. But this is not a doc-gen error. If you run just lake build Tutorial or even lake build you will get the same error so this is broken because your lakefile/project structure is improperly set up. If you declare a lean_lib of name Tutorial without modifying the source location via options in the lakefile your lake will expect there to be a file Tutorial.lean in the root that imports the subpackages from other directories.
Thank you. I apologize for the incompleteness of my question.