📅 * (2022-05-14 08:21:45 UTC)*

# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base conf-findutils 1 Virtual package relying on findutils conf-gmp 4 Virtual package relying on a GMP lib system installation coq dev Formal proof management system dune 3.1.1 Fast, portable, and opinionated build system ocaml 4.12.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.12.1 Official release 4.12.1 ocaml-config 2 OCaml Switch Configuration ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled ocamlfind 1.9.3 A library manager for OCaml zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers # opam file: opam-version: "2.0" maintainer: "assia.mahboubi@inria.fr" homepage: "https://github.com/coq-community/apery" dev-repo: "git+https://github.com/coq-community/apery.git" bug-reports: "https://github.com/coq-community/apery/issues" license: "CECILL-C" synopsis: "A formally verified proof in Coq, by computer algebra, that ζ(3) is irrational" description: """ This project contains a formal proof that the real number ζ(3), also known as Apéry's constant, is irrational. It follows roughly Apéry's original sketch of a proof. However, the recurrence relations constituting the crux of the proof have been guessed by a computer algebra program (in this case in Maple/Algolib). These relations are formally checked a posteriori, so that Coq's kernel remains the sole trusted code base.""" build: [make "-j%{jobs}%"] install: [make "install"] depends: [ "coq" {>= "8.11" & < "8.16~"} "coq-mathcomp-ssreflect" {>= "1.12" & < "1.15~"} "coq-mathcomp-algebra" "coq-mathcomp-field" "coq-coqeal" {>= "1.0.5"} "coq-mathcomp-real-closed" {>= "1.1.2"} "coq-mathcomp-bigenough" {>= "1.0.0"} ] tags: [ "category:Mathematics/Arithmetic and Number Theory/Number theory" "keyword:apery recurrence" "keyword:irrationality" "keyword:creative telescoping" "logpath:mathcomp.apery" "date:2022-02-03" ] authors: [ "Frédéric Chyzak" "Assia Mahboubi" "Thomas Sibut-Pinote" ] url { src: "https://github.com/coq-community/apery/archive/1.0.1.tar.gz" checksum: "sha512=3c768f31fe055a5cf98be6766d1a5f180e670d71fd3ad194523e414d4c2dba4ddfe49a24c98b3f7fe64a5366f5a531d2b6c0700387ff9b3b16a01df74bab0cfa" }

- Command
`true`

- Return code
- 0

Dry install with the current Coq version:

- Command
`opam install -y --show-action coq-mathcomp-apery.1.0.1 coq.dev`

- Return code
- 5120
- Output
[NOTE] Package coq is already installed (current version is dev). The following dependencies couldn't be met: - coq-mathcomp-apery -> coq < 8.16~ -> ocaml < 4.12 base of this switch (use `--unlock-base' to force) Your request can't be satisfied: - No available version of coq satisfies the constraints No solution found, exiting

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

- Command
`opam remove -y coq; opam install -y --show-action --unlock-base coq-mathcomp-apery.1.0.1`

- Return code
- 0

- Command
`true`

- Return code
- 0
- Duration
- 0 s

- Command
`true`

- Return code
- 0
- Duration
- 0 s

No files were installed.

- Command
`true`

- Return code
- 0
- Missing removes
- none
- Wrong removes
- none