Steve Dunham

I didn't see this until after I filed #2552, but the scheme backends have the same problem. They appear to be leaking a lot of memory (e.g. 100k leaks from...

Yeah, this is not an issue if you compile with the `node` codegen, which I'd recommend if you intend to run the code outside the browser. It has a more...

I could see cases where there is both a .ttc and a .so, but the .so is older than the .ttc (e.g. compile with incr on, change file, compile with...

Interesting. So the .ttc file says if there is a .so or not. And it collects that information to know what to link, but doesn't actually include the code in...

Ok, it was more subtle than I thought, but it looks like this will fix the issue. The root cause is that Idris will drop the `allIncData` for a backend...

Yeah, I wasn't sure what to do in the non-PLet cases, so I just put `top` in there tentatively. In Case.idr, I kinda followed what Binders.idr was doing for ILet...

Last night (UTC-7) I figured out that the `allow` in Case.idr was lifting x back up from Rig0 to Rig1, which is why I put that if statement in there....

Yeah, double check the Maybe thing. I thought about a Maybe, but saw the code for `ILet` in `Binders.idr` that it just multiplied the optionally supplied rig with ambient. I...

It's interesting that this fails: ```idris data Foo : Bool -> Type where MkInt : Int -> Foo True MkString : String -> Foo False blah : (0 f :...

Yeah, I wasn't used to binding capitalized names. With the parens, it fails: ```idris data Bar : Bool -> Type where BarA : Bar True BarB : Bar False blah...