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

#100 - option to supress variables bound to _, in info view

Issue - State: closed - Opened by ratmice about 6 years ago - 3 comments

#99 - cannot enter unicode symbols in search window

Issue - State: open - Opened by fpvandoorn over 6 years ago

#98 - Custom translations

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

#97 - don't ask to install lean if it's there

Pull Request - State: closed - Opened by bryangingechen over 6 years ago

#96 - Add unicode completions to markdown files.

Pull Request - State: closed - Opened by EdAyers over 6 years ago - 8 comments

#95 - "Install lean using elan" in extra places

Issue - State: closed - Opened by khoek over 6 years ago - 2 comments

#94 - Subscripts don't work

Issue - State: open - Opened by kevinsullivan over 6 years ago - 2 comments

#93 - add command to toggle infoview updating

Pull Request - State: closed - Opened by bryangingechen over 6 years ago

#92 - Infoview goes blank a bit too aggressively

Issue - State: open - Opened by bryangingechen over 6 years ago

#91 - feat: offer to install missing Lean using elan

Pull Request - State: closed - Opened by kim-em over 6 years ago - 5 comments

#90 - [WIP] TM scopes for brackets

Pull Request - State: closed - Opened by bryangingechen over 6 years ago - 1 comment

#89 - Auto-closing for unicode pairs such as ⟨ ⟩ etc.

Issue - State: closed - Opened by luxbock over 6 years ago - 1 comment

#88 - fix comment highlighting bug: -- disabling -/

Pull Request - State: closed - Opened by bryangingechen over 6 years ago

#87 - fix two syntax highlighting examples from zulip

Pull Request - State: closed - Opened by bryangingechen over 6 years ago - 2 comments

#86 - Add syntax highlighting for λ

Pull Request - State: closed - Opened by luxbock over 6 years ago

#85 - fix(translations.json): Make \func available for functors in categories

Pull Request - State: closed - Opened by jcommelin over 6 years ago

#84 - coloring after "#print definition"

Issue - State: closed - Opened by bryangingechen over 6 years ago - 1 comment

#82 - comments after imports not being colored properly

Issue - State: closed - Opened by bryangingechen over 6 years ago - 1 comment

#79 - v0.11.11 causes VS code to stall endlessly when opening a lean file

Issue - State: closed - Opened by evhub over 6 years ago - 8 comments

#78 - Spurious errors in comment blocks

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

#77 - ctrl+shift+enter opens current file on the side

Issue - State: closed - Opened by gebner over 6 years ago - 5 comments

#76 - Spurious "command expected" errors

Issue - State: closed - Opened by kevinsullivan over 6 years ago - 1 comment

#75 - How can I run Lean on vscode?

Issue - State: closed - Opened by HenriqueMartinsBotelho over 6 years ago

#74 - adding unicode Mathematical Alphanumeric Symbols

Pull Request - State: closed - Opened by kim-em over 6 years ago - 5 comments

#73 - lean.executablePath may be incorrect

Issue - State: closed - Opened by yotamDvir almost 7 years ago - 2 comments

#72 - Command failed: lean --version /bin/sh:1 lean: not found

Issue - State: closed - Opened by shingtaklam1324 almost 7 years ago - 1 comment

#71 - Support new proposed visible ranges API

Issue - State: closed - Opened by gebner almost 7 years ago

#70 - command 'lean.roiMode.cursor' not found

Issue - State: open - Opened by aqjune about 7 years ago - 2 comments

#69 - README: enhance windows instructions

Pull Request - State: closed - Opened by fpvandoorn about 7 years ago

#68 - ctrl-space autocompletion might fail the first time

Issue - State: open - Opened by kbuzzard over 7 years ago

#67 - cannot go to definition at the end of definition

Issue - State: open - Opened by fpvandoorn over 7 years ago

#66 - "leanpkg.path changed", even when it is merely touched

Issue - State: closed - Opened by kim-em over 7 years ago

#65 - lean doesn't work for me in vscode on windows

Issue - State: closed - Opened by fpvandoorn over 7 years ago - 2 comments

#64 - Configuration for stack size

Issue - State: closed - Opened by jldodds over 7 years ago - 2 comments

#63 - Support multi-root workspaces

Issue - State: open - Opened by gebner over 7 years ago

#62 - Automatically restart server when leanpkg.path changes

Issue - State: closed - Opened by gebner over 7 years ago
Labels: enhancement

#61 - Info view updates too agressively

Issue - State: open - Opened by jldodds over 7 years ago

#60 - Certain Keywords Not Highlighted

Issue - State: closed - Opened by OwenGraves over 7 years ago - 1 comment

#59 - fix(syntaxes): remove old keywords "take" and "suppose"

Pull Request - State: closed - Opened by johoelzl over 7 years ago

#57 - lean syntax: add coinductive, remove duplicated mutual, remove override

Pull Request - State: closed - Opened by johoelzl over 7 years ago

#56 - mutual keyword syntax highlighting

Issue - State: closed - Opened by joshpoll over 7 years ago

#55 - infoview: mark current messages (to be used by CSS); reload css on configuration change

Pull Request - State: closed - Opened by johoelzl over 7 years ago - 2 comments

#54 - Add explicit pause/continue button in infoview; remove underlines from links

Pull Request - State: closed - Opened by johoelzl over 7 years ago - 1 comment

#53 - Set source in diagnostics: goto erro shows multiline errors

Pull Request - State: closed - Opened by johoelzl over 7 years ago - 1 comment

#52 - region processing bug

Issue - State: closed - Opened by leodemoura over 7 years ago

#51 - fix(package.json): only show commands acting on Lean files when a Lea…

Pull Request - State: closed - Opened by johoelzl over 7 years ago

#50 - RFC: Use previewHtml for Lean's Info View

