Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / leanprover/vscode-lean issues and pull requests

#344 - Elan installation fails on Windows

Issue - State: open - Opened by Timmmm about 2 months ago - 2 comments

#343 - Documentation recourses broken

Issue - State: closed - Opened by fpvandoorn 4 months ago

#342 - Fix link to widgets in mathlib3 documentation

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

#341 - Update display name to reflect version and deprecation

Pull Request - State: closed - Opened by mhuisi 6 months ago

#339 - Update README to reflect that extension is for Lean 3

Pull Request - State: closed - Opened by mhuisi over 1 year ago - 1 comment

#338 - update README to clearly label as for Lean 3

Issue - State: closed - Opened by kim-em over 1 year ago - 1 comment

#337 - Make incomplete proofs more prominent

Issue - State: open - Opened by DanielFabian over 1 year ago - 2 comments

#335 - Trouble setting up: lean.executablePath incorrect

Issue - State: open - Opened by minimario almost 2 years ago

#334 - Add the two-sided abbreviation for <<>>

Pull Request - State: closed - Opened by Julian almost 2 years ago

#333 - Waiting for Lean server to start...

Issue - State: open - Opened by vithar1 almost 2 years ago - 2 comments

#332 - Bump terser from 5.7.0 to 5.16.3

Pull Request - State: open - Opened by dependabot[bot] about 2 years ago
Labels: dependencies

#331 - Bump minimist from 1.2.5 to 1.2.8

Pull Request - State: open - Opened by dependabot[bot] about 2 years ago
Labels: dependencies

#330 - Bump nth-check from 2.0.0 to 2.1.1

Pull Request - State: open - Opened by dependabot[bot] about 2 years ago
Labels: dependencies

#329 - Bump follow-redirects from 1.14.1 to 1.15.2

Pull Request - State: open - Opened by dependabot[bot] about 2 years ago
Labels: dependencies

#328 - Correct the symbol for perpendicular

Pull Request - State: closed - Opened by eric-wieser about 2 years ago - 4 comments

#326 - Bump minimatch from 3.0.4 to 3.1.2

Pull Request - State: open - Opened by dependabot[bot] about 2 years ago
Labels: dependencies

#325 - Bump json5 from 2.1.3 to 2.2.3

Pull Request - State: open - Opened by dependabot[bot] about 2 years ago
Labels: dependencies

#324 - Bump express from 4.17.1 to 4.17.3

Pull Request - State: open - Opened by dependabot[bot] about 2 years ago
Labels: dependencies

#323 - Bump qs and express

Pull Request - State: open - Opened by dependabot[bot] about 2 years ago
Labels: dependencies

#322 - Correct the abbreviation for angle

Pull Request - State: closed - Opened by eric-wieser about 2 years ago

#321 - New API suggestion icon

Pull Request - State: closed - Opened by timlacroix about 2 years ago - 1 comment

#320 - Feature request: highlight proof placeholders ("sorry")

Issue - State: open - Opened by champignoom about 2 years ago

#319 - fix(abbreviations.json): update norm symbol

Pull Request - State: closed - Opened by fpvandoorn over 2 years ago - 3 comments

#318 - Bump loader-utils from 2.0.0 to 2.0.4

Pull Request - State: open - Opened by dependabot[bot] over 2 years ago
Labels: dependencies

#317 - Bump loader-utils from 2.0.0 to 2.0.3

Pull Request - State: closed - Opened by dependabot[bot] over 2 years ago - 1 comment
Labels: dependencies

#316 - Bump underscore and ovsx

Pull Request - State: open - Opened by dependabot[bot] over 2 years ago
Labels: dependencies

#315 - add abbreviations for `‖ ‖` which place the cursor inside

Pull Request - State: closed - Opened by j-loreaux over 2 years ago - 3 comments

#314 - Add suggest API defaults. Add Suggest button / API to README

Pull Request - State: closed - Opened by timlacroix over 2 years ago

#313 - Bump markdown-it, ovsx and vsce

Pull Request - State: open - Opened by dependabot[bot] over 2 years ago
Labels: dependencies

#312 - Proposal for an API based "Suggestions" detail in infoview

