idris-lang/Idris2 issues and pull requests

#100 - Use Control.Delayed from the 'contrib' package

Pull Request - State: closed - Opened by ska80 over 4 years ago - 3 comments

#99 - "Alternative 2: Installing with an existing Idris 2" stopped working

Issue - State: closed - Opened by ska80 over 4 years ago - 2 comments
Labels: Installation Issue

#98 - Building on Mac OSX 10.14.5 fails

Issue - State: closed - Opened by b-studios over 4 years ago - 3 comments
Labels: Installation Issue

#97 - Discrepancies between IDE mode protocol and Emacs idris-mode

Issue - State: open - Opened by abailly over 4 years ago - 3 comments

#96 - Exclude `DN` from `Hashable Name`

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

#95 - Implementations trigger unnecessary rebuild of dependent modules

Issue - State: closed - Opened by ziman over 4 years ago - 2 comments

#94 - Windows support

Pull Request - State: closed - Opened by melted over 4 years ago - 5 comments

#93 - Rename some file/dir manipulation functions for consistency

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

#92 - Move System.Clock from 'contrib' to 'base'

Pull Request - State: closed - Opened by ska80 over 4 years ago - 2 comments

#91 - Correct ‘Installation problem’ issue template

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

#90 - Fix typo seperate -> separate in System/Path.idr

Pull Request - State: closed - Opened by keram over 4 years ago - 1 comment

#89 - Split Parser into Source(.idr) and Package (.ipkg) (Part 1)

Pull Request - State: closed - Opened by fabianhjr over 4 years ago - 1 comment

#88 - libs/network: Port FFI calls from deprecated interface to `%foreign` pragma

Pull Request - State: closed - Opened by ohad over 4 years ago - 1 comment

#87 - Remove stale src/IdrisPath.idr on each 'make clean' run

Pull Request - State: closed - Opened by ska80 over 4 years ago - 1 comment

#86 - Add a total version of the fromMaybe

Pull Request - State: closed - Opened by andylokandy over 4 years ago - 1 comment

#85 - Add List folds without default value

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

#84 - Split Parser.Support

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

#83 - Fixing path: `idris2-boot.ss` instead of `idris2-boot.so`

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

#82 - Add System.Path

Pull Request - State: closed - Opened by andylokandy over 4 years ago - 5 comments

#81 - Update README.md

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

#80 - Update INSTALL.md

Pull Request - State: closed - Opened by jfdm over 4 years ago
Labels: documentation

#79 - Update README.md

Pull Request - State: closed - Opened by jfdm over 4 years ago
Labels: documentation

#78 - First class byte array support

Issue - State: open - Opened by edwinb over 4 years ago - 7 comments
Labels: Feature request

#77 - Build error: Can't disambiguate name: Main.yprefix, YafflePaths.yprefix

Issue - State: closed - Opened by edwinb over 4 years ago - 3 comments
Labels: Installation Issue

#76 - Can't pass argument of type %World to foreign function

Issue - State: closed - Opened by edwinb over 4 years ago - 1 comment

#75 - linear lambda claims to consume unrelated binder

Issue - State: open - Opened by edwinb over 4 years ago - 6 comments
Labels: error: bad message, status: expected behaviour

#74 - case-split fails on private definition in nested namespace

Issue - State: closed - Opened by edwinb over 4 years ago - 2 comments
Labels: status: confirmed bug, interactive: case

#73 - Multiplicity subtyping with dependent types can break linearity

Issue - State: closed - Opened by edwinb over 4 years ago - 16 comments
Labels: status: confirmed bug, implem: quantity subtyping

#72 - Interface resolution bug

Issue - State: closed - Opened by edwinb over 4 years ago - 16 comments
Labels: status: confirmed bug, library: contrib

#71 - Proof search produces ill-typed terms

Issue - State: closed - Opened by edwinb over 4 years ago - 1 comment

#70 - Incorrect reduction of pattern matching

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

#69 - Issue with hints and search space: Can't find implementation

Issue - State: closed - Opened by edwinb over 4 years ago - 1 comment
Labels: status: expected behaviour

#68 - 'addclause' client command fails to produce a meaningful definition for helpers under 'where' blocks

Issue - State: closed - Opened by edwinb over 4 years ago

#67 - Implicits in Interface Functions cause Typecheck Error

Issue - State: closed - Opened by edwinb over 4 years ago - 11 comments
Labels: status: confirmed bug, language: implicit

#66 - Can't unify an interface with its instance

Issue - State: closed - Opened by edwinb over 4 years ago - 2 comments

#65 - inference in case requires extra let

Issue - State: closed - Opened by edwinb over 4 years ago - 4 comments
Labels: language: case, implem: inference

#64 - type inference on record update in let doesn't work based on RHS

