ejgallego/coq-lsp issues and pull requests

#856 - Goto definition doesn't work for record constructors

Issue - State: open - Opened by Alizter about 2 months ago
Labels: kind: bug, part: lsp server

#855 - Adapt to coq/coq#19646 (wit_binders and wit_withtac are vernac arguments)

Pull Request - State: open - Opened by SkySkimmer about 2 months ago
Labels: kind: upstream, part: serlib

#854 - Syntax highlighting

Issue - State: open - Opened by Alizter about 2 months ago - 1 comment
Labels: kind: bug, part: client (VSCode)

#853 - [fleche] fix quick fixes for errors being lost

Pull Request - State: closed - Opened by ejgallego about 2 months ago
Labels: kind: fix, needs: test-case, part: flèche

#852 - [web worker] Package manager

Issue - State: open - Opened by ejgallego about 2 months ago
Labels: kind: enhancement, part: web worker

#851 - [web worker] Add progress bar for worker download

Issue - State: open - Opened by ejgallego about 2 months ago
Labels: kind: enhancement, part: web worker

#850 - [web worker] Allow users to select different Coq versions

Issue - State: open - Opened by ejgallego about 2 months ago
Labels: kind: enhancement, part: web worker

#849 - [vscode] Expand selectors to include `vscode-vfs://` URIs

Pull Request - State: closed - Opened by ejgallego about 2 months ago
Labels: kind: enhancement, part: client (VSCode), kind: fix, part: web worker

#848 - [meta] Release 0.2.1

Pull Request - State: closed - Opened by ejgallego about 2 months ago
Labels: part: documentation, kind: meta

#847 - [petanque] Fix bug for detection of proof finished in deep stacks

Pull Request - State: closed - Opened by ejgallego about 2 months ago
Labels: kind: fix, part: petanque

#846 - [faq] Update FAQ for VsCoq 2 release.

Pull Request - State: open - Opened by ejgallego about 2 months ago - 4 comments
Labels: kind: enhancement, kind: fix, part: documentation

#845 - [coq] Abstract the feedback / error payloads better.

Pull Request - State: closed - Opened by ejgallego about 2 months ago
Labels: kind: cleanup, kind: internal, part: Coq API

#844 - Nits refactor fleche

Pull Request - State: closed - Opened by ejgallego 2 months ago
Labels: kind: cleanup, kind: internal, part: flèche

#843 - [lang] Move `Lang.Diagnostics.Data.t` from a list to name field

Pull Request - State: closed - Opened by ejgallego 2 months ago
Labels: part: lsp server, part: protocol (custom), kind: cleanup, kind: redesign, part: flèche

#842 - [ci] [worker] Make the build flexible for non-vendored setups.

Pull Request - State: closed - Opened by ejgallego 2 months ago
Labels: part: CI, kind: internal

#841 - [fleche] New immediate request serving mode.

Pull Request - State: closed - Opened by ejgallego 2 months ago
Labels: kind: enhancement, part: protocol (LSP), kind: redesign, part: flèche

#841 - [fleche] New immediate request serving mode.

Pull Request - State: closed - Opened by ejgallego 2 months ago
Labels: kind: enhancement, part: protocol (LSP), kind: redesign, part: flèche

#840 - Code Actions

Pull Request - State: closed - Opened by ejgallego 2 months ago
Labels: kind: enhancement, part: lsp server, part: protocol (LSP), kind: upstream, kind: HCI design, part: upstream, part: Coq API

#839 - [hover] Fix universe printing in hover.

Pull Request - State: closed - Opened by ejgallego 2 months ago - 2 comments
Labels: kind: fix, lsp: hover, part: upstream

#839 - [hover] Fix universe printing in hover.

Pull Request - State: closed - Opened by ejgallego 2 months ago - 2 comments
Labels: kind: fix, lsp: hover, part: upstream

#838 - [coq] [init] Allow init to tweak VM mode and warnings.

Pull Request - State: closed - Opened by ejgallego 2 months ago
Labels: kind: enhancement, kind: internal, part: Coq API

#837 - [args] [coq] Allow to set ocamlpath and findlib init file separately.

Pull Request - State: closed - Opened by ejgallego 2 months ago
Labels: kind: internal, part: Coq API

#837 - [args] [coq] Allow to set ocamlpath and findlib init file separately.

Pull Request - State: closed - Opened by ejgallego 2 months ago
Labels: kind: internal, part: Coq API

