List view

• 5. Features and Bugs

  No due date

  •0/12 issues closed
  0% complete12 open0 closed

• 4. Breaking: Support both Eglot and lsp-mode

  We need to remove the hard dependency on lsp-mode. Ideally, end-users should be able to choose between both lsp-mode and Eglot. The removal of the hard dependency on lsp-mode allows us to distribute lean4-mode on the Melpa package-archive.

  No due date

  •0/4 issues closed
  0% complete4 open0 closed

• 3. Breaking: Refactor

  We need to deeply refactor Lean4-Mode. Some files can be dissolved/merged and others deleted. We might rework the abbreviations workflow. We add a common prefix to all files and symbols. We will introduce breaking changes.

  No due date

  •1/4 issues closed
  25% complete3 open1 closed