Ecosyste.ms: Issues

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

GitHub / idris-lang/Idris2 issues and pull requests

#3391 - Girards Paradox copied from Agda

Issue - State: open - Opened by yokto about 13 hours ago

#3390 - Type checker silently stuck on missing import.

Issue - State: closed - Opened by yellowsquid about 20 hours ago - 2 comments
Labels: status: expected behaviour, language: import, scope: public, scope: private

#3388 - [ doc ] Update gambit docs

Pull Request - State: open - Opened by dunhamsteve 4 days ago

#3387 - A plea for improved Gambit support for bare metal

Issue - State: open - Opened by flintwinters 5 days ago - 6 comments
Labels: Feature request

#3386 - Handle multiline comments in Package (ipkg)

Pull Request - State: open - Opened by stephen-smith 6 days ago - 2 comments

#3384 - Correct ipkg comment docs

Pull Request - State: closed - Opened by stephen-smith 7 days ago - 1 comment
Labels: documentation, status: confirmed bug

#3383 - Unlawful `Monad` implementation for `Stream`

Issue - State: closed - Opened by gallais 8 days ago - 1 comment
Labels: status: invalid, library: base

#3382 - include hidden files in artifact

Pull Request - State: closed - Opened by mattpolzin 10 days ago

#3381 - [ new ] Support for dumping a package's install location

Pull Request - State: closed - Opened by mattpolzin 10 days ago - 2 comments

#3380 - [ base ] Add atomically function

Pull Request - State: closed - Opened by Matthew-Mosior 15 days ago - 8 comments

#3379 - Can't solve constraint between: or' z False and or' z False

Issue - State: closed - Opened by johannes-riecken 16 days ago - 3 comments
Labels: status: invalid

#3377 - [ libs ] Add `public export` modifiers to arithmetic inequality proofs

Pull Request - State: open - Opened by elkcl 23 days ago - 2 comments

#3376 - [ codegen ] get rid of artifacts introduced when optimizing `IO`

Pull Request - State: closed - Opened by stefan-hoeck 29 days ago - 3 comments
Labels: performance

#3374 - [ base ] Implement `Foldable` and `Traversable` for `Identity`

Pull Request - State: closed - Opened by buzden about 1 month ago

#3373 - [ refactor ] export signal to code conversions

Pull Request - State: closed - Opened by stefan-hoeck about 1 month ago

#3372 - Evaluation of partial functions during conversion

Issue - State: open - Opened by zanzix about 1 month ago - 1 comment
Labels: implem: normalise, discussion: design

#3371 - [ new ] add docs-for-type-of IDE command

Pull Request - State: open - Opened by DanMax03 about 1 month ago - 2 comments

#3369 - Parsing Performance & Maintainability.

Issue - State: open - Opened by andrevidela about 1 month ago - 4 comments

#3368 - [ refactor ] ScopedSnocList: WIP

Pull Request - State: open - Opened by GulinSS about 1 month ago - 5 comments

#3367 - Holes at unerased quantity produce bad code

Issue - State: open - Opened by dunhamsteve about 1 month ago

#3366 - [ fix ] Make searching in pairs to not cause ambiguity when there isn't

Pull Request - State: closed - Opened by buzden about 2 months ago - 1 comment

#3365 - Searching of `auto` inside pairs introduces ambiguity error between actually same things

Issue - State: closed - Opened by buzden about 2 months ago - 3 comments
Labels: language: let, implem: search

#3364 - Case split causes my function to no longer be covering

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

#3363 - [ fix ] Report chez failures

Pull Request - State: closed - Opened by dunhamsteve about 2 months ago - 2 comments

#3362 - [ new ] totality checking can look under constructors

Pull Request - State: open - Opened by dunhamsteve about 2 months ago

#3361 - `%hint` not listed as a pragma

Pull Request - State: closed - Opened by Matthew-Mosior about 2 months ago - 1 comment

#3360 - `idris2 --init` doesnt check the name of a package

Pull Request - State: closed - Opened by Matthew-Mosior about 2 months ago

#3359 - Revert "[ new ] totality checking can look under constructors (#3328)"

Pull Request - State: closed - Opened by gallais about 2 months ago

#3358 - [ linear ] typo in the docstring

Pull Request - State: closed - Opened by gallais about 2 months ago
Labels: documentation, typo, library: linear

#3357 - Erased type-casing function seen as total when it's not

Issue - State: open - Opened by gallais about 2 months ago
Labels: status: confirmed bug, safety: coverage, safety: proof of false

#3356 - Dictionary syntax

Pull Request - State: open - Opened by andrevidela about 2 months ago

#3355 - Syntax for Dictionary types

Issue - State: open - Opened by andrevidela about 2 months ago - 7 comments
Labels: Feature request

