[ERROR] Package dune has no version 3.15.3.

[lengyijun]

./coq_platform_make.sh
====================== JUST COQ OR COMPLETE PLATFORM ? =======================
This script installs the Coq Platform release 2025.01.0, that is:

- the Coq compiler and Coq's standard library (b)
- optionally CoqIDE, a GTK3 based graphical user interface (i)
- optionally various widely used Coq libraries and plugins (f)
- optionally an extended set of Coq libraries and plugins (x)

The script uses opam, the OCaml package manager, to do all the work.
In case opam is not yet installed, it will install opam.
A new opam switch will be created unless a Coq Platform switch already exists.

This script is tested on Windows 10, macOS and many Linux variants.

The script compiles everything from sources, which might takes less than one
hour on a fast machine with lot's of RAM, or up to 6 hours with little RAM.

Instead of installing the full or extended Coq Platform now, you can install
just Coq (+ CoqIDE) and install additional packages via opam later as needed.
You should install CoqIDE unless you know what VSCoq or Proof General is.
====================== JUST COQ OR COMPLETE PLATFORM ? =======================
Install full (f), extended (x), base (b) or IDE (i)? (f/x/b/i/c=cancel) f

========================= SELECT PACKAGE_PICK VERSION ==========================
The Coq Platform allows to install the latest release version of Coq, but also
older or development versions of Coq. Besides the Coq version, you can choose
a 'package pick', that is a selection of specific versions of Coq libraries,
plugins and tools. For some versions of Coq several package picks are available.
Package picks with the same release date for different Coq versions are made
as compatible as possible.
You can install several versions of Coq in parallel, which simplifies porting of
developments. You can use "opam switch" to switch between Coq versions.

The following Coq versions and package picks are available:
(1): Coq 8.20.1 (released Jan 2025) with the first package pick from Jan 2025
(2): Coq 8.19.2 (released Jun 2024) with the first package pick from Oct 2024
(3): Coq 8.18.0 (released Sep 2023) with the first package pick from Nov 2023
(4): Coq 8.17.1 (released Jun 2023) with the first package pick from Aug 2023
(5): Coq 8.16.1 (released Nov 2022) with the first package pick from Sep 2022
(6): Coq 8.15.2 (released Jun 2022) with the first package pick from Apr 2022
(7): Coq 8.14.1 (released Nov 2021) with the first package pick from Jan 2022
(8): Coq 8.13.2 (released Apr 2021) with the first package pick from Feb 2021
(9): Coq 8.12.2 (released Dec 2020) with the first package pick from Dec 2020
(10): Coq 8.19.2+ltac2-debugger (released Nov 2024)
(11): Coq dev (latest master of all packages)
(12): Coq 8.18.0 (released Sep 2023) with a package pick based on mathcomp 2.1
(13): Coq 8.16.1 (released Nov 2022) with an updated package pick from from Aug 2023
(14): Coq 8.15.2 (released Jun 2022) with an updated package pick from Sep 2022
(15): Coq 8.14.1 (released Nov 2021) with an updated package pick from Apr 2022
(16): Coq 8.13.2 (released Apr 2021) with an updated package pick from Jan 2022
(17): Coq 8.13.2 (released Apr 2021) with an extended package pick from Sep 2021

Please select a package pick by entering the number shown at the begin of a line.
========================= SELECT PACKAGE_PICK VERSION ==========================
Select package list (number in 1..17, c=cancel) 2

=============================== PARALLEL BUILD ===============================
The Coq Platform opam build has two levels of parallelism:

- parallel build of (independent) opam packages
- parallel build inside the make of each opam package

Since a single coqc call can take more than 1 GB of RAM and since the two
above kinds of parallelism multiply, the total amount of memory can be large.
But it is not as bad as one might expect: tests show that a full parallel
build takes less than 14GB of RAM with 15 parallel make jobs.

With 32 GB of RAM a parallel package build with 12 make jobs is recommended.
With 16 GB of RAM a parallel package build with 4 make jobs is recommended.
With 8 GB of RAM a sequential package build with 4 make jobs is recommended.
With 4 GB+1GB swap a sequential package build with 2 make jobs is recommended.
With less RAM, you might have to remove failing packages, e.g. VST.
In order to remove packages, just edit the file in the package_picks folder.

