Hacktoberfest 2026: the issues maintainers tagged for October, open and beginner-friendly. Browse Hacktoberfest issues

Lake: `moreServerOptions` not passed to the server for files inside a library

Open Beginner friendly
  • Is something wrong?
#15,626 0 comments 0 reactions 0 assignees View on GitHub

Maintainers usually reply within 1 day

Nobody has claimed this yet.

Assessment

Difficulty
2/5
Estimated time
1-3 hours
Newbie friendliness
82/100
Issue type
Bug
Clarity
Clearly specified
Activity status
Active
Domain
tooling

Research direction

Read Lake/Build/Module.lean, starting at setupEditedModule, and compare its server options with setupExternalModule and getServerOptions. The reproduction uses lake setup-file on a library file and an external file; done when both report the expected moreServerOptions value for the library file as well.

Written by the indexing model from the issue text.

Description

[Claude Agent] Filed on behalf of @wrwg from a Claude Code session; the reproduction was run as described.

lake setup-file includes moreServerOptions only for files Lake does not identify as a library module. In Lake/Build/Module.lean, setupEditedModule sets

      options := mod.leanOptions

although Module.serverOptions exists for this (it accumulates the package's and library's leanOptions and moreServerOptions). setupExternalModule does use getServerOptions, so files outside every library get them.

Reproduction

lakefile.toml:

name = "laketest"
defaultTargets = ["Foo"]
leanOptions = { maxHeartbeats = 400000 }
moreServerOptions = { "pp.unicode.fun" = true }

[[lean_lib]]
name = "Foo"

with Foo.lean and External.lean (any contents) next to it:

$ lake build
$ lake setup-file Foo.lean       # library module
{..., "options":{"maxHeartbeats":400000}, ...}
$ lake setup-file External.lean  # outside the library
{..., "options":{"maxHeartbeats":400000,"«pp.unicode.fun»":true}, ...}

Expected: Foo.lean also gets pp.unicode.fun, i.e. options := mod.serverOptions.

Lake 5.0.0-src+f3b06c7 (Lean 4.32.2), Linux aarch64.

Dominant language
Lean
Stars
9.5k
Forks
1k
Avg merge
1d 4h
Merged PRs (30d)
270

Getting set up

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from leanprover/lean4

All issues in leanprover/lean4

Similar issues

More DevTools issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.