action does not respect lake-package-directory

[b-mehta]

The action does not respect the lake_package_directory setting

[jcreedcmu]

I think actually the action does currently not respect any of the options managed by deprecation.js, in either their deprecated (underscore) or non-deprecated (hypen) forms:

api_docs
api-docs
lake_package_directory
lake-package-directory
build_args
build-args

#14 should fix this.

[jcreedcmu]

In this workflow (against my PR) I can see it respecting my value of lake-package-directory and then clearly failing trying to access the made-up directory.

[jcreedcmu]

@b-mehta out of band explained that perhaps #14 doesn't actually fix all of this issue.

As I understand it, the typical project directory structure when we have blueprints is

lean_development/
  blueprint/
    print/
    src/
    web/
  .lake/
  lean-toolchain
  lakefile.toml
  MyMath.lean
  MyMath/Basic.lean
  etc.

and by setting lake_package_directory: "lean_development" we might be able to accommodate instead

proj/
  lean_development/
    .lake/
    lean-toolchain
    lakefile.toml
    MyMath.lean
    MyMath/Basic.lean
    etc.
  blueprint/
    print/
    src/
    web/

Maybe this works for the doc-gen4 parts of the docgen-action, but I don't currently see any command-line flags for leanblueprint that would tell it to find the blueprint/ directory anywhere other than the current directory.

[b-mehta]

Nonetheless, the change in #14 still helps when blueprint is not enabled!

[jcreedcmu]

Further out of band conversation convinced me that the case we actually want to handle is merely

deeply/
  nested/
    lean_development/
      blueprint/
        print/
        src/
        web/
      .lake/
      lean-toolchain
      lakefile.toml
      MyMath.lean
      MyMath/Basic.lean
      etc.

(and in this example the docgen-action caller would want

with:
 lake-package-directory: "deeply/nested/lean_development"

)
so I think #14 now has enough working_directory:s to handle this case.

[jcreedcmu]

I was wrong! #14 doesn't quite solve everything yet. I'm going to recap what I know now. There's at least a few things going on.

• Prior to fix: thread through workflow inputs to deprecation.js #14, the workflow inputs never actually reached the deprecation.js script due to how GitHub actions isolates steps; fix: thread through workflow inputs to deprecation.js #14 at least solves this. This at least makes theapi-docsoption actually work, whereas it didn't before in my testing.
• Even if the workflow input lake-package-directory successfully makes its way into deprecation.js, thereby being turned into the env var LAKE_PACKAGE_DIRECTORY, that env var in turn doesn't yet influence the blueprint steps in the action --- so that if you're like @b-mehta (or his student) and you want to put the entire lean-project-that-has-a-blueprint in a nested directory, you're out of luck if you want to generate blueprints from it
• Even if we thread that environment variable through to the step that runs leanblueprint and does a cd $LAKE_PACKAGE_DIRECTORY, leanblueprint cleverly looks up through its parent directories and runs from the nearest git repo, not the current directory. So if you're doing what @b-mehta wants to do, you're out of luck, because now leanblueprint is running from the parent directory of where lakefile.toml and blueprint/ and friends live.
• If docgen-action does a git init inside $LAKE_PACKAGE_DIRECTORY before running leanblueprint, then it correctly generates a blueprint, but now the intended meaning of homepage path is a little uncertain to me: is it supposed to be relative to the git repo root, or relative to $LAKE_PACKAGE_DIRECTORY? If I could settle this question I think I could fix fix: thread through workflow inputs to deprecation.js #14 do the right thing.

[NullDev]

Is there any workaround for this? I tried setting it both as env-var as well es using with but it still tries to look in the repo root.

    steps:
      - uses: actions/checkout@v5
      - uses: leanprover/lean-action@v1
        with:
          lake-package-directory: "lean_convergence_proof"
      - uses: leanprover-community/docgen-action@v1
        with:
          lake-package-directory: "lean_convergence_proof"
        env:
          LAKE_PACKAGE_DIRECTORY: "lean_convergence_proof"