Ecosyste.ms: Issues

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

GitHub / leanprover/verso issues and pull requests

#100 - chore: bump to latest nightly toolchain

Pull Request - State: closed - Opened by david-christiansen 6 months ago

#100 - chore: bump to latest nightly toolchain

Pull Request - State: closed - Opened by david-christiansen 6 months ago

#99 - Add missing word

Pull Request - State: closed - Opened by david-christiansen 6 months ago

#99 - Add missing word

Pull Request - State: closed - Opened by david-christiansen 6 months ago

#98 - Small typo in README

Issue - State: closed - Opened by chenson2018 6 months ago - 1 comment

#98 - Small typo in README

Issue - State: closed - Opened by chenson2018 6 months ago - 1 comment

#96 - Reduce size of generated HTML

Issue - State: closed - Opened by david-christiansen 7 months ago - 1 comment

#96 - Reduce size of generated HTML

Issue - State: closed - Opened by david-christiansen 7 months ago - 1 comment

#95 - chore: bump Subverso for proof states after by and =>

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#95 - chore: bump Subverso for proof states after by and =>

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#94 - feat: add support for signatures, highlighted & checked

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#94 - feat: add support for signatures, highlighted & checked

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#93 - feat: flexible whitespace matching in blog genre

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#93 - feat: flexible whitespace matching in blog genre

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#92 - feat: support name references in subprojects

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#92 - feat: support name references in subprojects

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#91 - chore: bump subverso

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#91 - chore: bump subverso

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#89 - chore: use memoir for LaTeX output

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#89 - chore: use memoir for LaTeX output

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#88 - feat: code exercises in example textbook

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#88 - feat: code exercises in example textbook

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#87 - feat: add an example of a minimal genre

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#87 - feat: add an example of a minimal genre

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#86 - chore: bump SubVerso for round-trip JSON fix (#19)

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#86 - chore: bump SubVerso for round-trip JSON fix (#19)

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#85 - feat: example textbook

Pull Request - State: closed - Opened by david-christiansen 7 months ago - 1 comment

#85 - feat: example textbook

Pull Request - State: closed - Opened by david-christiansen 7 months ago - 1 comment

#84 - test: bump subverso

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#84 - test: bump subverso

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#83 - test: bump subverso

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#83 - test: bump subverso

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#82 - Check in CI that there's no `import Lean` checked in

Issue - State: closed - Opened by david-christiansen 7 months ago - 1 comment

#81 - chore: bump subverso

Pull Request - State: closed - Opened by david-christiansen 7 months ago

#80 - leanOutput Code action removes a `

Issue - State: open - Opened by nomeata 8 months ago

#80 - leanOutput Code action removes a `

Issue - State: open - Opened by nomeata 8 months ago

#79 - fix: stack info hovers in a single window

Pull Request - State: closed - Opened by david-christiansen 8 months ago

#79 - fix: stack info hovers in a single window

Pull Request - State: closed - Opened by david-christiansen 8 months ago

#78 - feat: incremental elaboration of Verso documents

Pull Request - State: closed - Opened by david-christiansen 8 months ago - 3 comments

#78 - feat: incremental elaboration of Verso documents

Pull Request - State: closed - Opened by david-christiansen 8 months ago - 3 comments

#76 - multi-lang support

Issue - State: open - Opened by Seasawher 8 months ago - 2 comments

#76 - multi-lang support

Issue - State: open - Opened by Seasawher 8 months ago - 2 comments

#75 - chore: work with newer Lean core

Pull Request - State: closed - Opened by david-christiansen 8 months ago

#75 - chore: work with newer Lean core

Pull Request - State: closed - Opened by david-christiansen 8 months ago

#74 - Add an example of a minimal genre

Issue - State: closed - Opened by david-christiansen 8 months ago - 1 comment

#74 - Add an example of a minimal genre

Issue - State: closed - Opened by david-christiansen 8 months ago - 1 comment

#73 - feat: basic inclusion of docstrings in manuals

