how does `Gemfile`/`.bundle/` work?

[quinn-dougherty]

With the following action:

name: Lean Action CI

on:
  push:
  pull_request:
  workflow_dispatch:

permissions:
  contents: read # Read access to repository contents
  pages: write # Write access to GitHub Pages
  id-token: write # Write access to ID tokens

jobs:
  build:
    runs-on: ubuntu-latest

    steps:
      - uses: actions/checkout@v5
      - uses: leanprover/lean-action@v1
      - uses: leanprover-community/docgen-action@v1
      - uses: actions/upload-pages-artifact@v3
        with:
          path: docbuild/.lake/build/doc
      - uses: actions/deploy-pages@v4

I'm getting

[1848/1848] Built CuTe/CuTe:docs (2.4s)
info: Documentation indexing
Build completed successfully (1848 jobs).
Run ruby/setup-ruby@eaecf785f6a34567a6d97f686bbb7bccc1ac1e5c
Modifying PATH
  Entries added to PATH to use selected Ruby:
    /opt/hostedtoolcache/Ruby/3.1.7/x64/bin
Downloading Ruby
  https://github.com/ruby/ruby-builder/releases/download/toolcache/ruby-3.1.7-ubuntu-24.04.tar.gz
  Took   0.50 seconds
Extracting  Ruby
  /usr/bin/tar -xz -C /opt/hostedtoolcache/Ruby/3.1.7 -f /home/runner/work/_temp/5731c066-66c8-4c4a-bdf4-d356fd050795
  Took   0.35 seconds
Print Ruby version
Installing Bundler
> bundle install
Could not determine gemfile path, skipping "bundle install" and caching
Took   0.00 seconds
Run JEKYLL_ENV=production bundle exec jekyll build
Could not locate Gemfile or .bundle/ directory

at the end of the docgen-action step.

Here's the repo https://github.com/for-all-dev/formal-CuTe

[quinn-dougherty]

Sorry-- i found the part of your docs that described how to do this

input: homepage
Default value: home_page

If you would like more than just a docs and a blueprint folder, this action automatically runs the [Jekyll](https://jekyllrb.com/) site generator for you. Run jekyll new home_page in your project folder and commit the resulting home_page folder. The action will automatically detect the home_page folder and build it for you alongside the API documentation and the blueprint. After CI is complete, the compiled site will be available in https://YOUR_USERNAME.github.io/YOUR_PROJECT_NAME.

[quinn-dougherty]

Update: my repo has home_page/Gemfile, and my action doesn't override homepage so it should be looking for Gemfile in home_page as per docs. Still getting same "can't find .bundle/Gemfile" error.

Build completed successfully (1872 jobs).
Run ruby/setup-ruby@eaecf785f6a34567a6d97f686bbb7bccc1ac1e5c
Modifying PATH
Downloading Ruby
Extracting  Ruby
Print Ruby version
  /opt/hostedtoolcache/Ruby/3.1.7/x64/bin/ruby --version
  ruby 3.1.7p261 (2025-03-26 revision 0a3704f218) [x86_64-linux]
  Took   0.02 seconds
Installing Bundler
  Using Bundler 2 shipped with ruby-3.1.7
  Took   0.00 seconds
> bundle install
Could not determine gemfile path, skipping "bundle install" and caching
Took   0.00 seconds
Run JEKYLL_ENV=production bundle exec jekyll build
  JEKYLL_ENV=production bundle exec jekyll build
  shell: /usr/bin/bash --noprofile --norc -e -o pipefail {0}
  env:
    LAKE_PACKAGE_DIRECTORY: .
    API_DOCS: true
    BUILD_ARGS: --log-level=warning
    DOCS_EXISTS: true
    JEKYLL_GITHUB_TOKEN: ***
Could not locate Gemfile or .bundle/ directory

[quinn-dougherty]

Fixed:

1. i was using a docs dir for general markdown files and project discussion, not for what jekyll or docgen-action needs it reserved for. (DOC_EXISTS: true in the logs). I changed my personal documentation to ref dirname, and got the certificate of success from CI.
2. please add that home_page/_config.yml needs to be edited with org-name.github.io and repo-name, because i was still getting 404 since i had left that default.

EDIT:

this is bizarre: when i pushed the urls to home_page/_config.yml and ran the job again, it failed due to docbuild/references.bib not existing. But the commit that got the CI certificate of success also did not have docbuild/ dir!

I'm going to re-add the docbuild dir as described here https://github.com/leanprover/doc-gen4 in readme, will report back what happens.

EDIT: same error. See full tree and job file here https://github.com/for-all-dev/formal-CuTe/tree/05ceaaf7aa59cef4dae5d6f2a8ec85da214d8d97

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
✖ [1318/1318] Building CuTe/CuTe:docs (2.7s)
info: Documentation indexing
trace: .> /home/runner/work/formal-CuTe/formal-CuTe/.lake/packages/doc-gen4/.lake/build/bin/doc-gen4 index --build /home/runner/work/formal-CuTe/formal-CuTe/docbuild/.lake/build
error: no such file or directory (error code: 2)
  file: /home/runner/work/formal-CuTe/formal-CuTe/docbuild/.lake/build/doc/references.bib
error: build failed
Some required targets logged failures:
- CuTe/CuTe:docs
Error: Process completed with exit code 1.

Here is the successful job that deployed a 404 to https://for-all-dev.github.io/formal-CuTe: https://github.com/for-all-dev/formal-CuTe/actions/runs/21116855288

[kim-em]

The issues reported here have a few different causes:

1. references.bib not found error

This was a bug in doc-gen4 where it tried to read references.bib before the file was created. Fixed in leanprover/doc-gen4#354.

The fix is now included in the v4.28.0-rc1 tag, so projects using Lean toolchain v4.28.0-rc1 or later will get it automatically. For older toolchains, create an empty references.bib file in your repository root as a workaround.

2. Gemfile not found error

This happens when the action detects a docs folder (triggering Jekyll build) but there's no Gemfile in it. Two solutions:

• Run jekyll new docs to create a proper Jekyll site, OR
• Set build-page: false in the action inputs if you don't want a Jekyll site

3. README said wrong default for homepage

The README incorrectly said the default was home_page when it's actually docs. Fixed in #21.

---

For the formal-CuTe project specifically: you had a docs folder for general documentation which triggered Jekyll detection. Renaming it (as you did) or setting build-page: false are the correct solutions.