Issue - State: open - Opened by edwinb over 4 years ago - 2 comments
Labels: status: confirmed bug, implem: inference, language: record update

#63 - one type annotation in let means all other definitions must have type annotation

Issue - State: closed - Opened by edwinb over 4 years ago - 6 comments
Labels: status: discussion, language: let

#62 - case in a lambda is broken

Issue - State: open - Opened by edwinb over 4 years ago - 1 comment
Labels: language: case, language: lambda-case, implem: inference

#61 - feature request: constructor only/wildcard pattern matches

Issue - State: closed - Opened by edwinb over 4 years ago - 1 comment
Labels: Feature request, syntax

#60 - Messing up parameters order of interfaces implementation

Issue - State: closed - Opened by edwinb over 4 years ago - 1 comment
Labels: status: confirmed bug, implem: interface elaboration

#59 - Duplicate pattern cases have an unclear error message

Issue - State: closed - Opened by edwinb over 4 years ago - 2 comments

#58 - Non-Auto Implicits get Deferred as Holes and not checked on REPL Evaluation

Issue - State: closed - Opened by edwinb over 4 years ago - 2 comments
Labels: status: confirmed bug, implem: normalise, language: implicit

#57 - Ambigous Implementations when using `using` on a constrainted interface implementation

Issue - State: closed - Opened by edwinb over 4 years ago - 1 comment
Labels: status: confirmed bug, language: interface, language: using

#56 - Multiple constrains with unreseolved type parameters on interface declaration cause typecheck issue

Issue - State: closed - Opened by edwinb over 4 years ago - 4 comments
Labels: status: expected behaviour, implem: interface resolution

#55 - Local definitions in irrelevant definitions are incorrectly checked for relevance

Issue - State: closed - Opened by edwinb over 4 years ago - 13 comments
Labels: good first issue, status: confirmed bug, language: quantity, language: where

#54 - Using the arrow keys in the REPL should cycle through recently used commands

Issue - State: closed - Opened by edwinb over 4 years ago - 9 comments
Labels: good first issue, Feature request, cli: repl

#53 - Automated Documentation generation from source code.

Issue - State: closed - Opened by edwinb over 4 years ago - 2 comments
Labels: Feature request

#52 - Browsable source code

Issue - State: closed - Opened by edwinb over 4 years ago - 6 comments
Labels: Feature request, status: upstream

#51 - problem with Prelude

Issue - State: closed - Opened by edwinb over 4 years ago - 10 comments
Labels: Installation Issue, admin: faq

#50 - "record {elem_name} record_name" to access elements in a record

Issue - State: closed - Opened by edwinb over 4 years ago - 6 comments
Labels: Feature request

#49 - chez010 test fails with libcb.so cannot open shared object file

Issue - State: closed - Opened by edwinb over 4 years ago - 6 comments
Labels: Installation Issue

#48 - Add option to dump CompileExpr in a standard, parseable format

Issue - State: closed - Opened by edwinb over 4 years ago - 3 comments
Labels: Feature request

#47 - JavaScript backend

Issue - State: closed - Opened by edwinb over 4 years ago - 13 comments
Labels: Feature request, backend: javascript

#46 - Missing functionality: impossibility assertions in pattern-matching anonymous functions

Issue - State: closed - Opened by edwinb over 4 years ago - 4 comments
Labels: status: expected behaviour, language: lambda-case

#45 - Build failing when linking libidris_rts in MSYS2 MinGW64 terminal

Issue - State: closed - Opened by edwinb over 4 years ago - 1 comment
Labels: Installation Issue, status: upstream

#44 - WSL1 install error

Issue - State: closed - Opened by edwinb over 4 years ago - 4 comments
Labels: Installation Issue, os: windows

#43 - INTERNAL ERROR: build/ttc/Test.ttc: File Not Found

Issue - State: closed - Opened by edwinb over 4 years ago - 4 comments
Labels: cli: repl, internal error

#42 - "Undefined name filter"

Issue - State: closed - Opened by edwinb over 4 years ago - 1 comment

#41 - "Can't find an implementation for Range Type"

Issue - State: open - Opened by edwinb over 4 years ago - 2 comments
Labels: error: bad message, implem: overloading

#40 - AddClause does not not generate a correct clause for operators

Issue - State: open - Opened by edwinb over 4 years ago
Labels: status: confirmed bug, language: interface, interactive: case

#39 - AddClause on an interface implementation adds only one clause

Issue - State: open - Opened by edwinb over 4 years ago
Labels: status: confirmed bug, language: interface, interactive: case

#38 - AddClause does not indent the clauses of an interface implementation

Issue - State: closed - Opened by edwinb over 4 years ago - 1 comment
Labels: status: confirmed bug, language: interface, interactive: case

#37 - Idris always use <file>.idr instead of <file>.lidr

