Commands

Commands

Docker

List docker elements

docker container ls -a
docker image ls -a
docker volume ls

Stop all containers

docker kill $(docker ps -q)

Remove / delete all docker elements (be careful!)

docker rm $(docker ps -a -q)
docker rmi -f $(docker images -a -q)
docker system prune -a

Source: https://www.digitalocean.com/community/tutorials/how-to-remove-docker-images-containers-and-volumes

Change host port of docker container

• Get ID of container: sudo docker inspect <CONTAINERNAME> | grep Id
• Change port: sudo nano /var/lib/docker/containers/<CONTAINERID>/hostconfig.json
• Restart docker daemon

Source: https://stackoverflow.com/questions/19335444/how-do-i-assign-a-port-mapping-to-an-existing-docker-container/38783433#38783433

nbgrader import example

nbgrader db student import --db=sqlite:////home/nbgadmin/gradebook.db /full/path/to/file.csv

id,last_name,first_name
student2,Smith,Claudius
student1,Student1Last,Student1First

nbgrader export example

nbgrader export --db="sqlite:////tmp/gradebook.db" --to pggrades.csv