diff --git a/coq-interval/benchmarks/README.md b/coq-interval/benchmarks/README.md index eadf9e8..1f2e72c 100644 --- 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,8 +28,9 @@ 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' @@ -35,7 +38,7 @@ following alias in your `~/.bashrc` file: 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 @@ -43,11 +46,11 @@ prompt protection. ```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 ``` @@ -55,9 +58,9 @@ 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 index a67609f..97ec9c9 100644 --- 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,8 +28,9 @@ 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' @@ -35,7 +38,7 @@ following alias in your `~/.bashrc` file: 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. ```