search

leanprover / doc-gen4

Document Generator for Lean 4
Apache License 2.0
62 stars 41 forks source link

error: no such file or directory #142

Closed Seasawher closed 1 year ago

Seasawher commented 1 year ago

Running lake -Kenv=dev build MyPackage:docs as described in the README gives the error in the title.

hargoniX commented 1 year ago

That is far too little information to reproduce or fix anything, can you elaborate further on at least:

If you can publish your package can I get a link to it so I can debug on my end?

Seasawher commented 1 year ago

Thank you for your reply.

Please see https://github.com/Seasawher/lean-math-workshop/tree/feature/doc-gen4 and use gitpod to setup.

hargoniX commented 1 year ago

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.

Seasawher commented 1 year ago

Thank you. I apologize for the incompleteness of my question.