search

idris-lang / Idris-dev

A Dependently Typed Functional Programming Language
http://idris-lang.org
Other
3.43k stars 644 forks source link

Command-line support for running a package (`idris run`) #3442

Open sbp opened 8 years ago

sbp commented 8 years ago

Akin to go run for Go, or cargo run for Rust. What somebody might expect from the existing --execute flag, cf. Issue #3441. @ahmadsalim suggested on IRC that this is something I could contribute, so I'm writing this issue as a reminder to myself and in case anybody else wants to pick it up if I don't.

Melvar commented 8 years ago

There is a REPL command, :exec, which compiles and runs the currently loaded file. (As opposed to :e, which uses the executor like --execute apparently does.) Perhaps that could be reused.

There’s also the question of whether this should be usable for source files, for ipkgs, or for both.