#3354 - Regression in #3328, compilation now hangs sometimes

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

#3353 - Clean removes generated docs

Pull Request - State: closed - Opened by Matthew-Mosior about 2 months ago - 2 comments

#3352 - [ fix #1236 ] Already fixed, add test case

Pull Request - State: closed - Opened by gallais about 2 months ago

#3351 - Show module docstring for namespace indexes

Pull Request - State: closed - Opened by Matthew-Mosior about 2 months ago - 5 comments
Labels: documentation, backend: html

#3350 - [ fix ] check indentation after = in declarations

Pull Request - State: closed - Opened by dunhamsteve 2 months ago
Labels: status: confirmed bug, implem: parsing

#3349 - Support more flexible requirements for Golden tests

Pull Request - State: closed - Opened by mattpolzin 2 months ago
Labels: enhancement, library: test

#3348 - Add `fromRight` and `fromLeft` for extracting values out of `Either`

Pull Request - State: closed - Opened by joelberkeley 2 months ago - 1 comment

#3346 - Fix annoying warning when running tests on some macOS machines

Pull Request - State: closed - Opened by mattpolzin 3 months ago
Labels: admin: continuous-integration

#3345 - Totality checker inconsistency when using Inf

Issue - State: open - Opened by JavierGelatti 3 months ago - 2 comments

#3344 - Why quoted values are EmptyFC?

Issue - State: open - Opened by freddi301 3 months ago

#3343 - Bootstrap with Racket error: `raco: Unrecognized command: exe`

Issue - State: open - Opened by barracuda156 3 months ago - 3 comments
Labels: Installation Issue

#3342 - Nested code blocks are ignored in literate markdown

Issue - State: open - Opened by joelberkeley 3 months ago - 1 comment

#3341 - [ cleanup ] Make `makeFuture` to be `%foreign`, not `%extern`

Pull Request - State: closed - Opened by buzden 3 months ago
Labels: code: cleanup, language: primitives

#3340 - [ fix #3339 ] Set the global test locale

Pull Request - State: closed - Opened by buzden 3 months ago
Labels: status: confirmed bug, admin: continuous-integration

#3339 - Test idris2/reflection/reflection024 fails due to not accounting for locales

Issue - State: closed - Opened by elkcl 3 months ago
Labels: Installation Issue

#3338 - [ fix ] compile time typecase for functions

Pull Request - State: closed - Opened by dunhamsteve 3 months ago
Labels: status: confirmed bug, language: typecase

#3336 - Support for non-glibc versions of linux (musl, android)

Pull Request - State: open - Opened by spocino 3 months ago

#3335 - [ elab ] Change quantity of the `search` function's argument to `0`

Pull Request - State: closed - Opened by buzden 3 months ago
Labels: enhancement, language: reflection, library: base

#3334 - [ elab, minor ] Implement `Functor` for `PiInfo`

Pull Request - State: closed - Opened by buzden 3 months ago
Labels: enhancement, library: base

#3332 - Public export Decidable.Decidable.decision

Pull Request - State: closed - Opened by michaelmesser 3 months ago

#3331 - [ perf ] Use alternative better GC on chez

Pull Request - State: closed - Opened by buzden 3 months ago
Labels: performance, backend: chez

#3330 - Nix `buildIdris` improvement: precisely target executable

Pull Request - State: closed - Opened by mattpolzin 3 months ago
Labels: admin: packaging, os: nix

#3329 - Add type annotations to monadic bind #3327

Pull Request - State: closed - Opened by dunhamsteve 3 months ago

#3328 - [ new ] totality checking can look under constructors

Pull Request - State: closed - Opened by dunhamsteve 3 months ago
Labels: enhancement, implem: termination checking

#3327 - Support type annotations on LHS of a monadic bind `<-`

Issue - State: open - Opened by joelberkeley 3 months ago - 9 comments
Labels: Feature request

#3326 - idris2.ss: support powerpc

Pull Request - State: closed - Opened by barracuda156 3 months ago - 20 comments
Labels: os: mac, backend: chez, backend: chez-sep

#3325 - idris_signal: fix static_assert

Pull Request - State: closed - Opened by barracuda156 3 months ago - 4 comments
Labels: library: base

#3324 - idris_support: fix environ for macOS

Pull Request - State: closed - Opened by barracuda156 3 months ago - 5 comments
Labels: library: base

#3323 - [ cleanup ] remove unused code left in #3108

Pull Request - State: closed - Opened by dunhamsteve 3 months ago - 1 comment

#3322 - Add fromTTImp, fromName, and fromDecls

Pull Request - State: closed - Opened by madman-bob 3 months ago

#3321 - Add JSON manipulation functions

Pull Request - State: closed - Opened by madman-bob 3 months ago - 12 comments
Labels: library: contrib