#836 - Show Proof window

Issue - State: open - Opened by Alizter 2 months ago - 2 comments
Labels: kind: enhancement

#835 - Unvierse levels displayed as de bruijin indices in hover

Issue - State: closed - Opened by Alizter 2 months ago - 3 comments
Labels: kind: bug, lsp: hover

#835 - Unvierse levels displayed as de bruijin indices in hover

Issue - State: closed - Opened by Alizter 2 months ago - 3 comments
Labels: kind: bug, lsp: hover

#834 - Utils.with_control use VernacControl (adapt to coq/coq#19517 adding a control flag)

Pull Request - State: closed - Opened by SkySkimmer 2 months ago - 1 comment
Labels: kind: fix, kind: upstream, kind: cleanup, kind: upstream-bug, part: upstream, part: Coq API

#833 - JS Worker Meta Issue

Issue - State: open - Opened by ejgallego 2 months ago
Labels: kind: meta

#832 - [fleche] Highlight the full first line of the document on initialization error.

Pull Request - State: closed - Opened by ejgallego 2 months ago
Labels: kind: enhancement, kind: HCI design, part: flèche

#831 - [nits] Minor refactorings and tweaks from the JS branch.

Pull Request - State: closed - Opened by ejgallego 2 months ago
Labels: part: lsp server, kind: cleanup, kind: internal

#830 - [vendor] [deps] bump Coq

Pull Request - State: closed - Opened by ejgallego 2 months ago
Labels: part: deps, kind: upstream, kind: internal, part: upstream

#829 - [plugins] Example for error explaining plugin.

Pull Request - State: closed - Opened by ejgallego 2 months ago - 1 comment
Labels: kind: enhancement, part: compiler, part: plugins

#828 - [coq] [fleche] Support `Restart` command.

Pull Request - State: closed - Opened by ejgallego 2 months ago
Labels: kind: enhancement, kind: fix, part: flèche, part: Coq API

#827 - Errors: Restart cannot be used through the Load command;

Issue - State: closed - Opened by Alizter 2 months ago - 9 comments
Labels: kind: bug, part: flèche, part: Coq API

#826 - Adapt to coq/coq#19575 (ltac2 parsing uses attributes)

Pull Request - State: closed - Opened by SkySkimmer 2 months ago - 1 comment
Labels: kind: upstream, part: upstream

#825 - [coq] Understand rewrite rules and symbols on document outline

Pull Request - State: closed - Opened by ejgallego 2 months ago
Labels: kind: enhancement, part: lsp server, part: protocol (LSP), part: Coq API

#824 - Rewrite rule symbols not appearing in document outline

Issue - State: closed - Opened by Alizter 2 months ago - 4 comments
Labels: kind: bug, part: protocol (LSP), part: Coq API

#823 - [goals] Allow `command` to process several Coq commands.

Pull Request - State: closed - Opened by ejgallego 2 months ago - 2 comments
Labels: kind: enhancement, kind: internal, lsp: goals, part: flèche

#822 - Adapt to https://github.com/coq/coq/pull/19530

Pull Request - State: open - Opened by proux01 2 months ago - 28 comments

#821 - [serlib] Fix wrong piercing of Ltac2 AST + test case

Pull Request - State: closed - Opened by ejgallego 2 months ago
Labels: kind: fix, kind: upstream, kind: upstream-bug, part: upstream, part: serlib

#820 - [serlib] Support for ltac2_ltac1 plugin

Pull Request - State: closed - Opened by ejgallego 2 months ago
Labels: kind: enhancement, part: serlib

#819 - [workspace] [coq] Support _CoqProject arguments `-type-in-type` and `allow-rewrite-rules` (for 8.20)

Pull Request - State: closed - Opened by ejgallego 3 months ago
Labels: kind: bug, kind: enhancement, kind: fix, kind: upstream, part: workspace setup, part: config

#818 - Nix build error (unable to find coq-core plugins)

Issue - State: closed - Opened by BenjaminCB 3 months ago - 4 comments
Labels: kind: bug

#817 - Clarify the difference between VsCoq 1 and VsCoq 2 here?

Issue - State: open - Opened by patrick-nicodemus 3 months ago - 1 comment
Labels: kind: bug, part: documentation

#816 - Document outline doesn't work with on-demand checking

Issue - State: open - Opened by Alizter 3 months ago - 1 comment
Labels: kind: bug

#815 - [ci] [windows] Try OPAM 2.2 for the Windows build

