Ursus Docker Image

Docker is a set of platform as a service (PaaS) products that use OS-level virtualization to deliver software in packages called containers.[1]

Before before interaction you probablly have got tar (let call it pruvendo.tar) file with needed lib packaging into Docker image.

Therefore first step for working in the container is

> docker load < pruvendo.tar

And we can see it using

> docker images
REPOSITORY TAG    IMAGE ID CREATED SIZE
pruvendo   latest bdd...   ...     3.59GB

Ok, let's run it :) where

docker run -p 81 -it --entrypoint=/bin/bash pruvendo
  1. -p remote port
  2. -it interactive mode

As said before pruvendo images consist of built coq libs and some example project (which called now preuvendo-erc20)

Of cource we can use container as dev area for our manipulation. For example, we could use VS Code for this goal.

  1. Install Docker extension
  2. do docker run -p 81 -it --entrypoint=/bin/bash pruvendo
  3. Attach Visual Studio Code alt text
  4. After that new window with this project appear which allow you to do something

Usefull tips:

  1. Allow write/read in the container
sudo chown -R username /path/to/working/directory

where username is coq

  1. VS Code allows to install VSCoq into the container and use it, but it doesn't it will ask you path which contains Coq bin default is /home/coq/.opam/4.13.1+flambda/bin/ or you can ask
> which coqc
/home/coq/.opam/4.13.1+flambda/bin/coqc

If which coqc doesn't work, so you probably need set env variables via

> source ~/.profile