Code

feat: per-package server options#2858

Code

Merged

mhuisi merged 18 commits intoleanprover:masterleanprover/lean4:masterfrom mhuisi:mhuisi/per-package-server-optionsmhuisi/lean4:mhuisi/per-package-server-optionsCopy head branch name to clipboardNov 26, 2023

+780-516

Commits

Commits on Nov 23, 2023

• feat: per-package server options

  Show description for ab5bfef
  

  mhuisi

  and

  digama0

  committed
  ab5bfef

  Copy full SHA for ab5bfef

• test: use correct file uri in interactive tests

  mhuisi

  committed
  612f93e

  Copy full SHA for 612f93e

• refactor: style and Lean.Util import

  mhuisi

  committed
  7670b07

  Copy full SHA for 7670b07

• fix: adjust math template

  mhuisi

  committed
  40034eb

  Copy full SHA for 40034eb

• chore: deprecate moreServerArgs instead of removing it

  mhuisi

  committed
  f6d64a7

  Copy full SHA for f6d64a7

• feat: converting ServerOption to cli arg

  mhuisi

  committed
  2188cbd

  Copy full SHA for 2188cbd

• chore: adjust deprecation warning to be more helpful

  mhuisi

  committed
  49b484c

  Copy full SHA for 49b484c

• feat: lake leanOptions config entry

  mhuisi

  committed
  e676245

  Copy full SHA for e676245

• refactor: arg order

  mhuisi

  committed
  431b054

  Copy full SHA for 431b054

• fix: don't forget the library leanOptions

  mhuisi

  committed
  843721e

  Copy full SHA for 843721e

• doc: missing headers

  mhuisi

  committed
  42065bf

  Copy full SHA for 42065bf

• test: fix new tests with wrong uri

  mhuisi

  committed
  bad3e43

  Copy full SHA for bad3e43

• test: fix new tests with wrong uri

  mhuisi

  committed
  5fbecc3

  Copy full SHA for 5fbecc3

Commits on Nov 24, 2023

• Merge branch 'master' into mhuisi/per-package-server-options

  mhuisi

  committed
  a702c60

  Copy full SHA for a702c60

Commits on Nov 25, 2023

• refactor: post merge cleanup

  mhuisi

  committed
  5508326

  Copy full SHA for 5508326

• refactor: clean up horrible setup-file control flow

  mhuisi

  committed
  ae0aeba

  Copy full SHA for ae0aeba

• Merge remote-tracking branch 'upstream/nightly' into mhuisi/per-package-server-options

  mhuisi

  committed
  1100771

  Copy full SHA for 1100771

• doc: forgot the file header again

  mhuisi

  committed
  e01dee6

  Copy full SHA for e01dee6