Issue - State: closed - Opened by edwinb over 4 years ago - 4 comments
Labels: status: confirmed bug, cli: repl, implem: import

#36 - Nested Structs in FFI not read correctly

Issue - State: open - Opened by edwinb over 4 years ago - 2 comments

#35 - Pretty printing of duplicate names should avoid name clashes

Issue - State: open - Opened by edwinb over 4 years ago - 14 comments
Labels: error: bad message, naming

#34 - Multiple solutions found in search error

Issue - State: open - Opened by edwinb over 4 years ago - 4 comments
Labels: status: expected behaviour, implem: interface resolution

#33 - Native Windows build efforts

Issue - State: closed - Opened by edwinb over 4 years ago - 2 comments
Labels: Installation Issue

#32 - Cannot compile prelude with latest Idris, file read error

Issue - State: closed - Opened by edwinb over 4 years ago - 11 comments
Labels: Installation Issue

#31 - Whitespace sensitive parsing of local definitions (type-ascribing let)

Issue - State: closed - Opened by edwinb over 4 years ago - 1 comment
Labels: status: confirmed bug, language: let, implem: parsing

#30 - Compiler.Common.tmpName should not use tmpnam

Issue - State: closed - Opened by edwinb over 4 years ago - 2 comments

#29 - Double IEEE constants: infinity, NaN, epsilon ... where are they?

Issue - State: closed - Opened by edwinb over 4 years ago - 6 comments
Labels: good first issue, Feature request, language: float

#28 - Incorrect interaction of nested with blocks and nested dependent pattern matching

Issue - State: open - Opened by edwinb over 4 years ago - 1 comment
Labels: language: with, implem: elaboration

#27 - With-clause doesn't take advantage of ruled out patterns to normalise

Issue - State: closed - Opened by edwinb over 4 years ago - 2 comments
Labels: Feature request

#26 - Normaliser doesn't detect reducible patterns across arguments

Issue - State: closed - Opened by edwinb over 4 years ago - 2 comments

#25 - Flip the Left/Right branches of Data.So.choose

Issue - State: closed - Opened by edwinb over 4 years ago - 1 comment
Labels: Feature request

#24 - Module import unstable

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

#23 - REPL 'last change' time-stamp should be taken from start of reload

Issue - State: closed - Opened by edwinb over 4 years ago

#22 - fail to reduce imported functions when name could be ambiguous

Issue - State: closed - Opened by edwinb over 4 years ago - 2 comments

#21 - Segfault when displaying a hole

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

#20 - Whitespace-sensitive parsing of let binding without ascription

Issue - State: closed - Opened by edwinb over 4 years ago - 1 comment

#19 - Totality annotations are ignored

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

#18 - Infinite loop in the REPL for GenerateDefinition on binary tree

Issue - State: closed - Opened by edwinb over 4 years ago - 3 comments
Labels: status: confirmed bug, language: quantity, interactive: search

#17 - Can't build network library on Windows

Issue - State: closed - Opened by edwinb over 4 years ago - 11 comments
Labels: Installation Issue

#16 - Unexpected run-time complexity

Issue - State: closed - Opened by edwinb over 4 years ago - 16 comments
Labels: performance

#15 - Cycle detected in solution of metavariable:

Issue - State: closed - Opened by edwinb over 4 years ago - 5 comments
Labels: error: bad message, Needs a closer look

#14 - Implicit lambda arguments

Issue - State: open - Opened by edwinb over 4 years ago - 10 comments
Labels: Feature request

#13 - Feature requests and proposals

Issue - State: closed - Opened by edwinb over 4 years ago - 20 comments
Labels: Proposal

#12 - Silence 'idris2 --clean idris2.ipkg' errors

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

#11 - Ignore Racket's build artifacts in 'bootstrap' directory

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

#10 - More fixes and improvements

Pull Request - State: closed - Opened by ska80 over 4 years ago - 1 comment

#9 - Ignoring autogenerated bootstrap/test files

Pull Request - State: closed - Opened by zenntenn over 4 years ago - 1 comment

#8 - Refactor Utils.String.stripQuotes to avoid double reversion on Strings

Pull Request - State: closed - Opened by fabianhjr over 4 years ago - 1 comment

#7 - Fix chez016 test

Pull Request - State: closed - Opened by chrrasmussen over 4 years ago - 1 comment

#6 - Create new mapError utility function and refactor some parser code

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

#5 - Make network test build on windows

Pull Request - State: closed - Opened by melted over 4 years ago - 2 comments

#4 - Refactor makefiles

Pull Request - State: closed - Opened by ska80 over 4 years ago - 1 comment

#3 - Update .gitignore files

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

#2 - Windows fixes

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

#1 - Add rmDir to System.Directory

Pull Request - State: closed - Opened by andrevidela over 4 years ago - 1 comment

GitHub / idris-lang/Idris2 issues and pull requests