Deploy docs as the main page

[mdbrnowski]

From the README:

When CI completes, the API documentation can be found at https://YOUR_USERNAME.github.io/YOUR_PROJECT_NAME/docs.

Is it possible (or could such an option be added) to deploy the docs at YOUR_PROJECT_NAME instead of YOUR_PROJECT_NAME/docs?

[arademaker]

+1 with the same question

[arademaker]

I see now here that docs folder is hardcoded.

Can we make it more flexible? See plan below

1. We could allow the users to define the folder name. So docs will be only the default value for a input like doc-folder.
2. We can also add one extra input called docs-only accepting true/false. If true, the build-page and blueprint will need to be false (or assumed as false). In the end of the scripts/build_docs.sh we will need to check of this flag and copy the docbuild/.lake/build/doc to $HOMEPAGE or $HOMEPAGE/$DOCFOLDER.

Does it make sense?

[arademaker]

Implementation Proposal: build-doc-only Parameter

📋 Summary

Add a new build-doc-only parameter that simplifies the build to API docs only, automatically disabling Jekyll and blueprint. Documentation continues to be copied to $HOMEPAGE/docs (no changes to bash script), but the upload deploys directly from that folder, resulting in docs at the root of the published site.

🎯 Expected Behavior

When build-doc-only=true:

1. ✅ Force blueprint=false (never build blueprint)
2. ✅ Force build-page=false (never run Jekyll)
3. ✅ Keep copying docs to $HOMEPAGE/docs (no changes to build_docs.sh)
4. ✅ Upload $HOMEPAGE/docs for deployment (docs at site root)
5. ✅ build-doc-only takes precedence over other parameters

📁 Files to Modify

1. action.yml

Change 1.1: Add new input

Location: after line 51

  build-doc-only:
    description: Build only API documentation without Jekyll site or blueprint. When enabled, overrides build-page and blueprint settings to false, and copies docs directly to homepage root.
    required: false
    default: "false"

Change 1.2: Modify "Check for homepage folder" condition

Location: line 83

From:

if: inputs.build-page == 'true'

To:

if: inputs.build-page == 'true' && inputs.build-doc-only != 'true'

Change 1.3: Modify "Build blueprint" condition

Location: line 95

From:

if: inputs.blueprint == 'true'

To:

if: inputs.blueprint == 'true' && inputs.build-doc-only != 'true'

Change 1.4: Modify "Check declarations" condition

Location: line 117

From:

if: inputs.blueprint == 'true'

To:

if: inputs.blueprint == 'true' && inputs.build-doc-only != 'true'

Change 1.5: Modify "Bundle dependencies" condition

Location: line 133

From:

if: github.event_name == 'push' && inputs.build-page == 'true' && env.DOCS_EXISTS == 'true'

To:

if: github.event_name == 'push' && inputs.build-page == 'true' && inputs.build-doc-only != 'true' && env.DOCS_EXISTS == 'true'

Change 1.6: Modify "Build website using Jekyll" condition

Location: line 141

From:

if: github.event_name == 'push' && inputs.build-page == 'true' && env.DOCS_EXISTS == 'true'

To:

if: github.event_name == 'push' && inputs.build-page == 'true' && inputs.build-doc-only != 'true' && env.DOCS_EXISTS == 'true'

Change 1.7: Modify upload path logic (MOST IMPORTANT)

Location: line 152

From:

path: ${{ env.DOCS_EXISTS == 'true' && format('{0}/_site', inputs.homepage) || format('{0}/', inputs.homepage) }}

To:

path: ${{ inputs.build-doc-only == 'true' && format('{0}/docs', inputs.homepage) || (env.DOCS_EXISTS == 'true' && format('{0}/_site', inputs.homepage) || format('{0}/', inputs.homepage)) }}

Ternary expression logic:

• If build-doc-only=true: upload $HOMEPAGE/docs
• Else if DOCS_EXISTS=true: upload $HOMEPAGE/_site (Jekyll)
• Else: upload $HOMEPAGE/ (docs without Jekyll)

---

2. README.md

Change 2.1: Add documentation

Location: after line 103 (after references section)

### input: `build-doc-only`

Allowed values: `false`, `true`

Default value: `false`

Set to true to build only API documentation without Jekyll site or blueprint. When enabled:
- Overrides `build-page` to effectively disable Jekyll processing
- Overrides `blueprint` to effectively disable blueprint generation
- Copies documentation directly to the homepage root directory
- Uploads only the `docs` folder for deployment

This is useful for projects that only need API documentation without additional site infrastructure.

Example usage:
```yaml
- name: Build project documentation (API docs only).
  id: build-docgen
  uses: leanprover-community/docgen-action@main
  with:
    build-doc-only: true
```

---

🔧 Implementation Order

1. action.yml: Make 7 changes (1.1 to 1.7)
2. README.md: Add documentation (2.1)

Important note: build_docs.sh does NOT need to be modified - it keeps the current behavior of copying to $HOMEPAGE/docs

✨ Advantages of This Approach

• ✅ Only 2 files modified
• ✅ No conditional logic in bash
• ✅ $HOMEPAGE/docs always exists, regardless of mode

---

🔄 Backward Compatibility

✅ 100% compatible - Default is "false", does not affect existing workflows

---

📊 Behavior Matrix

build-doc-only	build-page	blueprint	Copy in build	Upload	Result on site
false	true	true	$HOMEPAGE/docs	$HOMEPAGE/_site	Jekyll + Blueprint + docs at /docs/
false	false	false	$HOMEPAGE/docs	$HOMEPAGE/	Only docs at /docs/
true	any	any	$HOMEPAGE/docs	$HOMEPAGE/docs	Docs at root /

Key difference: In build-doc-only=true mode, we upload directly from $HOMEPAGE/docs (skipping Jekyll), resulting in documentation at the root of the published site (/) instead of at /docs/.

---

✅ Recommended Test Cases

1. ✓ build-doc-only: true (basic - API docs only)
2. ✓ build-doc-only: true + build-page: true (verify build-doc-only takes precedence)
3. ✓ build-doc-only: true + blueprint: true (verify build-doc-only takes precedence)
4. ✓ build-doc-only: true + homepage: custom-folder (custom path)
5. ✓ build-doc-only: false or omitted (backward compatibility - current behavior)

---

⚠️ Risks and Mitigations

Risk	Level	Mitigation
Complex nested ternary expression (line 152)	Low	Extensive testing with all combinations
Users may not understand precedence	Low	Clear documentation in README

---

💡 Use Case

This parameter is useful for Lean projects that:

• Want only API documentation without Jekyll overhead
• Don't need blueprint
• Prefer documentation directly at site root (/) instead of at /docs/
• Seek faster and simpler builds