search

idris-hackers / IdrisWeb

A secure web framework, built in the Idris language.
MIT License
109 stars 6 forks source link

Syntactic error when building #10

Open fabriceleal opened 9 years ago

fabriceleal commented 9 years ago

When I build IdrisWeb by

idris --build idris_web.ipkg

I get a syntactic error

./IdrisWeb/DB/SQLite/SQLiteNew.idr:321:17: error: not
    a terminator, expected: (....)
reset = if_left then ResetFromEnd else Reset

I also saw a lot of if_valid scattered through the same file. My idris version: 0.9.14.2-git:f50a883

david-christiansen commented 9 years ago

I believe this is from an older version of effects. It'll need porting to the new one.

/David (from phone)

jmitchell commented 9 years ago

While reading the paper I also started wondering about if_valid.

Based on the changelog it was introduced in v0.9.10. Poked around a bit with git bisect and identified these two commits, the first where if_valid was moved to oldeffects and the second where oldeffects was removed entirely.

SimonJF commented 9 years ago

Yup, this is all done oldeffects, as described in the ICFP13 paper. There was a brief period between oldeffects and neweffects where if_valid was introduced.

What if_valid does was basically a more specific version of the new effects system -- instead of allowing the result of an effectual operation to determine the output effect, the output effect was a sum type, and if_valid differentiated between it. It turned out to be a bit messy (as you can see!), and this is when Edwin added Resource-Dependent Algebraic Effects, as you can see in the TFP'14 paper.

The initial draft didn't have if_valid -- instead, it handled things on the value level, not making underlying calls unless everything was OK. This was messy, hence the inspiration for neweffects.

(I know mine refers to RDAEs, which in that case referred to the old system, which is confusing. Sorry about that).

Essentially though, there's a huge amount of bitrot to fix here to get it working with neweffects, which I'll have to get round to at some point. @david-christiansen did some work a while ago on porting the SQLite library to neweffects though, which might be useful.

ericqweinstein commented 8 years ago

@david-christiansen & @SimonJF, this will be a bit longish, so! I'll preface by saying I'm very happy to make any PRs necessary to help get this project up & running with Idris 0.9.20 (I'm running 0.9.20.1).

The project now fails to build due to the recent FFI changes:

λ idris --install idris_web.ipkg
Entering directory `./src'
make: Nothing to be done for `all'.
Type checking ./IdrisWeb/Common/Random/RandC.idr
./IdrisWeb/Common/Random/RandC.idr:8:11:
When checking right hand side of getRandom with expected type
        IO Int

No such variable mkForeign

I think that this line (IdrisWeb/Common/Random/RandC.idr:8:11):

getRandom min max = mkForeign (FFun "random_number" [FInt, FInt] FInt) min max

should now be:

getRandom min max = foreign FFI_C "random_number" (Int -> Int -> IO Int) min max

Next, it looks like we need to update the package syntax:

λ idris --install idris_web.ipkg
Entering directory `./src'
make: Nothing to be done for `all'.
Type checking ./IdrisWeb/Common/Random/RandC.idr
Can't find import Effects

I think this change to idris_web.ipkg will do it:

package idrisweb

opts = "--typecase"
pkgs = effects, simpleparser

At this point, we start getting the above-noted if_* errors (IdrisWeb/DB/SQLite/SQLiteNew.idr:321:17):

reset = if_left then ResetFromEnd else Reset

I'm happy to make the FFI and package changes (in separate PRs) if the incremental improvement seems worthwhile; if you have the time to provide some guidance, I'm also happy to work on porting to the new Effects library or doing whatever needs doing.

Thanks so much for your work on this project! I've only just started working with Idris, but love it so far.

david-christiansen commented 8 years ago

I'd be happy to answer what questions I can if you want to work on de-bitrotting this lib. I haven't done the real work on this library, but I think you've identified what needs doing.

I don't think it's realistic to do these in separate PRs, because you can't test it until all of them are done. So I'd just update it to work with the newest Idris, and send a commit.

Thanks!

ericqweinstein commented 8 years ago

@david-christiansen Makes sense; I'll get cracking and submit a PR (though it may be large) when ready.

Are there preferred replacements for if_left and if_valid?

david-christiansen commented 8 years ago

On December 6, 2015 9:19:32 PM GMT+01:00, Eric Weinstein notifications@github.com wrote:

@david-christiansen Makes sense; I'll get cracking and submit a PR (though it may be large) when ready.

Are there preferred replacements for if_left and if_valid?

Reply to this email directly or view it on GitHub: https://github.com/idris-hackers/IdrisWeb/issues/10#issuecomment-162344431

Pattern matching on the result of the call does the same thing now!

ericqweinstein commented 8 years ago

:+1:

ericqweinstein commented 8 years ago

@david-christiansen Making good headway! Are these SQLite bindings relatively current (would they be useful in updating src/IdrisWeb/DB/SQLite/SQLiteNew.idr)?

ericqweinstein commented 8 years ago

Done so far:

Working on:

neduard commented 8 years ago

@ericqweinstein Hey there, I was playing around with making IdrisWeb compile when I stumbled upon this issue and I see you already made some progress in solving it :+1: Any idea on when you might have time to complete the update? Or maybe share a "work-in-progress" branch on what you have updated so far?

SimonJF commented 8 years ago

Hi, sorry I seem to have missed this.

I'd say that this is in need of a rewrite now -- the Effects library that was current back when this library was written is deprecated now.

IdrisWeb provided:

What were you looking for from the library?

Reflecting on the web form DSL, I now think there are better ways of doing this (Formlets, in particular) and this implementation, while an interesting experiment, rather overcomplicates things.

neduard commented 8 years ago

@SimonJF oh I see, I wanted to setup a simple webpage using Idris. I want to learn the language and I thought working with already existing, simple code, would be a very good learning experience.

ericqweinstein commented 8 years ago

@neduard Thanks for reminding me about this! I sort of fell down a rabbit hole and agree with @SimonJF that this probably needs to be rewritten, given the changes in Idris and the Effects library since this repo was started. I'm happy to collaborate on that—things are a bit hectic on my end this week, but I'm free to help out starting next. 👍