Pull Request - State: open - Opened by ejgallego 3 months ago
Labels: kind: enhancement, kind: cleanup, part: CI, needs: merge of dependency, platform: windows

#814 - [nix] [build] Update flake to more modern ppx packages.

Pull Request - State: closed - Opened by ejgallego 3 months ago
Labels: part: deps, kind: internal, os: nix

#813 - [build] [deps] Bump ppxlib toolchain to 0.26.0.

Pull Request - State: closed - Opened by ejgallego 3 months ago - 1 comment
Labels: part: build, part: deps, kind: cleanup, kind: internal, part: ocaml

#812 - [meta] Release 0.2.0

Pull Request - State: closed - Opened by ejgallego 3 months ago
Labels: part: packaging, kind: meta

#811 - [vendor] Bump Coq.

Pull Request - State: closed - Opened by ejgallego 3 months ago
Labels: part: deps, kind: internal, part: upstream

#809 - Adapt to https://github.com/coq/coq/pull/19310

Pull Request - State: closed - Opened by proux01 4 months ago - 2 comments
Labels: kind: upstream, part: upstream

#799 - [plugins] Baseline plugin for `fcc`

Pull Request - State: open - Opened by ejgallego 5 months ago

#797 - Universe information

Issue - State: open - Opened by Alizter 5 months ago - 3 comments
Labels: kind: enhancement

#790 - [petanque] Allow clients to set file contents

Pull Request - State: open - Opened by ejgallego 6 months ago

#785 - [tools] Checkdecls tool for Coq blueprints

Pull Request - State: open - Opened by ejgallego 6 months ago

#776 - [doc] Some tweaks to PROTOCOL.md documentation.

Pull Request - State: closed - Opened by ejgallego 6 months ago
Labels: kind: enhancement, part: documentation

#761 - [upstream] Automating the registration of serializers for generic arguments

Issue - State: open - Opened by ejgallego about 6 years ago
Labels: kind: upstream

#759 - [serlib] Explore ppx_override

Issue - State: open - Opened by ejgallego about 3 years ago

#678 - Restarting server resets position of goal window

Issue - State: open - Opened by Alizter 8 months ago - 2 comments
Labels: kind: bug, part: goals and info panel

#668 - [layout engine] Move Coq Layout engine tree to coq-lsp repos.

Pull Request - State: open - Opened by ejgallego 8 months ago

#641 - [wip] File auto-build

Pull Request - State: open - Opened by ejgallego 11 months ago - 1 comment
Labels: kind: enhancement, needs: test-case, part: workspace setup, needs: testing, part: compiler, part: flèche

#632 - Ltac, Notation and Tactic Notation doesn't appear in the document overview

Issue - State: open - Opened by Alizter 11 months ago - 1 comment
Labels: kind: bug

#628 - [meta] CoqPilot support issue

Issue - State: open - Opened by ejgallego 12 months ago
Labels: kind: meta

#626 - [example] Example how to use the LSP client

Pull Request - State: open - Opened by ejgallego about 1 year ago

#590 - [hover] [wip] First prototype of show documentation on hover

Pull Request - State: open - Opened by ejgallego about 1 year ago - 2 comments

#546 - [workspace] Workspace determination code works not well with relative paths

Issue - State: open - Opened by ejgallego about 1 year ago
Labels: kind: bug, part: workspace setup

#514 - [build] Ensure isolation of Yojson wrt to Flèche

Issue - State: open - Opened by ejgallego over 1 year ago
Labels: kind: bug

#505 - [workspace] Include list of known modules in workspace.

Pull Request - State: open - Opened by ejgallego over 1 year ago
Labels: kind: enhancement, part: lsp server, part: workspace setup

#433 - [controller] [js] Initial javascript JSSO controller

Pull Request - State: closed - Opened by ejgallego almost 2 years ago
Labels: kind: enhancement, part: build, part: client (VSCode), part: lsp server, part: CI, needs: changes entry, part: web worker

#353 - Feature request: split comments, not just code

Issue - State: open - Opened by cpitclaudel over 4 years ago - 17 comments
Labels: kind: enhancement

#333 - Querying module definitions

Issue - State: open - Opened by dkhalansky over 5 years ago - 1 comment

#332 - Tracking relationships between goals

Issue - State: open - Opened by cpitclaudel about 3 years ago - 10 comments
Labels: kind: enhancement