Pull Request - State: closed - Opened by johoelzl over 7 years ago - 20 comments

#49 - confusing response to check open files

Issue - State: closed - Opened by cartazio over 7 years ago - 1 comment

#48 - Too many sorry warnings cause printing to stop

Issue - State: open - Opened by digama0 over 7 years ago - 4 comments

#47 - Suppress sorry warnings in info view

Issue - State: open - Opened by gebner over 7 years ago - 1 comment

#46 - Cannot type ⦄ using unicode input

Issue - State: closed - Opened by gebner over 7 years ago - 4 comments

#45 - hide _target directory

Issue - State: closed - Opened by kim-em almost 8 years ago - 2 comments

#44 - ' should not close unless it is preceded by whitespace

Issue - State: closed - Opened by jldodds almost 8 years ago

#43 - Path injection is broken on windows

Issue - State: open - Opened by gebner almost 8 years ago

#42 - Restart server with currently set executable path

Issue - State: closed - Opened by gebner almost 8 years ago

#41 - Use lean-client-js.

Pull Request - State: closed - Opened by gebner almost 8 years ago - 2 comments

#39 - Parsing status messages have disappeared

Issue - State: closed - Opened by kim-em almost 8 years ago - 2 comments

#38 - Checking visible files and checking open files has the same behaviour.

Issue - State: closed - Opened by kim-em almost 8 years ago - 1 comment

#37 - Refactor extension.ts into smaller files

Issue - State: closed - Opened by jroesch almost 8 years ago

#36 - Setting to always start in "checking open files" mode.

Issue - State: closed - Opened by kim-em almost 8 years ago - 1 comment

#35 - Recognize ⟨ ⟩ as matching brackets

Issue - State: closed - Opened by digama0 almost 8 years ago - 1 comment

#34 - #eval output only highlights the #

Issue - State: closed - Opened by digama0 almost 8 years ago - 4 comments

#33 - Fix grammar to support new transient commands and command aliases

Issue - State: closed - Opened by jroesch almost 8 years ago - 1 comment

#32 - Automatic Display goal

Issue - State: closed - Opened by jldodds almost 8 years ago - 1 comment

#31 - request: capturing the cause of the Lean server stopping

Issue - State: closed - Opened by kim-em almost 8 years ago - 2 comments

#30 - If timeLimit is set to too large a number, it is silently ignored.

Issue - State: closed - Opened by kim-em almost 8 years ago

#29 - Spurious error: Could not resolve Import

Issue - State: closed - Opened by kevinsullivan almost 8 years ago

#28 - Extension seems to ignore lean.executablePath option

Issue - State: closed - Opened by vitaliyparinov almost 8 years ago - 2 comments

#27 - Use proper semver library for comparing versions

Issue - State: closed - Opened by jroesch almost 8 years ago

#26 - Fix language-configuration.json

Pull Request - State: closed - Opened by gebner about 8 years ago - 1 comment

#25 - Set the wordPattern in the language configuration

Pull Request - State: closed - Opened by emberian about 8 years ago

#24 - Lean sometimes tries processing git diffs.

Issue - State: closed - Opened by kim-em about 8 years ago - 2 comments

#23 - Add support for new goal mode

Issue - State: closed - Opened by jroesch about 8 years ago - 1 comment

#22 - Add configuration option for setting Lean flags

Issue - State: closed - Opened by jroesch about 8 years ago - 2 comments

#21 - Display server startup errors

Pull Request - State: closed - Opened by Kha about 8 years ago

#20 - hover: Show docs when available

Pull Request - State: closed - Opened by Kha about 8 years ago

#19 - Open Lean.exe on Windows

Issue - State: closed - Opened by jroesch about 8 years ago - 1 comment

#18 - Add more documentation

Issue - State: closed - Opened by jroesch about 8 years ago

#17 - Stuff!

Pull Request - State: closed - Opened by Kha about 8 years ago

#16 - Let executablePath default to "lean"

Pull Request - State: closed - Opened by Kha about 8 years ago - 3 comments

#15 - Weird files when using vscode's git interface

Issue - State: closed - Opened by gebner about 8 years ago - 2 comments

#14 - Lean executable in PATH is not found

Issue - State: closed - Opened by gebner about 8 years ago - 1 comment

#13 - Sync file that are already open

Pull Request - State: closed - Opened by Kha about 8 years ago

#12 - Completions should only contain names, not input assist

Issue - State: closed - Opened by jroesch about 8 years ago - 1 comment

#11 - Misc

Pull Request - State: closed - Opened by Kha about 8 years ago

#10 - Update to new autocompletion protocol.

Pull Request - State: closed - Opened by gebner about 8 years ago

#9 - autocomplete after `import `

Issue - State: closed - Opened by diakopter about 8 years ago - 2 comments

#8 - autocomplete doesn't have keywords

Issue - State: closed - Opened by diakopter about 8 years ago - 2 comments

#7 - Replace input-assist extension by a simpler built-in version.

Pull Request - State: closed - Opened by gebner about 8 years ago

#6 - Ensure the server is restarted after crash

Issue - State: closed - Opened by jroesch about 8 years ago - 1 comment

#5 - Add "batch" command

Issue - State: closed - Opened by jroesch about 8 years ago

#4 - Fix crash when using explicit exe path

Pull Request - State: closed - Opened by Kha about 8 years ago

#3 - Files are not synced when reopening a directory

Issue - State: closed - Opened by gebner about 8 years ago - 1 comment

#2 - Number of "Lean: Proof Context" output channels increases steadily

Issue - State: closed - Opened by gebner about 8 years ago - 3 comments

#1 - Figure out (or document) a good way to ignore olean files

Issue - State: closed - Opened by gebner about 8 years ago - 4 comments