Pull Request - State: closed - Opened by david-christiansen 8 months ago

#73 - feat: basic inclusion of docstrings in manuals

Pull Request - State: closed - Opened by david-christiansen 8 months ago

#71 - Missing \hyperlink in LaTeX

Issue - State: closed - Opened by david-christiansen 8 months ago

#71 - Missing \hyperlink in LaTeX

Issue - State: closed - Opened by david-christiansen 8 months ago

#70 - Confusing error message with include

Issue - State: open - Opened by PatrickMassot 8 months ago

#70 - Confusing error message with include

Issue - State: open - Opened by PatrickMassot 8 months ago

#69 - Parser doesn't say "expected" always

Issue - State: open - Opened by david-christiansen 8 months ago

#69 - Parser doesn't say "expected" always

Issue - State: open - Opened by david-christiansen 8 months ago

#68 - Go-to-def for {include A.B.C}

Issue - State: open - Opened by david-christiansen 8 months ago

#68 - Go-to-def for {include A.B.C}

Issue - State: open - Opened by david-christiansen 8 months ago

#67 - Manual genre: multiple author rendering

Issue - State: open - Opened by david-christiansen 8 months ago

#67 - Manual genre: multiple author rendering

Issue - State: open - Opened by david-christiansen 8 months ago

#66 - toggle displaying information

Issue - State: open - Opened by Seasawher 8 months ago - 1 comment

#66 - toggle displaying information

Issue - State: open - Opened by Seasawher 8 months ago - 1 comment

#65 - fix: CSS - make hover boxes fit their content

Pull Request - State: closed - Opened by david-christiansen 8 months ago

#65 - fix: CSS - make hover boxes fit their content

Pull Request - State: closed - Opened by david-christiansen 8 months ago

#64 - Library root file and housekeeping

Pull Request - State: closed - Opened by david-christiansen 8 months ago

#64 - Library root file and housekeeping

Pull Request - State: closed - Opened by david-christiansen 8 months ago

#63 - doc: point README at both renderings of the manual

Pull Request - State: closed - Opened by david-christiansen 8 months ago

#63 - doc: point README at both renderings of the manual

Pull Request - State: closed - Opened by david-christiansen 8 months ago

#61 - fix: upload all generated docs to one release/artifact

Pull Request - State: closed - Opened by david-christiansen 8 months ago

#61 - fix: upload all generated docs to one release/artifact

Pull Request - State: closed - Opened by david-christiansen 8 months ago

#60 - chore: bump subverso version

Pull Request - State: closed - Opened by david-christiansen 8 months ago

#60 - chore: bump subverso version

Pull Request - State: closed - Opened by david-christiansen 8 months ago

#58 - chore: bump subverso for fix to whitespace tokens

Pull Request - State: closed - Opened by david-christiansen 8 months ago

#58 - chore: bump subverso for fix to whitespace tokens

Pull Request - State: closed - Opened by david-christiansen 8 months ago

#56 - feat: manually highlight keywords

Pull Request - State: closed - Opened by david-christiansen 9 months ago

#56 - feat: manually highlight keywords

Pull Request - State: closed - Opened by david-christiansen 9 months ago

#55 - Blog usability

Pull Request - State: closed - Opened by david-christiansen 9 months ago

#55 - Blog usability

Pull Request - State: closed - Opened by david-christiansen 9 months ago

#54 - Support for multiline math formulas

Issue - State: open - Opened by utensil 9 months ago - 7 comments

#54 - Support for multiline math formulas

Issue - State: open - Opened by utensil 9 months ago - 7 comments

#52 - fix: minor highlighting issue for info display

Pull Request - State: closed - Opened by david-christiansen 9 months ago

#52 - fix: minor highlighting issue for info display

Pull Request - State: closed - Opened by david-christiansen 9 months ago

#50 - feat: code examples from separate Lean package

Pull Request - State: closed - Opened by david-christiansen 9 months ago

#50 - feat: code examples from separate Lean package

Pull Request - State: closed - Opened by david-christiansen 9 months ago