It appears IdrisSqlite does not build anymore

[MarkusBarthlen]

Hello,

when trying to compile the package (using the latest version of idris), I am getting the following:

idris --verbose --build sqlite.ipkg Entering directory `./src' gcc -c sqlite3api.c gcc -fPIC -o sqlite3api.so -shared sqlite3api.c Type checking ./DB/SQLite/SQLiteCodes.idr ./DB/SQLite/Effect.idr:108:16: error: expected: "%", type signature FinishBind : {SQLitePSSuccess Binding ==> ^
Type checking ./DB/SQLite/Effect.idr

Is there a problem with IdrisSqlite or is there something wrong with my installation? By the way, the following code in sqlite3api.c (line 157) also looks wrong:

if(rc == SQLITE_ERROR && rc == SQLITE_MISUSE){

Let me express my appreciation of your work. Your introduction videos on youtube are excellent.

[david-christiansen]

I'm happy those videos were worthwhile!

The problem with this library is that it's bit-rotted with respect to recent Idris releases and the new API of the effects library. I don't have time to update it right now, due to impending dissertation handin, but I can walk you through generally what needs to happen if you'd like.

It's quite likely that there's things that need improving in the C shim. It was always a quick hack - again, if you'd like to do some work on it, I'm happy to answer questions!

[MarkusBarthlen]

Well, I cannot promise anything, but I will take a (short or longer) look at it some time.

[david-christiansen]

Of course! Thanks for the report, in any case!

[ericqweinstein]

I've been working on this off and on and I've gotten a bit past the above error, though I've hit a few type mismatches since. @david-christiansen when you have some time, could you shed a bit of light on the below?

Type mismatch between
  SQLiteConnected
and
  either (Delay (\v => ())) (Delay (\v => SQLiteConnected)) result

I think this points to some laziness introduced in Idris 0.9.20.1/the latest version of Effects, but am not totally sure; right now I'm monkeying with the SQLiteConnected data type to try to figure it out. Learning a bunch about Idris in the process, at any rate!

[ericqweinstein]

(Happy holidays, by the way!)

[david-christiansen]

I'm off duty until next week - on honeymoon! Will check back to Github then. If it falls through the cracks, please ping me!

[david-christiansen]

But for this error, you need to pattern-match "result" somewhere.

[codygman]

Is that offer to help out still valid and do you have time? I might have some time from 12PM-4PM CT tomorrow to work on it in the off chance you can plan to be on IRC or monitoring Github ;)

[david-christiansen]

I won't be able to do real-time support this weekend, unfortunately, but I'm happy to check my email from time to time and answer questions that come up, free time allowing.