Pull Request - State: closed - Opened by timlacroix over 2 years ago - 3 comments

#311 - Do not do manual html escaping of react components

Pull Request - State: closed - Opened by eric-wieser over 2 years ago - 8 comments

#310 - Bump terser from 5.7.0 to 5.14.2

Pull Request - State: closed - Opened by dependabot[bot] over 2 years ago - 1 comment
Labels: dependencies

#309 - Tweak the README now that bracket pair coloring is upstream.

Pull Request - State: closed - Opened by Julian over 2 years ago

#308 - "Try this:" fails on messages with quotation marks

Issue - State: closed - Opened by robertylewis over 2 years ago - 1 comment

#307 - feat(.gitpod): Add gitpod configuration

Pull Request - State: closed - Opened by eric-wieser over 2 years ago

#306 - feat(completion,search): show icons next to symbols

Pull Request - State: closed - Opened by eric-wieser over 2 years ago

#305 - Add support for listing symbols

Pull Request - State: closed - Opened by eric-wieser over 2 years ago - 3 comments

#303 - Fix 'try this' in untitled windows

Pull Request - State: closed - Opened by eric-wieser over 2 years ago

#302 - Add game shortcuts

Pull Request - State: closed - Opened by vihdzp over 2 years ago

#301 - fix: translate between utf16 code unit offsets (vscode) and codepoints (lean)

Pull Request - State: closed - Opened by eric-wieser almost 3 years ago - 1 comment

#300 - Consider using `message.end_pos` in diagnostics

Issue - State: closed - Opened by eric-wieser almost 3 years ago - 2 comments

#299 - Bump nanoid from 3.1.23 to 3.3.4

Pull Request - State: open - Opened by dependabot[bot] almost 3 years ago
Labels: dependencies

#298 - Add weakly covers symbol and opposites shortcuts

Pull Request - State: closed - Opened by YaelDillies almost 3 years ago - 2 comments

#296 - Bump minimist from 1.2.5 to 1.2.6

Pull Request - State: closed - Opened by dependabot[bot] almost 3 years ago - 1 comment
Labels: dependencies

#295 - Bump nanoid from 3.1.23 to 3.3.1

Pull Request - State: closed - Opened by dependabot[bot] almost 3 years ago - 1 comment
Labels: dependencies

#294 - Bump ansi-regex from 5.0.0 to 5.0.1

Pull Request - State: open - Opened by dependabot[bot] almost 3 years ago
Labels: dependencies

#293 - Bump nth-check from 2.0.0 to 2.0.1

Pull Request - State: closed - Opened by dependabot[bot] almost 3 years ago - 1 comment
Labels: dependencies

#292 - fix: some shutdown bugs found in CI testing with the lean3 extension.

Pull Request - State: closed - Opened by lovettchris almost 3 years ago

#290 - Bump follow-redirects from 1.14.1 to 1.14.8

Pull Request - State: closed - Opened by dependabot[bot] about 3 years ago - 1 comment
Labels: dependencies

#289 - Bump ajv from 6.11.0 to 6.12.6

Pull Request - State: open - Opened by dependabot[bot] about 3 years ago
Labels: dependencies

#288 - Shortcuts for `⋖` and `⋗`

Pull Request - State: closed - Opened by YaelDillies about 3 years ago - 4 comments

#287 - Restarting server causes options to be appended again

Issue - State: closed - Opened by alexjbest about 3 years ago

#286 - Add lowercase `\bb` shortcuts

Pull Request - State: closed - Opened by YaelDillies about 3 years ago

#285 - Add `\specializes` → ⤳ abbreviation

Pull Request - State: closed - Opened by erdOne about 3 years ago - 4 comments

#284 - Abbreviations `\/` and `\quot` for `⧸`

Pull Request - State: closed - Opened by Vierkantor about 3 years ago - 1 comment

#283 - Bump axios from 0.21.1 to 0.21.2

Pull Request - State: open - Opened by dependabot[bot] about 3 years ago
Labels: dependencies

#282 - "end" colorized incorrectly

Issue - State: closed - Opened by BoltonBailey over 3 years ago - 3 comments

