docs(*/README.md): Update documentation

validsdp · Jul 28, 2023 · deb484a · deb484a
1 parent b011d49
commit deb484a
Show file tree

Hide file tree

Showing 2 changed files with 45 additions and 39 deletions.
diff --git a/coq-interval/benchmarks/README.md b/coq-interval/benchmarks/README.md
@@ -1,17 +1,19 @@
 # Benchmarks for primitive-floats in Coq
 
-Building
-[Coq with primitive-floats](https://github.com/coq/coq/pull/9867),
-then the
-[posdef_check tactic](https://github.com/validsdp/validsdp/blob/posdef_check/theories/posdef_check.v)
-with its dependencies takes around 75mn.
-
-To make the process faster and less tedious, we prepared Docker images
-gathering all this material prebuilt. They are available in this
-[GitLab CI registry](https://gitlab.com/erikmd/docker-coq-primitive-floats/container_registry)
-and these images are built from this
-[Dockerfile](https://gitlab.com/erikmd/docker-coq-primitive-floats/blob/1.0/Dockerfile)
-and [GitLab CI configuration](https://gitlab.com/erikmd/docker-coq-primitive-floats/blob/1.0/.gitlab-ci.yml).
+These benchmarks specifically focus on
+[Coq with primitive-floats](https://coq.github.io/doc/master/refman/language/core/primitive.html#primitive-floats), and the [coq-interval tactic](https://gitlab.inria.fr/coqinterval/interval).
+
+To make the process faster, less tedious, and reproducible, we
+prepared Docker images gathering all this material prebuilt.
+
+Building CoqInterval with its dependencies
+from a [coqorg/coq](https://hub.docker.com/r/coqorg/coq) image takes around 17mn.
+
+The resulting images are available in this
+[GitLab CI registry](https://gitlab.com/erikmd/docker-coq-interval-primitive-floats/container_registry),
+they are built from this
+[Dockerfile](https://gitlab.com/erikmd/docker-coq-interval-primitive-floats/-/blob/2.0/Dockerfile)
+and [GitLab CI configuration](https://gitlab.com/erikmd/docker-coq-interval-primitive-floats/-/blob/2.0/.gitlab-ci.yml).
 
 The sequel of this document describes how to install Docker, and how
 to run the benchmarks using Docker.
@@ -26,38 +28,39 @@ Follow the official instructions and install [Docker Engine](https://docs.docker
 
 As the Docker daemon socket is owned by `root`, you will need to
 prepend all `docker` CLI commands by `sudo`.
-To do this automatically, a standard practice consists in adding the
-following alias in your `~/.bashrc` file:
+To do this automatically, a standard practice consists in
+[adding an alias](https://stackoverflow.com/a/65956808/9164010)
+in one's `~/.bashrc` file, e.g.:
 
     alias docker='sudo docker'
 
 **Warning:** to avoid this, some tutorials on the web suggest instead
 to add your default Linux user to the `docker` group. *Don't do this*
 on your personal workstation, because this would amount to provide the
 default user with `root` permissions without `sudo`-like password
-prompt protection.
+prompt protection nor auditing.
 [(cf. doc)](https://docs.docker.com/engine/security/security/#docker-daemon-attack-surface)
 
 ## Run the benchmarks using Docker
 
 ```bash
 # cd "the_folder_containing_this_README"
 
-docker pull registry.gitlab.com/erikmd/docker-coq-primitive-floats/master_coq-8.15-validsdp-1.0.1
-# note that this may take a while as the compressed size of this Docker image is 998 MB,
-# and you'll need enough space (in the '/' partition) as its uncompressed size is 3.14 GB.
+docker pull registry.gitlab.com/erikmd/docker-coq-interval-primitive-floats/master_coq-8.15-interval-4.5.2
+# note that this may take a while as the compressed size of this Docker image is 820 MB,
+# and you'll need enough space (in the '/' partition) as its uncompressed size is 2.55 GB.
 
-docker run --rm -it -v "$PWD:$PWD" -w "$PWD" registry.gitlab.com/erikmd/docker-coq-primitive-floats/master_coq-8.15-validsdp-1.0.1 make
+docker run --rm -it -v "$PWD:$PWD" -w "$PWD" registry.gitlab.com/erikmd/docker-coq-interval-primitive-floats/master_coq-8.15-interval-4.5.2 make
 
 pdflatex primfloat_comparison.tex
 ```
 
 To just experience with primitive floats in Coq, one can simply run:
 
 ```bash
-docker run --rm -it -v "$PWD:$PWD" -w "$PWD" registry.gitlab.com/erikmd/docker-coq-primitive-floats/master_coq-8.15-validsdp-1.0.1
-$ coqtop  # or emacs (with proof-general)
-Coq < Require Import Float.
+docker run --rm -it -v "$PWD:$PWD" -w "$PWD" registry.gitlab.com/erikmd/docker-coq-interval-primitive-floats/master_coq-8.15-interval-4.5.2
+$ coqtop
+Coq < Require Import Floats.
 Coq < Open Scope float_scope.
 Coq < Eval vm_compute in 1 + 0.5.
 ```
diff --git a/random_posdef_matrices/matrices/README.md b/random_posdef_matrices/matrices/README.md
@@ -1,17 +1,19 @@
 # Benchmarks for primitive-floats in Coq
 
-Building
-[Coq with primitive-floats](https://github.com/coq/coq/pull/9867),
-then the
-[posdef_check tactic](https://github.com/validsdp/validsdp/blob/posdef_check/theories/posdef_check.v)
-with its dependencies takes around 75mn.
-
-To make the process faster and less tedious, we prepared Docker images
-gathering all this material prebuilt. They are available in this
-[GitLab CI registry](https://gitlab.com/erikmd/docker-coq-primitive-floats/container_registry)
-and these images are built from this
-[Dockerfile](https://gitlab.com/erikmd/docker-coq-primitive-floats/blob/1.0/Dockerfile)
-and [GitLab CI configuration](https://gitlab.com/erikmd/docker-coq-primitive-floats/blob/1.0/.gitlab-ci.yml).
+These benchmarks specifically focus on
+[Coq with primitive-floats](https://coq.github.io/doc/master/refman/language/core/primitive.html#primitive-floats), and the [posdef_check tactic](https://github.com/validsdp/validsdp/blob/v1.0.1/theories/posdef_check.v) from ValidSDP.
+
+To make the process faster, less tedious, and reproducible, we
+prepared Docker images gathering all this material prebuilt.
+
+Building ValidSDP with its dependencies
+from a [coqorg/coq](https://hub.docker.com/r/coqorg/coq) image takes around 65mn.
+
+The resulting images are available in this
+[GitLab CI registry](https://gitlab.com/erikmd/docker-coq-primitive-floats/container_registry),
+they are built from this
+[Dockerfile](https://gitlab.com/erikmd/docker-coq-primitive-floats/-/blob/2.0/Dockerfile)
+and [GitLab CI configuration](https://gitlab.com/erikmd/docker-coq-primitive-floats/-/blob/2.0/.gitlab-ci.yml).
 
 The sequel of this document describes how to install Docker, and how
 to run the benchmarks using Docker.
@@ -26,16 +28,17 @@ Follow the official instructions and install [Docker Engine](https://docs.docker
 
 As the Docker daemon socket is owned by `root`, you will need to
 prepend all `docker` CLI commands by `sudo`.
-To do this automatically, a standard practice consists in adding the
-following alias in your `~/.bashrc` file:
+To do this automatically, a standard practice consists in
+[adding an alias](https://stackoverflow.com/a/65956808/9164010)
+in one's `~/.bashrc` file, e.g.:
 
     alias docker='sudo docker'
 
 **Warning:** to avoid this, some tutorials on the web suggest instead
 to add your default Linux user to the `docker` group. *Don't do this*
 on your personal workstation, because this would amount to provide the
 default user with `root` permissions without `sudo`-like password
-prompt protection.
+prompt protection nor auditing.
 [(cf. doc)](https://docs.docker.com/engine/security/security/#docker-daemon-attack-surface)
 
 ## Run the benchmarks using Docker
@@ -73,7 +76,7 @@ To just experience with primitive floats in Coq, one can simply run:
 ```bash
 docker run --rm -it -v "$PWD:$PWD" -w "$PWD" registry.gitlab.com/erikmd/docker-coq-primitive-floats/master_coq-8.15-validsdp-1.0.1
 $ coqtop  # or emacs (with proof-general)
-Coq < Require Import Float.
+Coq < Require Import Floats.
 Coq < Open Scope float_scope.
-Coq < Eval vm_compute in 1 + 0.5.
+Coq < Eval vm_compute in sqrt 2.
 ```