Idris2

Idris2 copied to clipboard

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

1

# Description (This pull request is a continuation of pull request #3257, since github doesn't allow me to re-open it) close #2995 This pull request consists of two part: -...

AntonPing

unification failure between if then else statements when using isYes (decEq n a) as the condition

2

``` $ idris2 --version Idris 2, version 0.7.0 ``` code: ``` import Data.Vect import Decidable.Equality import Decidable.Decidable count : Nat -> Vect n Nat -> Nat count t [] =...

astaugaard

# Steps to Reproduce ```idris %default total interface S where pop : {_ : Unit} -> Unit S where pop = ?fooo ``` The signature may have an `auto`-implicit parameter...

buzden

# Steps to Reproduce Set `CHEZ` environment variable to something that does not start with a slash (`/`) and compile an application. # Expected Behavior Either successsfull compilation or nice...

buzden

Nested Structs in FFI not read correctly

2

**Issue by [vfrinken](https://github.com/vfrinken)** _Tuesday Mar 24, 2020 at 04:39 GMT_ _Originally opened as https://github.com/edwinb/Idris2-boot/issues/238_ ---- If I have 2 structs in C ```C typedef struct{ int * a; int b;...

edwinb

In the following freehand code I'm concerned that Idris can garbage collect the `Foo` pointer while it's still in use. I have had mixed experience with using this pattern. Sometimes...

joelberkeley

Loss of Linearity in Interaction of Abstract Interfaces and Linear State Transformer Monad

5

A full explanation of and a minimal case for reproducing the problem can be found here: https://github.com/Lichborne/IdrisLinearityIssue/blob/main/ErrorExamples.idr Depends only on Data.Linear.LVect and Data.Linear.Notation # Steps to Reproduce Firstly, we create...

Lichborne

This came up as part of a thing I'm currently working on. Due to `Prelude.elem` being implemented for all `Foldable`s, it is significantly slower at compile-time compared to the "trivial"...

CodingCellist

Fedora FC38, FC39 with racket 7.9 — "make bootstrap-racket" freezes on compilation

2

Trying install idris2 with racket on Fedora with racket 7.9 (tested on FC38 and FC39, on several desktops, `racket-7.9-1.fc38.x86_64`, `racket-7.9-1.fc39.x86_64`) Compilation `raco exe idris2_app/idris2-boot.rkt` from `make bootstrap-racket` hangs with 100%...

belonesox

# Steps to Reproduce Typecheck the following code ```idris import Data.DPair f : Exists List -> Unit f = \(Evidence _ _) => () ``` in an editor with semantic...

buzden