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

#3398 - Unable to `--exec` ambiguous mains

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

#3395 - [ fix ] Data and Type Constructor tags for :di

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

#3394 - [ refactor ] Add a nix overlay

Pull Request - State: closed - Opened by mitchmindtree about 1 month ago - 7 comments

#3393 - fix: help menu for `refine` command

Pull Request - State: open - Opened by Jyang772 about 1 month ago

#3392 - [ base ] Deprecate `toList` functions for sorted sets and maps

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

#3391 - Girards Paradox copied from Agda

Issue - State: closed - Opened by yokto about 2 months ago - 1 comment
Labels: safety: proof of false, language: universe levels

#3390 - Type checker silently stuck on missing import.

Issue - State: open - Opened by yellowsquid about 2 months ago - 3 comments
Labels: status: expected behaviour, language: import, scope: public, scope: private

#3388 - [ doc ] Update gambit docs

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

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

Issue - State: open - Opened by flintwinters about 2 months ago - 6 comments
Labels: Feature request

#3386 - Handle multiline comments in Package (ipkg)

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

#3385 - [ fix ] make buildIdris nix function still work when there are more than one app directories in the build output

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

#3384 - Correct ipkg comment docs

Pull Request - State: closed - Opened by stephen-smith about 2 months ago - 1 comment
Labels: documentation, status: confirmed bug

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

Issue - State: closed - Opened by gallais about 2 months ago - 1 comment
Labels: status: invalid, library: base

#3382 - include hidden files in artifact

Pull Request - State: closed - Opened by mattpolzin 2 months ago

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

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

#3380 - [ base ] Add atomically function

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

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

Issue - State: closed - Opened by johannes-riecken 2 months ago - 3 comments
Labels: status: invalid

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

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

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

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

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

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

#3373 - [ refactor ] export signal to code conversions

Pull Request - State: closed - Opened by stefan-hoeck 3 months ago

#3372 - Evaluation of partial functions during conversion

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

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

Pull Request - State: open - Opened by DanMax03 3 months ago - 2 comments

#3369 - Parsing Performance & Maintainability.

Issue - State: open - Opened by andrevidela 3 months ago - 4 comments

#3368 - [ refactor ] ScopedSnocList: WIP

Pull Request - State: open - Opened by GulinSS 3 months ago - 5 comments

#3367 - Holes at unerased quantity produce bad code

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

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

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

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

Issue - State: closed - Opened by buzden 3 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 3 months ago - 4 comments

#3363 - [ fix ] Report chez failures

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

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

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

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

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

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

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

#3358 - [ linear ] typo in the docstring

Pull Request - State: closed - Opened by gallais 4 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 4 months ago
Labels: status: confirmed bug, safety: coverage, safety: proof of false

#3356 - Dictionary syntax

Pull Request - State: open - Opened by andrevidela 4 months ago

#3355 - Syntax for Dictionary types

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

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

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

#3353 - Clean removes generated docs

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

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

Pull Request - State: closed - Opened by gallais 4 months ago

#3351 - Show module docstring for namespace indexes

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

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

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

#3349 - Support more flexible requirements for Golden tests

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

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

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

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

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

#3345 - Totality checker inconsistency when using Inf

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

#3344 - Why quoted values are EmptyFC?

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

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

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

#3342 - Nested code blocks are ignored in literate markdown

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

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

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

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

Pull Request - State: closed - Opened by buzden 4 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 4 months ago
Labels: Installation Issue

#3338 - [ fix ] compile time typecase for functions

Pull Request - State: closed - Opened by dunhamsteve 4 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 4 months ago

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

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

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

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

#3332 - Public export Decidable.Decidable.decision

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

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

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

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

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

#3329 - Add type annotations to monadic bind #3327

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

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

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

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

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

#3326 - idris2.ss: support powerpc

Pull Request - State: closed - Opened by barracuda156 5 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 5 months ago - 4 comments
Labels: library: base

#3324 - idris_support: fix environ for macOS

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

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

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

#3322 - Add fromTTImp, fromName, and fromDecls

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

#3321 - Add JSON manipulation functions

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

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

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

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

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

#3318 - List packages improvements

Pull Request - State: closed - Opened by mattpolzin 5 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 5 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 5 months ago
Labels: language: fixity

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

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

#3309 - Execution and compilation hangs indefintely

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

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

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

#3302 - Add error message with missing fixity namespace

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

#3272 - fixed bugs that caused compiler to hang forever when there is %tcinline pragma

Pull Request - State: open - Opened by AntonPing 6 months ago - 1 comment

#3264 - Doc: "Multiplicities" section roadmap

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

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

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

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

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

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

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

#3209 - Type checker does not terminate when comparing codata types.

Issue - State: closed - Opened by yellowsquid 9 months ago - 3 comments
Labels: status: duplicate, status: confirmed bug, language: codata

#3014 - Show module docstring for namespace indexes

Issue - State: closed - Opened by scarf005 over 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 almost 2 years ago - 6 comments

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

Issue - State: closed - Opened by Matthew-Mosior almost 2 years 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