feat: per-package server options

[mhuisi]

This PR adds per-package server options to resolve #2455. It is based on the previous work in #2456, but takes a different approach: options are loaded for the specific file in the file worker when print-paths is called, instead of loading them in the watchdog with a separate Lake command. This change addresses review comments made in #2456.

In doing so, it introduces two new Lake config fields:

• leanOptions: -D flag options that are passed to both the language server and lean when building.
• moreServerOptions: -D flag options that are passed to the language server.

Since print-paths must also accept a file path to compute the options for that file, this PR is changing the API for print-paths. As there have been numerous complaints about the name print-paths, I also decided to change it to setup-file in this PR, since it would break compatibility with the old Lake API anyways.

This PR deprecates the Lakefile field moreServerArgs in favor of moreGlobalServerArgs, as suggested in the review for #2456.

Updating your Lakefile

A Lakefile with the following package declaration:

def moreServerArgs := #[
  "-Dpp.unicode.fun=true"
]
def moreLeanArgs := moreServerArgs

package SomePackage where
  moreServerArgs := moreServerArgs
  moreLeanArgs := moreLeanArgs

... can be updated to the following package declaration to use per-package options:

package SomePackage where
  leanOptions := ⟨`pp.unicode.fun, true⟩

A package configuration that does not set moreLeanArgs can use moreServerOptions instead of leanOptions:

package SomePackage where
  moreServerOptions := ⟨`pp.unicode.fun, true⟩

Fixes #2455

[mhuisi]

(cc @Kha to adjust the Nix stuff)

[mhuisi]

The tests are red because of a bug in System.Uri.fileUriToPath?. I will investigate it later.

[tydeu]

LGTM!

[mhuisi]

The tests are red because of a bug in System.Uri.fileUriToPath?. I will investigate it later.

It's worse: The tests used an incorrect URI format and it never caused problems before!

[leanprover-community-mathlib4-bot]

• ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-11-10 21:16:20)
• 🟡 Mathlib branch lean-pr-testing-2858 build this PR didn't complete normally. (2023-11-10 21:19:14) View Log
• ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-11-14' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2023-11-14 11:56:18)
• ❌ Mathlib branch lean-pr-testing-2858 built against this PR, but lean4checker failed. (2023-11-20 04:50:47) View Log
• ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-11-20' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2023-11-21 10:45:35)
• ✅ Mathlib branch lean-pr-testing-2858 has successfully built against this PR. (2023-11-23 15:38:49) View Log
• ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-11-25' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2023-11-25 20:34:20)
• 💥 Mathlib branch lean-pr-testing-2858 build failed against this PR. (2023-11-25 21:26:00) View Log
• ✅ Mathlib branch lean-pr-testing-2858 has successfully built against this PR. (2023-11-26 10:31:09) View Log

[tydeu]

I missed something! Since you renamed moreServerArgs, the math package template needs to be updated as well:
https://github.com/mhuisi/lean4/blob/aa0774467e9ce6ab5f911bd06674593967283bbd/src/lake/Lake/CLI/Init.lean#L98-L118

Also, for temporary backwards compatibility, it might be worth it for one version to leave the PackageConfig.moreServerArgs field and have moreGlobalServerArgs default to it. To deprecate a property like this one, I usually put a note on its deprecation in the docstring, remove the mention of it in the README, and potentially a warning issue during package config load if it is non-empty (for reference, see how I deprecated manifestFile).

[kim-em]

Note that the Mathlib bot reporting that PR didn't complete normally is actually a failure:

Run lake exe cache clean
error: ./lakefile.lean:26:2: error: 'moreServerArgs' is not a field of structure 'Lake.PackageConfig'
error: ./lakefile.lean: package configuration has errors
Error: Process completed with exit code 1.

If you're able to make changes to the lean-pr-testing-2858 branch of Mathlib directory to make it compatible with these chaanges, please go ahead. Ping me if you need assistance on the Mathlib side.

[tydeu]

Some minor suggestions that help the code of the new options fit the style of other package configuration options. Otherwise, LGTM!

[tydeu]

@mhuisi I think you lost the library's leanOptions when addressing my suggestions.