#3320 - [ re #3314, #34 ] Tighten the location information for implicits

Pull Request - State: closed - Opened by gallais 3 months ago
Labels: language: auto-implicit, language: implicit, error: reporting

#3319 - [ fix #72 ] remove the broken modules

Pull Request - State: closed - Opened by gallais 3 months ago - 3 comments
Labels: library: contrib, code: cleanup

#3318 - List packages improvements

Pull Request - State: closed - Opened by mattpolzin 3 months ago - 1 comment
Labels: enhancement, language: packaging

#3317 - Reconstructing a (structurally smaller) aggregate from pattern-matched components trips up the totality checker

Issue - State: open - Opened by hyphenrf 3 months ago - 8 comments
Labels: Feature request, implem: termination checking

#3315 - Emit error when unbound fixity is hidden

Pull Request - State: closed - Opened by andrevidela 3 months ago
Labels: language: fixity

#3314 - [ fix ] auto search returns no solution instead of ambiguous solution #3313

Pull Request - State: closed - Opened by dunhamsteve 3 months ago - 2 comments
Labels: implem: search, error: reporting

#3309 - Execution and compilation hangs indefintely

Issue - State: closed - Opened by freddi301 3 months ago - 3 comments

#3306 - [ fix ] implicits are not in scope under an implicit parameter block

Pull Request - State: closed - Opened by dunhamsteve 3 months ago - 1 comment

#3302 - Add error message with missing fixity namespace

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

#3264 - Doc: "Multiplicities" section roadmap

Issue - State: closed - Opened by foxyseta 5 months ago - 7 comments
Labels: documentation, admin: faq

#3258 - [ fix ] Fix search around `%defaulthints`

Pull Request - State: closed - Opened by buzden 5 months ago

#3242 - [RefC] Object Immortalization and Pre-Generation of Constants

Pull Request - State: open - Opened by seagull-kamome 6 months ago
Labels: backend: refc

#3232 - `idris2 --init` doesn't check a name of a package

Issue - State: closed - Opened by DanMax03 7 months ago - 2 comments
Labels: status: confirmed bug, cli: package init

#3014 - Show module docstring for namespace indexes

Issue - State: closed - Opened by scarf005 about 1 year ago - 4 comments
Labels: good first issue, Feature request

#2994 - chez bootstrap requires large amount of memory

Issue - State: open - Opened by spocino over 1 year ago - 8 comments
Labels: Installation Issue

#2932 - `%defaulthint` works differently with `data` and `interface`

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

#2867 - Incorrect running times for Data.Seq due to missing laziness

Issue - State: open - Opened by noinia over 1 year ago - 6 comments

#2828 - Invalid lexing of self-closing multiline comments of the form `{------}`

Issue - State: closed - Opened by Matthew-Mosior over 1 year ago - 5 comments
Labels: status: confirmed bug, implem: lexing, language: comments

#2791 - [ performance ] Implement weak memoisation of lazy values for chez and racket

Pull Request - State: closed - Opened by buzden almost 2 years ago - 4 comments
Labels: performance, event: IDM 2022/12

#2766 - `%hint` not listed as a pragma

Issue - State: closed - Opened by CodingCellist almost 2 years ago - 2 comments
Labels: good first issue, status: confirmed bug

#2555 - Fix issue with case inside a Pi type.

Pull Request - State: closed - Opened by dunhamsteve about 2 years ago - 1 comment
Labels: status: confirmed bug, language: quantity, implem: elaboration

#2250 - Definition with no RHS is incorrectly accepted as total

Issue - State: open - Opened by gallais over 2 years ago - 11 comments
Labels: status: confirmed bug, safety: coverage, safety: proof of false, implem: pattern-matching, language: impossible

#1988 - total Omega : ⊥

Issue - State: open - Opened by yallop almost 3 years ago - 4 comments
Labels: status: confirmed bug, safety: proof of false, safety: positivity, implem: termination checking, language: data, implem: typechecking

#1918 - Known issues of the `--mkdoc` command

Issue - State: open - Opened by gallais about 3 years ago - 2 comments
Labels: good first issue, status: confirmed bug, backend: html

#1236 - Access modifiers of definitions overwrite forward definitions

Issue - State: closed - Opened by ohad over 3 years ago - 6 comments
Labels: good first issue, status: confirmed bug, scope: public, language: forward-definition

#1201 - Layout processing - same column ; Haskell vs Idris

Issue - State: open - Opened by MilanKral over 3 years ago - 2 comments
Labels: good first issue, language: let, syntax, implem: parsing

#1179 - Failure to compile FFI-readline example on nix.

Issue - State: closed - Opened by locallycompact over 3 years ago - 5 comments
Labels: good first issue, Installation Issue, status: confirmed bug, os: nix