#281 - Get position

Pull Request - State: open - Opened by javier-m over 3 years ago

#280 - command 'lean.displayGoal' not found

Issue - State: open - Opened by FinalFantasy27 over 3 years ago

#278 - Extract abbreviation part of plugin into own package.

Issue - State: open - Opened by Invisible-Rabbit-Hunter over 3 years ago - 4 comments

#277 - Only open info view for Markdown files in Lean projects

Issue - State: open - Opened by inkytonik over 3 years ago

#276 - fix(syntaxes/lean): `exists` is not a binder if followed by a dot

Pull Request - State: closed - Opened by eric-wieser over 3 years ago - 1 comment

#275 - Hover information for definitions using parameters is misleading

Issue - State: open - Opened by eric-wieser over 3 years ago - 2 comments

#274 - Mardown highlighting in comments consumes closing `-/`

Issue - State: open - Opened by eric-wieser over 3 years ago - 3 comments

#273 - fix(syntaxes/lean): Various grammar fixes

Pull Request - State: closed - Opened by eric-wieser over 3 years ago - 2 comments

#269 - fix(syntaxes/lean): fix some corner cases, add more scopes

Pull Request - State: closed - Opened by eric-wieser over 3 years ago

#268 - feat(syntaxes/lean): add highlighting support for binders

Pull Request - State: closed - Opened by eric-wieser over 3 years ago - 1 comment

#267 - notation for ennreal

Pull Request - State: closed - Opened by sgouezel over 3 years ago

#265 - Correctly highlight lean expressions inside `@[...]` and `attribute […]`

Pull Request - State: closed - Opened by eric-wieser almost 4 years ago - 3 comments

#264 - Check for wrong lean version

Issue - State: open - Opened by jldodds almost 4 years ago

#263 - Do not move the selection if abbreviation substitution fails

Pull Request - State: closed - Opened by eric-wieser almost 4 years ago

#262 - Add four new submenus to the editor context menu

Pull Request - State: closed - Opened by hmonroe almost 4 years ago - 11 comments

#261 - update elan URL

Pull Request - State: closed - Opened by bryangingechen almost 4 years ago

#260 - Quoted Text Coloring

Issue - State: closed - Opened by BoltonBailey almost 4 years ago - 1 comment

#259 - Eager replacement of abbreviations destroys redo history

Issue - State: open - Opened by mhuisi almost 4 years ago - 2 comments

#256 - Only replace unicode input in lean files

Pull Request - State: closed - Opened by hediet about 4 years ago

#255 - Only replace unicode input in lean files

Issue - State: closed - Opened by BoltonBailey about 4 years ago - 1 comment

#254 - Don't replace empty abbreviations

Pull Request - State: closed - Opened by hediet about 4 years ago - 2 comments

#253 - Compatibility with vscode-lean4

Pull Request - State: closed - Opened by mhuisi about 4 years ago - 2 comments

#252 - Is lean 4 supported by the extension?

Issue - State: closed - Opened by Kariiem about 4 years ago - 3 comments

#251 - fix when condition for lean.input.convertWithNewline

Pull Request - State: closed - Opened by bryangingechen about 4 years ago

#250 - Bump axios from 0.19.2 to 0.21.1

Pull Request - State: closed - Opened by dependabot[bot] about 4 years ago
Labels: dependencies

#249 - feat(input): support for ⁅⁆

Pull Request - State: closed - Opened by ocfnash about 4 years ago

#248 - Abbreviations / Unicode-Input Improvement Discussion

Issue - State: open - Opened by hediet about 4 years ago - 2 comments

#246 - Add \^perp and \^bot as input for `ᗮ`, U+15EE

Pull Request - State: closed - Opened by hrmacbeth about 4 years ago - 1 comment

#240 - Rewrite of the abbreviation feature.

Pull Request - State: closed - Opened by hediet about 4 years ago - 12 comments

#239 - Refactoring Of Abbreviation Feature

Issue - State: closed - Opened by hediet about 4 years ago - 10 comments

#234 - Add widget effect support for specifying location of text to insert.

Pull Request - State: closed - Opened by EdAyers over 4 years ago