In case these recommendations don't work for you, please report an issue at:
https://github.com/coq/platform/issues
=============================== PARALLEL BUILD ===============================
Build opam packages parallel (p) or sequential (s)? (p/s/c=cancel) s

Number of parallel make jobs (number in 1..16, c=cancel) 1

================================== COMPCERT ==================================
The Coq Platform installs the formally verified C compiler CompCert.

CompCert is *not* free / open source software, but may be used for research and
evaluation purposes. Please clarify the license at:

https://github.com/AbsInt/CompCert/blob/master/LICENSE

In case you intend to use CompCert and your intended usage is in compliance
with the above license, please select "y" below, otherwise "n".

Please note that CompCert is required for the (open source) C verification
tool chain VST. If you don't install CompCert, you can't install VST.
If you want to use VST with the provided VST examples only, you require only
parts of CompCert, which are dual licensed and open source. In case you want
to verify your own C code with VST, you need non open source parts of
CompCert, notably the clightgen program. CompCert does not support
installing only its open source parts, since evaluation usage is explicitly
allowed in the license (see link above).
================================== COMPCERT ==================================
Install non open source SW CompCert (y) or (n)? (y/n/c=cancel) y

=============================== LARGE PACKAGES ===============================
The Coq Platform includes several packages which take a while to build.

The most time consuming packages are

  coq-vst:     a toolchain for verifying C code
  coq-unimath: a library for univalent mathematics
  coq-fiat-crypto, coq-bedrock2 and dependencies: (64 bit platforms only)
               Framework for correct by design code generation
               Cryptographic Primitive Code Generation by Fiat

Depending on your computer each of these packages takes between 10 minutes
and 2 hours to build. With just 4GB of RAM these packages might even fail
to build. In case you do not plan to use these packages, you can skip them
now. You can install them any time later with:

  opam install "package-name"
=============================== LARGE PACKAGES ===============================
Include (i) exclude (e) or select (s) large packages? (i/e/s/c=cancel) i

===== INSTALLING OPAM =====
## Downloading opam 2.3.0 for linux on x86_64...
## Downloaded.
## Where should it be installed ? [/usr/local/bin] Write access to '/usr/local/bin' required, using 'sudo'.
Command: install -m 755 /tmp/opam-2.3.0-x86_64-linux /usr/local/bin/opam
[sudo] password for lengyijun:
## opam 2.3.0 installed to /usr/local/bin
## Run this script again with '--restore ' to revert.
OPAM is now /usr/local/bin/opam with version 2.3.0
/usr/local/bin/opam
===== INITIALIZING OPAM =====
No configuration file found, using built-in defaults.
Checking for available remotes: rsync and local, git.
  - you won't be able to use mercurial repositories unless you install the hg command on your system.
  - you won't be able to use darcs repositories unless you install the darcs command on your system.


<><> Fetching repository information ><><><><><><><><><><><><><><><><><><><><><>
[default] Initialised

User configuration:
  Updating ~/.profile.
[NOTE] Make sure that ~/.profile is well sourced in your ~/.bashrc.

  Added 9 lines after line 31 in ~/.profile.
===== CREATE OPAM SWITCH =====
[CP.2025.01.0.patch_ocaml] Initialised
[CP.2025.01.0.patch_coq-released] Initialised
[CP.2025.01.0.patch_coq-dev] Initialised
[coq-released] Initialised
[coq-core-dev] Initialised
[coq-extra-dev] Initialised

