3 ms·

I too, would personally prefer a command line REPL. But sometimes you are interested enough in a thing to try it out, but not interested enough to install thin

I too, would personally prefer a command line REPL. But sometimes you are interested enough in a thing to try it out, but not interested enough to install things. Coq, in particular, is a pretty brutal installation process if you aren't already an emacs user. These web REPL's are great for reducing the friction necessary to try something out, and thereby getting people more interested. This one in particular is a big win for convenience over existing tooling. I will add, I think it can be very disheartening for people who put a lot of their own time into making something happen and then having a random commenter say, 'Yeah, but I would rather have had something else, that wasn't at all the project you set out to make.'

chriswarbo 11y ago
> Coq, in particular, is a pretty brutal installation process if you aren't already an emacs user. It's only "brutal" if you're compiling from source, in which case you've got to compile all of the ML and then all of the Coq libraries. That's only necessary for experimental branches though; I've not used an OS which doesn't provide binaries of official releases. The installation process is basically "apt-get install coq && coqide", or whatever package manager your system uses. That will run the GTK interface which comes bundled with Coq. The only time when Emacs might have anything to do with Coq is in relation to Proof General; but the only reason to run PG is if you're already an Emacs user. It's been in maintenance mode for years, and being rapidly overtaken by asynchronous interfaces based on PIDE (eg. the jEdit and Eclipse plugins). I'm a very happy Emacs user, but just because I use Coq via PG doesn't mean I'd ask non-Emacs-users to do the same; in the same way that I access my GMail account via Gnus, but wouldn't try to convince non-Emacs GMail users to do the same.
- clarus 11y ago
  By the way, there is also the OPAM package manager for Coq to install Coq and user libraries easily: http://coq-blog.clarus.me/use-opam-for-coq.html http://coq-blog.clarus.me/use-opam-for-coq.html
tempodox 11y ago
...it can be very disheartening... I hear what you're saying, but that's the risk you must take when you do a public display like that. Besides, it's at least half the fun. What's the use of only fanboys (& -girls) commenting, if that's not the whole picture?

chriswarbo 11y ago

> Coq, in particular, is a pretty brutal installation process if you aren't already an emacs user. It's only "brutal" if you're compiling from source, in which case you've got to compile all of the ML and then all of the Coq libraries. That's only necessary for experimental branches though; I've not used an OS which doesn't provide binaries of official releases. The installation process is basically "apt-get install coq && coqide", or whatever package manager your system uses. That will run the GTK interface which comes bundled with Coq. The only time when Emacs might have anything to do with Coq is in relation to Proof General; but the only reason to run PG is if you're already an Emacs user. It's been in maintenance mode for years, and being rapidly overtaken by asynchronous interfaces based on PIDE (eg. the jEdit and Eclipse plugins). I'm a very happy Emacs user, but just because I use Coq via PG doesn't mean I'd ask non-Emacs-users to do the same; in the same way that I access my GMail account via Gnus, but wouldn't try to convince non-Emacs GMail users to do the same.

clarus 11y ago
By the way, there is also the OPAM package manager for Coq to install Coq and user libraries easily: http://coq-blog.clarus.me/use-opam-for-coq.html http://coq-blog.clarus.me/use-opam-for-coq.html

tempodox 11y ago

...it can be very disheartening... I hear what you're saying, but that's the risk you must take when you do a public display like that. Besides, it's at least half the fun. What's the use of only fanboys (& -girls) commenting, if that's not the whole picture?