The Coq mailing list

[Amin Timany <amintimany AT gmail.com>]

Hi,

Mac application bundles (.dmg files downloadable from coq download page) need no installation. They are basically a compressed archive. There is a .app file in there that you can just copy/run. They come bundled with Coqide. You should be able to set up emacs and proof general to use the coq executable in the .app file but I have never tried this -- .app files are just folders.

amin

On Tuesday, July 21, 2015, Vincent Siles <vincent.siles AT ens-lyon.org> wrote:

Hi Jason,
Besides ProofWeb I don't know any other way. But you could build a
virtualbox/qemu virtual machine with what you need and give it to your
students, so they all have the same build ?

Best,
V.

2015-07-21 8:53 GMT+02:00 Jason Gross <jasongross9 AT gmail.com>:
> Hi,
> I'm teaching a class on Coq on Wednesday, and discovered Coq has not been
> installed on the computers I will be using.  Is there a way to run Coq on
> Windows and/or Mac without installing it (e.g., is there a
> run-from-a-flash-drive / portable version of Coq?  Are there websites that
> will let students run Coq programs and see the output?  There was a thread
> about this a year ago that mentioned ProofWeb and cloud.sagemath, but I'm
> curious if there are more options now.)
>
> Thanks,
> Jason