<><> Installing new switch packages <><><><><><><><><><><><><><><><><><><><><><>
Switch invariant: ["ocaml-variants" {= "4.14.2+options"} "ocaml-option-flambda"]

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
∗ installed base-bigarray.base
∗ installed base-threads.base
∗ installed base-unix.base
∗ installed ocaml-option-flambda.1
⬇ retrieved ocaml-config.2  (2 extra sources)
⬇ retrieved ocaml-config.2  (2 extra sources)
⬇ retrieved ocaml-variants.4.14.2+options  (https://opam.ocaml.org/cache)
∗ installed ocaml-variants.4.14.2+options
∗ installed ocaml-config.2
∗ installed ocaml.4.14.2
Done.
# To update the current shell environment, run: eval $(opam env --switch=CP.2025.01.0~8.19~2024.10)
=== OPAM SWITCHES ===
#  switch                     compiler                                              description
→  CP.2025.01.0~8.19~2024.10  ocaml-option-flambda.1,ocaml-variants.4.14.2+options  Coq 8.19.2 (released Jun 2024) with the first package pick from Oct 2024

[NOTE] Current switch is set locally through the OPAMSWITCH variable.
       The current global system switch is unset.
=== OPAM REPOSITORIES ===
[NOTE] These are the repositories in use by the current switch. Use '--all' to see all configured repositories.

<><> Repository configuration for switch CP.2025.01.0~8.19~2024.10 ><><><><><><>
 1 CP.2025.01.0.patch_coq-released file:///home/lengyijun/2025.01.0/platform-2025.01.0/opam/opam-coq-archive/released
 2 CP.2025.01.0.patch_ocaml        file:///home/lengyijun/2025.01.0/platform-2025.01.0/opam/opam-repository
 3 coq-released                    https://coq.inria.fr/opam/released
 4 default                         https://opam.ocaml.org
=== OPAM PACKAGES ===
# Packages matching: installed
# Name               # Installed    # Synopsis
base-bigarray        base
base-threads         base
base-unix            base
ocaml                4.14.2         The OCaml compiler (virtual package)
ocaml-config         2              OCaml Switch Configuration
ocaml-option-flambda 1              Set OCaml to be compiled with flambda activated
ocaml-variants       4.14.2+options Official release of OCaml 4.14.2
Cleaning up switch CP.2025.01.0~8.19~2024.10
===== UPDATE OPAM REPOSITORIES =====

<><> Updating package repositories ><><><><><><><><><><><><><><><><><><><><><><>
[CP.2025.01.0.patch_coq-released] no changes from file:///home/lengyijun/2025.01.0/platform-2025.01.0/opam/opam-coq-archive/released
[CP.2025.01.0.patch_ocaml] no changes from file:///home/lengyijun/2025.01.0/platform-2025.01.0/opam/opam-repository
[default] no changes from https://opam.ocaml.org
[coq-released] no changes from https://coq.inria.fr/opam/released
===== FINAL OPAM SANITY CHECKS =====
[NOTE] These are the repositories in use by the current switch. Use '--all' to see all configured repositories.
[NOTE] These are the repositories in use by the current switch. Use '--all' to see all configured repositories.
[NOTE] These are the repositories in use by the current switch. Use '--all' to see all configured repositories.
[NOTE] These are the repositories in use by the current switch. Use '--all' to see all configured repositories.
===== INSTALL PREREQUISITES (PARALLEL) =====
[ERROR] Package dune has no version 3.15.3.
[ERROR] Package dune-configurator has no version 3.15.3.
[ERROR] Package elpi has no version 1.18.2.

[Zimmi48]

I just requested version 3.15.3 of Dune to be reintroduced in the opam repository. For the future, to be more reproducible and avoid this kind of issues, I think the Platform scripts should pin the specific commit of the opam repository that is used (opam repo set-url default git+https://github.com/ocaml/opam-repository.git#$commit-hash).

[MSoegtropIMC]

We still need to adjust to the new opam regime. For all legacy builds we will include the legacy opam repo. For the latest builds we will insist that packages are not removed. IMHO it is reasonable to expect that packages are available for at least 1 year.

@Zimmi48 : thank!

[MSoegtropIMC]

The branch of this PR (mostly) works - see CI status: #473

[Zimmi48]

Apparently, this error is not yet solved. I focused too much on the title, but the error also contained:

[ERROR] Package dune-configurator has no version 3.15.3.
[ERROR] Package elpi has no version 1.18.2.

and now a user reports an error related with these two missing versions on Zulip: #Rocq users > Install Ubuntu 24.04 fails ; dune.configurator, elpi

@hannesm: would you mind also restoring these two package versions?

(Since the Rocq Platform is the recommended installation method, and this is still the latest and default version that users get through this means, it basically means that users using this installation method are preventing from installing Rocq.)

[MSoegtropIMC]

This is fixed in main since Tuesday (CI is green).

[MSoegtropIMC]

(I leave this open for a few more days so that people find it more easily).