Skip to content

--tstack=100000000 in lakefile.toml causes failed to create thread in CI #12

Description

@astefano

The Loom lib in lakefile.toml passes a 100 MB per-thread stack to Lean:

moreLeanArgs = ["-Dwarn.sorry=false", "--tstack=100000000"]

When Lean builds with its default worker-thread pool, each thread requests that stack, which exceeds the limits on a GitHub Actions runner. The build dies immediately:

✖ [2/22] Building Loom.LatticeExt
failed to create thread
error: Lean exited with code 1

Building single-threaded (-j1) avoids the oversized per-thread stacks and the failure. Verified on a fork: after --tstack=100000000-j1, the build proceeds past LatticeExt, and with an elan-resolvable toolchain (#10) and the workflow in place (#8) it completes green (22/22 jobs).

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions