jscoq light

A trimmed down version of jscoq for teaching purposes.

First time setup

• Install docker. Docker requires sudo by default, because it uses chroot to create a lightweight "virtual machine". If you are not comfortable with this, there exists an experimental rootless version of Docker . However, I haven't yet tested whether it works.

• In the root of the project run sudo docker build --tag jscoq-dev-image . this will take a while.

• While still in the root of the project, create a container using

sudo docker container create -p 8000:8000 --mount type=bind,source=.,target=/root/jscoq --name jscoq-dev jscoq-dev-image

• You can now start the container using sudo docker container start jscoq-dev. This runs a web server hosting your local version of jscoq on port 8000. You can stop it using sudo docker container stop jscoq-dev.

• After the container has been started, run sudo docker exec -it jscoq-dev bash -c "cd /root/jscoq && ./etc/toolchain-setup.sh && make coq && make jscoq && npm link" to compile everything for the first time

Compiling jscoq

• Make sure the container is started by running sudo docker container start jscoq-dev

• Run sudo docker exec -it jscoq-dev bash : you are now in a shell inside the container.

• cd /root/jscoq to enter to the jscoq directory source. This is a bind mount, meaning /root/jscoq inside the container is actually the same directory as the git repository on your machine. You can edit the source code of jscoq outside of the container and the changes will be reflected inside the container.

• To compile jscoq, run make jscoq. The result will be saved in _build/jscoq+32bit. You can upload this directory to a web server; it contains an index.html which should work in your browser.

• You don't need to copy this directory to a web server to test your version, the docker container runs a web server for this purpose.

Adding your own Coq files

You can add your own Coq files in the directory ./addons/teach/workdir/theories/ if you recompile jscoq (using make jscoq) they will be compiled. You can compile only your files using make addons at the root of the directory inside the container.

Then, you will be able to use From Teach Require Import YourFile in jscoq.

Creating your own worksheets

You can modify index.html to create your own worksheet. (TODO: expand on this).