#331 - Print a sentence with the notation interpretation, scope resolution, and explicit arguments

Issue - State: open - Opened by darbyhaller over 5 years ago - 3 comments
Labels: kind: enhancement, kind: upstream

#330 - Accessing fully qualified names when printing (for hyperlinking support in Alectryon)

Issue - State: closed - Opened by cpitclaudel over 4 years ago - 15 comments
Labels: kind: enhancement

#328 - TypeOf only gives the type of identifiers, not of expressions.

Issue - State: open - Opened by darbyhaller about 5 years ago - 3 comments
Labels: kind: enhancement

#327 - [query] Support querying dependency data

Issue - State: open - Opened by ejgallego almost 6 years ago - 8 comments
Labels: kind: enhancement

#326 - Add a query to perform a diff of terms

Issue - State: open - Opened by elidupree almost 4 years ago - 6 comments

#325 - Structured view of Coq documents

Issue - State: closed - Opened by ejgallego about 3 years ago - 1 comment

#324 - [protocol] Add `Search` support.

Issue - State: open - Opened by ejgallego over 6 years ago - 17 comments

#267 - [request queue] Improvements on request queuing.

Issue - State: open - Opened by ejgallego almost 2 years ago
Labels: part: protocol (LSP)

#233 - [server] [build] Worker versions

Issue - State: closed - Opened by ejgallego almost 2 years ago

#201 - Loc-independent cache behavior may be strange in some cases.

Issue - State: open - Opened by ejgallego almost 2 years ago - 1 comment

#123 - [code] Workspace panel

Issue - State: open - Opened by ejgallego almost 2 years ago - 3 comments
Labels: kind: HCI design

#88 - [serlib] Bump upstream version

Issue - State: closed - Opened by ejgallego almost 2 years ago - 1 comment
Labels: part: deps

#87 - [lsp] Implement LSP client-side logging, don't crash on log file creation

Pull Request - State: closed - Opened by ejgallego almost 2 years ago
Labels: part: client (VSCode), part: lsp server, part: protocol (LSP)

#86 - VSCode client does not start

Issue - State: closed - Opened by Alizter about 2 years ago - 1 comment

#85 - doc: Detail Nix usage in README.md

Pull Request - State: closed - Opened by Alizter about 2 years ago - 1 comment
Labels: part: documentation

#84 - chore(ci): add result/ to .gitignore

Pull Request - State: closed - Opened by Alizter about 2 years ago
Labels: part: CI

#83 - chore(ci): cancel previous workflow runs

Pull Request - State: closed - Opened by Alizter about 2 years ago
Labels: part: CI

#82 - chore(ci): add Nix to CI

Pull Request - State: closed - Opened by Alizter about 2 years ago - 6 comments

#81 - chore: Nix detects .ocamlformat version + CI fmt uses Nix

Pull Request - State: closed - Opened by Alizter about 2 years ago - 1 comment
Labels: part: CI

#80 - [makefile] add submodules-deinit target

Pull Request - State: closed - Opened by Alizter about 2 years ago
Labels: part: build

#79 - [goal panel] (Hacky) fix for panel lifetime

Pull Request - State: closed - Opened by ejgallego about 2 years ago
Labels: part: client (VSCode)

#78 - [goals] Show the goal _before_ running the tactic at point

Pull Request - State: closed - Opened by ejgallego about 2 years ago
Labels: kind: enhancement, part: lsp server

#77 - [goal] Fix goal printing to happen in the right state.

Pull Request - State: closed - Opened by ejgallego about 2 years ago
Labels: part: lsp server, kind: fix

#76 - [fleche] [controller] First steps towards resumption

Pull Request - State: closed - Opened by ejgallego about 2 years ago
Labels: kind: enhancement, part: lsp server

#75 - Windows support

Issue - State: closed - Opened by ejgallego about 2 years ago - 1 comment
Labels: kind: enhancement, part: lsp server, platform: windows

#74 - [hover] [lsp] Don't show goals on hover.

Pull Request - State: closed - Opened by ejgallego about 2 years ago
Labels: part: lsp server

#73 - [coq] Bump to Coq mainline, make it compile with unpatched Coq master

Pull Request - State: closed - Opened by ejgallego about 2 years ago
Labels: part: build

#72 - [roadmap] coq-layout-engine general issue

Issue - State: open - Opened by ejgallego about 2 years ago
Labels: kind: meta

GitHub / ejgallego/coq-lsp issues and pull requests