diff --git a/.github/workflows/macos.yml b/.github/workflows/macos.yml index 16a0951379..a111350c2d 100644 --- a/.github/workflows/macos.yml +++ b/.github/workflows/macos.yml @@ -49,8 +49,8 @@ jobs: matrix: variant: # Keep this in sync with the Smoke test below + - "9.2~2026.08" - "9.1~2026.01" - - "9.0~2025.08" steps: - name: Setup Xcode 16.0 @@ -249,8 +249,8 @@ jobs: fail-fast: false matrix: variant: + - "9.2~2026.08" - "9.1~2026.01" - - "9.0~2025.08" steps: - name: Install bash @@ -286,43 +286,43 @@ jobs: cp -r "/Volumes/${DMG%%.dmg}/${APP_PREFIX}"*.app /Applications/ hdiutil detach "/Volumes/${DMG%%.dmg}/" - - name: "Smoke coqc" + - name: "Smoke compiler" shell: bash run: | cd /Applications/${APP_PREFIX}*.app/Contents/Resources/bin/ - # Try default coqc first - if ./coqc -v 2>/dev/null; then - exit 0 + # Try rocq first (Rocq 9.2+), then coqc (legacy) + if [ -f ./rocq ]; then + echo "Testing rocq compile --version" + ./rocq compile --version + elif [ -f ./coqc ]; then + echo "Testing coqc -v" + ./coqc -v + else + echo "Neither rocq nor coqc found in $(pwd)" + ls -la + exit 1 fi - echo "coqc -v failed, trying with library path detection for Rocq 9.0+" - - # Try to find library path and use -coqlib - for path in ../lib/coq ../lib/rocq ../lib/coq-stdlib; do - if [ -d "$path" ] && ([ -f "$path/theories/Init/Prelude.vo" ] || [ -f "$path/Init/Prelude.vo" ]); then - echo "Trying with -coqlib $path" - ./coqc -coqlib "$path" -v && exit 0 - fi - done - - # Last resort: boot mode - echo "Trying boot mode..." - ./coqc -boot -noinit -v - - name: "Run Macos smoke test kit" shell: bash run: | ls /Applications/${APP_PREFIX}*.app export PATH="$PATH:$(cd /Applications/${APP_PREFIX}*.app/Contents/Resources/bin/; pwd)" - # Prefer ROCQLIB for Rocq 9+, but keep COQLIB fallback - if ROCQLIB_TEMP=$(coqc -where 2>/dev/null); then + # Detect compiler and set COQLIB/ROCQLIB + if command -v rocq >/dev/null 2>&1; then + ROCQLIB_TEMP=$(rocq compile -where 2>/dev/null | tr -d '\r') export ROCQLIB="$ROCQLIB_TEMP" export COQLIB="$ROCQLIB_TEMP" echo "ROCQLIB set to: $ROCQLIB" + elif command -v coqc >/dev/null 2>&1; then + ROCQLIB_TEMP=$(coqc -where 2>/dev/null | tr -d '\r') + export ROCQLIB="$ROCQLIB_TEMP" + export COQLIB="$ROCQLIB_TEMP" + echo "COQLIB set to: $COQLIB" else - echo "Warning: coqc -where failed, ROCQLIB/COQLIB not set" + echo "Warning: neither rocq nor coqc found, ROCQLIB/COQLIB not set" export ROCQLIB="" export COQLIB="" fi diff --git a/.github/workflows/ubuntu.yml b/.github/workflows/ubuntu.yml index 6604c1257b..74be55cb3a 100644 --- a/.github/workflows/ubuntu.yml +++ b/.github/workflows/ubuntu.yml @@ -53,8 +53,8 @@ jobs: - id: set-matrix shell: bash run: | - FULL='["9.1~2026.01","9.0~2025.08","8.20~2025.01","8.19~2024.10","8.18~2023.11","8.17~2023.08","8.16~2022.09","8.15~2022.04","8.14~2022.01","8.13~2021.02","8.12"]' - SHORT='["9.1~2026.01","9.0~2025.08"]' + FULL='[ "9.2~2026.08", "9.1~2026.01","9.0~2025.08","8.20~2025.01","8.19~2024.10","8.18~2023.11","8.17~2023.08","8.16~2022.09","8.15~2022.04","8.14~2022.01","8.13~2021.02","8.12"]' + SHORT='["9.2~2026.08", "9.1~2026.01"]' REST='["8.20~2025.01","8.19~2024.10","8.18~2023.11","8.17~2023.08","8.16~2022.09","8.15~2022.04","8.14~2022.01","8.13~2021.02","8.12"]' if [[ "${{ github.event_name }}" != "pull_request" ]]; then diff --git a/.github/workflows/windows.yml b/.github/workflows/windows.yml index 725a5b7353..e6d3d0cf4c 100644 --- a/.github/workflows/windows.yml +++ b/.github/workflows/windows.yml @@ -51,8 +51,8 @@ jobs: - "64" variant: # Keep this in sync with the Smoke test below + - "9.2~2026.08" - "9.1~2026.01" - - "9.0~2025.08" steps: - name: Set git to use LF @@ -116,8 +116,8 @@ jobs: architecture: - "64" variant: + - "9.2~2026.08" - "9.1~2026.01" - - "9.0~2025.08" steps: - name: "Download Artifact" diff --git a/doc/README_Linux.md b/doc/README_Linux.md index c174232242..374d77b25b 100755 --- a/doc/README_Linux.md +++ b/doc/README_Linux.md @@ -12,15 +12,15 @@ This method is intended for experienced users, who may want to use opam to insta - OpenSuse: `sudo zypper in -t pattern devel_C_C++` - For CentOS and possibly RHEL some additional steps are required, see [CentOS](#centos) below. - Get the Rocq Platform scripts via either of these methods - - Most users should download and extract `https://github.com/coq/platform/archive/refs/tags/2025.08.3.zip`. - - Users which intend to contribute to Rocq Platform should use `git clone --branch 2025.08.3 https://github.com/rocq-prover/platform.git`. + - Most users should download and extract `https://github.com/coq/platform/archive/refs/tags/2026.07.0.zip`. + - Users which intend to contribute to Rocq Platform should use `git clone --branch 2026.07.0 https://github.com/rocq-prover/platform.git`. - Open a shell, navigate to the download folder and execute `coq_platform_make.sh`. - The system will ask for sudo permissions to install prerequisites _several times_ so the script is not fully unattended but all installations of dependencies are done directly after the initialization of the opam switch. - In case the script aborts e.g. cause of internet issues, just rerun the script. -- The script creates a new opam switch named e.g. CP.2025.08.0~9.0~2025.08 - the exact name depends on the Rocq version and package pick you selected. +- The script creates a new opam switch named e.g. RP.2026.07.0~9.1~2026.01 - the exact name depends on the Rocq version and package pick you selected. This means the script does not touch your existing opam setup unless you already have a switch of this name. - Use the following commands to activate this switch after opening a new shell: - - `opam switch CP.2025.08.3~9.0~2025.08` (note: the switch name might vary if you choose a different version of Rocq - please use `opam switch` to see a list of switch names) + - `opam switch RP.2026.07.0~9.1~2026.01` (note: the switch name might vary if you choose a different version of Rocq - please use `opam switch` to see a list of switch names) - `eval $(opam env)` - The second step can be automated by rerunning `opam init` - The main opam repositories for Rocq and OCaml developments are already added to the created opam switch, so it should be easy to install additional Rocq (or OCaml) packages. diff --git a/doc/README_Windows.md b/doc/README_Windows.md index faa6a1d539..42ca2c76fb 100755 --- a/doc/README_Windows.md +++ b/doc/README_Windows.md @@ -23,8 +23,8 @@ This method is intended for experienced users, who may want to use opam to insta - In case you install **Rocq Platform for the first time**: - Get the Rocq Platform scripts via either of these methods - - Most users should download and extract `https://github.com/coq/platform/archive/refs/tags/2025.08.3.zip`. - - Users which intend to contribute to Coq Platform should use `git clone --branch 2025.08.3 https://github.com/rocq-prover/platform.git`. + - Most users should download and extract `https://github.com/coq/platform/archive/refs/tags/2026.07.0.zip`. + - Users which intend to contribute to Coq Platform should use `git clone --branch 2026.07.0 https://github.com/rocq-prover/platform.git`. Please note that the scripts are CR/LF sensitive, so if you use a Windows git client (not a Cygwin git) you should set `git config --global core.autocrlf false` - which is anyway a good idea. - Open a DOS command window, navigate to the download folder and execute `coq_platform_make_windows.bat`. - This will ask for the Cygwin installation path and setup a fresh Cygwin as build host (the created Rocq is MinGW and runs without Cygwin). @@ -35,26 +35,26 @@ This method is intended for experienced users, who may want to use opam to insta - Start a cygwin shell via `C:\\Cygwin.bat` - Download, clone or pull the Rocq Platform: - Download zip and expand: - - `wget https://github.com/coq/platform/archive/refs/tags/2025.08.3.zip` - - `unzip 2025.08.3.zip` - - `mv 2025.08.3 platform-2025.08.3`` - - `cd platform-2025.08.3` + - `wget https://github.com/coq/platform/archive/refs/tags/2026.07.0.zip` + - `unzip 2026.07.0.zip` + - `mv 2025.08.3 platform-2026.07.0`` + - `cd platform-2026.07.0` - **OR** Git clone: - - `git clone --branch 2025.08.3 https://github.com/rocq-prover/platform.git` + - `git clone --branch 2026.07.0 https://github.com/rocq-prover/platform.git` - `cd platform` - **OR** Git update (with existing git Coq Platform repo): - `cd platform` - - `git fetch & git checkout 2025.08.3` + - `git fetch & git checkout 2026.07.0` - Run the main Rocq Platform installation script `coq_platform_make.sh` - The script will ask a few questions if no parameters are given and then run fully unattended. - The build time is between 1..5 hours, depending on CPU speed and RAM size. - In case the script aborts e.g. cause of internet issues, just rerun the batch file - it won't install Cygwin again (assuming you specify the same Cygwin destination folder). - The script has various options for configuring paths and proxies; see `example_coq_platform_make.bat` for an example command line. - The resulting Rocq installation is opam based and best used from the Cygwin prompt (started via `C:\\Cygwin.bat`) -- The script creates a new opam switch named e.g. CP.2025.08.3~8.20~2025.01 - the exact name depends on the Rocq version and package pick you selected you selected. +- The script creates a new opam switch named e.g. RP.2026.07.0~9.1~2026.01 - the exact name depends on the Rocq version and package pick you selected you selected. This means the script does not touch your existing opam setup unless you already have a switch of this name. - Use the following commands at the Cygwin prompt to activate this switch after opening a new shell: - - `opam switch CP.2025.08.3~9.0~2025.01` (note: the switch name might vary if you choose a different version of Rocq - please use `opam switch` to see a list of switch names) + - `opam switch RP.2026.07.0~9.1~2026.01` (note: the switch name might vary if you choose a different version of Rocq - please use `opam switch` to see a list of switch names) - `eval $(opam env)` - The second step can be automated by rerunning `opam init` - The main opam repositories for Rocq and OCaml developments are already added to the created opam switch, so it should be easy to install additional Rocq (or OCaml) packages. diff --git a/doc/README_macOS.md b/doc/README_macOS.md index 768d0db651..67a392e919 100644 --- a/doc/README_macOS.md +++ b/doc/README_macOS.md @@ -13,13 +13,13 @@ In case you want to use the fast path: - Download the DMG package from https://github.com/rocq-prover/platform/releases (click on "Assets" at the end of a release section). - Open the downloaded DMG package with a double click. -- Drag and drop the "Rocq-Platform~9.0~2025.08.app" icon on the link to the "Applications" folder. +- Drag and drop the "Rocq-Platform~9.1~2026.07.app" icon on the link to the "Applications" folder. - RocqIDE appears under `/Applications` in Finder and in Launcher. - The published installers are always signed by INRIA, but no notarized by Apple yet. This means that on first start of the application, you must right click on the Rocq application in the `Applications` folder and select `open`. Subsequently this is not required - the application can be started directly. - In case you want to use the installed `coqc` and other tools from the command line, you have three options: - Use the supplied `rocq-shell.command` file. This file is included in the top level folder of the `.dmg` file and can be dragged e.g. to the desktop and started from there. It opens a terminal window in which the environment variables `$PATH` and `$COQLIB` are set. These `.command` files always refer to a specifc version of Rocq, so you can keep multiple of these files for multiple versions of Rocq. - - Run `eval $(/Applications/Rocq-Platform~9.0~2025.08.app/Contents/Resources/bin/coq-env.sh)` in your shell. This will set the same environment variables as `rocq-shell.command` in the current shell. - - Add the folder `/Applications/Rocq-Platform~9.0~2025.08.app/Contents/Resources/bin` to your `$PATH`, e.g. by running `sudo sh -c "echo '/Applications/Rocq-Platform~9.0~2025.08.app/Contents/Resources/bin' > /etc/paths.d/coq"`. Please note that this method has two disadvantages: first it is difficult to switch between different versions of Rocq and second some tools require additional environment variables, e.g. `COQLIB` or `LD_LIBRARY_PATH` to be set. + - Run `eval $(/Applications/Rocq-Platform~9.1~2026.07.app/Contents/Resources/bin/coq-env.sh)` in your shell. This will set the same environment variables as `rocq-shell.command` in the current shell. + - Add the folder `/Applications/Rocq-Platform~9.1~2026.07.app/Contents/Resources/bin` to your `$PATH`, e.g. by running `sudo sh -c "echo '/Applications/Rocq-Platform~9.1~2026.07.app/Contents/Resources/bin' > /etc/paths.d/coq"`. Please note that this method has two disadvantages: first it is difficult to switch between different versions of Rocq and second some tools require additional environment variables, e.g. `COQLIB` or `LD_LIBRARY_PATH` to be set. - If you want to inspect the installed content, right click the `Rocq_Platform` app in `/Applications` in Finder and select `Show Package Contents`. **A note to lecturers:** it is easy to create a customized Windows installer from an opam switch - see [Customized Installers](FAQ-customized-installers.md) @@ -37,15 +37,15 @@ This method is intended for experienced users, who may want to use opam to insta - If you have neither Homebrew nor MacPorts installed, read the section [Homebrew and MacPorts](#homebrew-and-macports) below. - If you have Homebrew installed, read the section [Homebrew issues and workarounds](#homebrew-issues-and-workarounds) below. - Get the Rocq Platform scripts via either of these methods - - Most users should download and extract `https://github.com/coq/platform/archive/refs/tags/2025.08.3.zip`. - - Users which intend to contribute to Rocq Platform should use `git clone --branch 2025.08.3 https://github.com/rocq-prover/platform.git`. + - Most users should download and extract `https://github.com/coq/platform/archive/refs/tags/2026.07.0.zip`. + - Users which intend to contribute to Rocq Platform should use `git clone --branch 2026.07.0 https://github.com/rocq-prover/platform.git`. - Open a shell, navigate to the download folder and execute `coq_platform_make.sh`. - If you are using MacPorts, the system will ask once for sudo permissions to install prerequisites after installing OCaml (5..20 minutes after script start). - In case the script aborts e.g. cause of internet issues, just rerun the script. -- The script creates a new opam switch named e.g. CP.2025.01.0~8.20~2025.01 - the exact name depends on the Rocq version and package pick you selected. +- The script creates a new opam switch named e.g. RP.2026.07.0~9.1~2026.01 - the exact name depends on the Rocq version and package pick you selected. This means the script does not touch your existing opam setup unless you already have a switch of this name. - Use the following commands to activate this switch after opening a new shell: - - `opam switch CP.2025.08.3~9.0~2025.01` (note: the switch name might vary if you choose a different version of Rocq - please use `opam switch` to see a list of switch names) + - `opam switch RP.2026.07.0~9.1~2026.01` (note: the switch name might vary if you choose a different version of Rocq - please use `opam switch` to see a list of switch names) - `eval $(opam env)` - The second step can be automated by rerunning `opam init` - The main opam repositories for Rocq and OCaml developments are already added to the created opam switch, so it should be easy to install additional Coq (or OCaml) packages. diff --git a/doc/README~9.1~2026.01.md b/doc/README~9.1~2026.01.md index 3ff588e7c2..2dfe7f3532 100644 --- a/doc/README~9.1~2026.01.md +++ b/doc/README~9.1~2026.01.md @@ -1,5 +1,4 @@ - -# Coq Platform 2026.02.0 providing Rocq 9.1 (released January 2026) with the preview package pick from Mars 2026 +# Coq Platform 2026.07.0 providing Rocq 9.1 (released January 2026) with the preview package pick from Mars 2026 The [Coq proof assistant](https://coq.inria.fr) provides a formal language to write mathematical definitions, executable algorithms, and theorems, together @@ -9,7 +8,7 @@ The [Coq Platform](https://github.com/coq/platform) is a distribution of the Coq interactive prover together with a selection of Coq libraries and plugins. The Coq Platform supports to install several versions of Coq (also in parallel). -This README file is for **Coq Platform 2026.02.0 with Coq 9.1+rc1**. +This README file is for **Coq Platform 2026.07.0 with Coq 9.1+rc1**. The README files for other versions are linked in the main [README](https://github.com/coq/platform/blob/main/README.md). This version of Rocq Platform 2026.01 includes Rocq 9.1 from January 2026.This is a **preview release** of the Rocq Platform for packages maintainers @@ -22,8 +21,6 @@ The sections below provide a short description of each level and the list of packages included in each level. Packaged versions of the Coq Platform usually contain the **extended** set with all optional packages. - - **Note on non-free licenses:** The Coq Platform contains software with **non-free licenses which do not allow commercial use without purchasing a license**, notably the **coq-compcert** package. Please study the package licenses given @@ -34,7 +31,7 @@ plan to use these packages. The license information given below is obtained from opam. The Coq Platform team does no double check this information. -**Note on multiple licenses:** +**Note on multiple licenses:** In case several licenses are given below, it is not clearly specified what this means. It could mean that parts of the software use one license while other parts use another license. It could also mean that you can choose between the given licenses. @@ -46,7 +43,7 @@ Please clarify the details with the homepage of the package.
-## **Coq Platform 2026.02.0 with Coq 9.1+rc1 "base level"** +## **Coq Platform 2026.07.0 with Coq 9.1+rc1 "base level"** The **base level** is mostly intended as a basis for custom installations using opam and contains the following package(s): @@ -113,7 +110,7 @@ opam and contains the following package(s):
-## **Coq Platform 2026.02.0 with Coq 9.1+rc1 "IDE level"** +## **Coq Platform 2026.07.0 with Coq 9.1+rc1 "IDE level"** The **IDE level** adds an interactive development environment to the **base level**. @@ -156,7 +153,7 @@ The **IDE level** contains the following package(s):
-## **Coq Platform 2026.02.0 with Coq 9.1+rc1 "full level"** +## **Coq Platform 2026.07.0 with Coq 9.1+rc1 "full level"** The **full level** adds many commonly used coq libraries, plug-ins and developments. @@ -934,7 +931,7 @@ The **full level** contains the following packages:
-## **Coq Platform 2026.02.0 with Coq 9.1+rc1 "optional packages"** +## **Coq Platform 2026.07.0 with Coq 9.1+rc1 "optional packages"** The **optional** packages have the same maturity and maintenance level as the packages in the full level, but either take a rather long time to build or have @@ -994,7 +991,7 @@ The following packages are **optional**:
-## **Coq Platform 2026.02.0 with Coq 9.1+rc1 "extended level"** +## **Coq Platform 2026.07.0 with Coq 9.1+rc1 "extended level"** The **extended level** contains packages which are in a beta stage or otherwise don't yet have the level of maturity or support required for inclusion in the @@ -1687,4 +1684,3 @@ Please refer to the linked opam package and/or your system package manager for d
description
- diff --git a/macos/create_installer_macos.sh b/macos/create_installer_macos.sh index acbb3161e6..1c66bf9785 100755 --- a/macos/create_installer_macos.sh +++ b/macos/create_installer_macos.sh @@ -101,7 +101,28 @@ echo "##### Coq Platform release = ${COQ_PLATFORM_RELEASE} version = ${COQ_PLATF # Get installed version of coq (otherwise opam source gives the latest) -if [ "$(opam show -f version coq | cut -d. -f1)" -ge 9 ]; then +if opam show -f version rocq-core >/dev/null 2>&1; then + rocq_major=$(opam show -f version rocq-core | cut -d. -f1) +else + rocq_major=0 +fi + +if opam show -f version coq >/dev/null 2>&1; then + coq_major=$(opam show -f version coq | cut -d. -f1) +else + coq_major=0 +fi + +if [ "$rocq_major" -ge 9 ] 2>/dev/null; then + echo "Rocq 9.x+ detected, sourcing components individually" + for pkg in rocq-core rocq-stdlib coqide-server rocq-runtime; do + if opam show -f version "$pkg" >/dev/null 2>&1; then + version=$(opam show -f version "$pkg") + echo "→ Sourcing ${pkg}.${version}" + opam source --dir=${pkg}.${version} ${pkg}.${version} + fi + done +elif [ "$coq_major" -ge 9 ] 2>/dev/null; then echo "Coq 9.x+ detected, sourcing components individually" for pkg in coq-core coq-stdlib coqide-server rocq-runtime; do if opam show -f version "$pkg" >/dev/null 2>&1; then @@ -118,7 +139,11 @@ fi ##### Get the version of Coq ##### -COQ_VERSION=$(coqc --print-version | cut -d ' ' -f 1) +if command -v rocq >/dev/null 2>&1; then + COQ_VERSION=$(rocq compile --print-version | cut -d ' ' -f 1) +else + COQ_VERSION=$(coqc --print-version | cut -d ' ' -f 1) +fi # The MacOS version needs to be purely numeric (no +beta) # As it looks in current Coq releases beta versions are called .0 diff --git a/package_picks/coq_platform_release.sh b/package_picks/coq_platform_release.sh index e9469545f8..8865e811aa 100644 --- a/package_picks/coq_platform_release.sh +++ b/package_picks/coq_platform_release.sh @@ -10,4 +10,4 @@ ###################### SET THE PLATFORM VERSION NAME ##################### -COQ_PLATFORM_RELEASE="2026.02.0" +COQ_PLATFORM_RELEASE="2026.08.0" diff --git a/package_picks/package-pick-9.1~2026.01.sh b/package_picks/package-pick-9.1~2026.01.sh index 834b15eb3e..f32f58baf9 100644 --- a/package_picks/package-pick-9.1~2026.01.sh +++ b/package_picks/package-pick-9.1~2026.01.sh @@ -12,7 +12,7 @@ # The two lines below are used by the package selection script COQ_PLATFORM_VERSION_TITLE="Rocq 9.1 (released January 2026) with the preview package pick from Mars 2026" -COQ_PLATFORM_VERSION_SORTORDER="1" +COQ_PLATFORM_VERSION_SORTORDER="2" # The package list name is the final part of the opam switch name. # It is usually either empty ot starts with ~. @@ -147,7 +147,7 @@ then PACKAGES="${PACKAGES} coq-coqeal.2.1.1" # modified PACKAGES="${PACKAGES} rocq-libhyps.4.0" - #PACKAGES="${PACKAGES} coq-itauto.8.20.0" # error + PACKAGES="${PACKAGES} coq-itauto.9.1.0" # General mathematics (which requires one of the above tools) PACKAGES="${PACKAGES} coq-mathcomp-analysis.1.16.0" # modified diff --git a/package_picks/package-pick-9.2~2026.08.sh b/package_picks/package-pick-9.2~2026.08.sh new file mode 100644 index 0000000000..5e2d8916ae --- /dev/null +++ b/package_picks/package-pick-9.2~2026.08.sh @@ -0,0 +1,65 @@ +#!/usr/bin/env bash + +###################### COPYRIGHT/COPYLEFT ###################### + +# (C) 2020..2022 Michael Soegtrop + +# Released to the public under the +# Creative Commons CC0 1.0 Universal License +# See https://creativecommons.org/publicdomain/zero/1.0/legalcode.txt + +###################### CONTROL VARIABLES ##################### + +# The two lines below are used by the package selection script +COQ_PLATFORM_VERSION_TITLE="Rocq 9.2 (released Mars 2026) with the preview package pick from August 2026" +COQ_PLATFORM_VERSION_SORTORDER="1" + +# The package list name is the final part of the opam switch name. +# It is usually either empty ot starts with ~. +# It might also be used for installer package names, but with ~ replaced by _ +# It is also used for version specific file selections in the smoke test kit. +COQ_PLATFORM_PACKAGE_PICK_POSTFIX="~9.2~2026.08" + +# The corresponding Coq development branch and tag +COQ_PLATFORM_COQ_BRANCH="v9.2" +COQ_PLATFORM_COQ_TAG="9.2+rc1" + +# This controls if opam repositories for development packages are selected +COQ_PLATFORM_USE_DEV_REPOSITORY="Y" + +# This extended descriptions is used for readme files +COQ_PLATFORM_VERSION_DESCRIPTION="This version of Rocq Platform 2026.08 includes Rocq 9.2 from January 2026." +COQ_PLATFORM_VERSION_DESCRIPTION+='This is a **preview release** of the Rocq Platform for packages maintainers' + +# The OCaml version to use for this pick (just the version number - options are elaborated in a platform dependent way) +COQ_PLATFORM_OCAML_VERSION="4.14.2" + +###################### PACKAGE SELECTION ##################### + +PACKAGES="" + +# - Comment out packages you do not want. +# - Packages which take a long time to build should be given last. +# There is some evidence that they are built early then. +# - Versions ending with ~flex are identical to the opam package without the +# ~flex extension, except that version restrictions have been relaxed. + +########## BASE PACKAGES ########## + +# Coq needs a patched ocamlfind to be relocatable by installers +PACKAGES="${PACKAGES} PIN.ocamlfind.1.9.8+relocatable" # TODO port patch to 1.9.6 # modified +# Since dune does support Coq, it is explicitly selected +PACKAGES="${PACKAGES} PIN.dune.3.21.0" # 3.17.2 has issues on Windows: cairo doesn't find cairo.h +PACKAGES="${PACKAGES} PIN.dune-configurator.3.21.0" +# The Coq compiler coqc and the Coq standard library +PACKAGES="${PACKAGES} PIN.rocq-core.9.2.0" +PACKAGES="${PACKAGES} PIN.rocq-stdlib.9.1.0" + +########## IDE PACKAGES ########## + +# GTK based IDE for Coq - alternatives are VSCoq and Proofgeneral for Emacs +if [[ "${COQ_PLATFORM_EXTENT}" =~ ^[iIfFxX] ]] +then +PACKAGES="${PACKAGES} rocqide.9.2.0" +PACKAGES="${PACKAGES} vsrocq-language-server.2.4.3+1" +fi \ No newline at end of file diff --git a/shell_scripts/ask_packagelist.sh b/shell_scripts/ask_packagelist.sh index c1d48b8fee..c74ca7e8a4 100644 --- a/shell_scripts/ask_packagelist.sh +++ b/shell_scripts/ask_packagelist.sh @@ -16,16 +16,16 @@ if [ -z "${COQ_PLATFORM_PACKAGE_PICK_FILE:+x}" ] then cat < /dev/null; then - if [ -f /Applications/PRODUCTNAME.app/Contents/Resources/bin/coqc ]; then - echo "Using coqc from '/Applications/PRODUCTNAME.app/Contents/Resources/bin'" - # Initialize PATH, DYLD_LIBRARY_PATH, etc. - eval $(/Applications/PRODUCTNAME.app/Contents/Resources/bin/coq-env.sh) - elif [ -f /snap/coq-prover/current/coq-platform/bin/coqc ]; then - echo "Using coqc from '/snap/coq-prover/current/coq-platform/bin'" - echo "ATTENTION: coq-hammer requires LD_LIBRARY_PATH to be set to lib/stublibs!" - export PATH='/snap/coq-prover/current/coq-platform/bin':"$PATH" - export LD_LIBRARY_PATH='/snap/coq-prover/current/coq-platform/lib/stublibs':"${LD_LIBRARY_PATH:-}" - else - echo "This script expects that coqc is in the PATH" - echo "or on macOS installed under /Applications/PRODUCTNAME.app/" - echo "or on Linux with Snap installed under /snap/coq-prover/current/" - exit 1 - fi - else - # coqc is already in PATH; if a coq-env.sh sits next to it (mac app), source it for DYLD/etc. + # Detect compiler command: "rocq compile" (Rocq 9.2+) or "coqc" (legacy) + COQC="" + if command -v rocq &> /dev/null; then + COQC="rocq compile" + echo "Using Rocq compiler: rocq compile" + elif command -v coqc &> /dev/null; then + COQC="coqc" + # coqc is in PATH; if a coq-env.sh sits next to it (mac app), source it for DYLD/etc. COQ_BINDIR="$(dirname "$(command -v coqc)")" if [ -x "$COQ_BINDIR/coq-env.sh" ]; then echo "Sourcing environment from '$COQ_BINDIR/coq-env.sh'" eval "$("$COQ_BINDIR/coq-env.sh")" fi + elif [ -f /Applications/PRODUCTNAME.app/Contents/Resources/bin/coqc ]; then + COQC="coqc" + echo "Using coqc from '/Applications/PRODUCTNAME.app/Contents/Resources/bin'" + eval $(/Applications/PRODUCTNAME.app/Contents/Resources/bin/coq-env.sh) + elif [ -f /snap/coq-prover/current/coq-platform/bin/coqc ]; then + COQC="coqc" + echo "Using coqc from '/snap/coq-prover/current/coq-platform/bin'" + echo "ATTENTION: coq-hammer requires LD_LIBRARY_PATH to be set to lib/stublibs!" + export PATH='/snap/coq-prover/current/coq-platform/bin':"$PATH" + export LD_LIBRARY_PATH='/snap/coq-prover/current/coq-platform/lib/stublibs':"${LD_LIBRARY_PATH:-}" + else + echo "This script expects that rocq or coqc is in the PATH" + echo "or on macOS installed under /Applications/PRODUCTNAME.app/" + echo "or on Linux with Snap installed under /snap/coq-prover/current/" + exit 1 fi - # Print Coq version - echo "Coq Version = $(coqc --version)" - - # Print Coq version - echo "Coq Version = $(coqc --version)" + # Print version + echo "Compiler version = $($COQC --version)" # set COQLIB variable - COQLIB="$(coqc -where | tr -d '\r')" + COQLIB="$($COQC -where | tr -d '\r')" echo "=== DEBUG ENV ===" echo "PATH=$PATH" - echo "coqc=$(command -v coqc)" + echo "COQC=$COQC" echo "COQLIB=$COQLIB" echo "ROCQLIB=${ROCQLIB:-}" echo "COQPATH=${COQPATH:-}" echo "PWD=$(pwd)" - echo - echo "=== DEBUG SEARCH MATHCOMP ===" - find "$COQLIB" -path "*mathcomp/ssreflect*" 2>/dev/null | head -50 || true - find "$(dirname "$COQLIB")" -path "*mathcomp/ssreflect*" 2>/dev/null | head -50 || true - find "$(dirname "$COQLIB")/../user-contrib" -path "*mathcomp/ssreflect*" 2>/dev/null | head -50 || true echo "=============================" # cd to smoke test folder @@ -292,17 +288,9 @@ cat <<-'EOH' | sed -e "s/PRODUCTNAME/Coq-Platform${COQ_PLATFORM_PACKAGE_PICK_POS echo "====================== Running test file $1 ======================" here="$(pwd)" cd "${1%/*}" - echo "coqc ${2:-} ${1##*/}" + echo "$COQC ${2:-} ${1##*/}" echo "PWD=$(pwd)" - echo "coqc=$(command -v coqc)" - echo "COQLIB=$(coqc -where | tr -d '\r')" - if [[ "$1" =~ mathcomp ]]; then - echo "--- mathcomp debug for $1 ---" - find "$(coqc -where | tr -d '\r')" -path "*mathcomp/ssreflect*" 2>/dev/null | head -50 || true - find "$(dirname "$(coqc -where | tr -d '\r')")" -path "*mathcomp/ssreflect*" 2>/dev/null | head -50 || true - echo "-----------------------------" - fi - coqc ${2:-} "${1##*/}" + $COQC ${2:-} "${1##*/}" cd "$here" echo $'\n\n' fi @@ -526,6 +514,10 @@ done ##### Write footer of bash runner script ##### +# Always run a minimal compiler version check +echo '' >> $smoke_script +echo 'echo "====================== Compiler version check ======================"' >> $smoke_script +echo '$COQC --version' >> $smoke_script echo '' >> $smoke_script echo 'cd "$HERE"' >> $smoke_script echo 'echo "====================== SMOKE TEST SUCCESS ======================"' >> $smoke_script diff --git a/windows/create_installer_windows.sh b/windows/create_installer_windows.sh index 9347d611c4..5815b2c086 100755 --- a/windows/create_installer_windows.sh +++ b/windows/create_installer_windows.sh @@ -233,9 +233,16 @@ NSIS_SCRIPT="Coq.nsi" SHELL_BAT="coq-shell.bat" SHELL_ICO="coq-shell.ico" -COQ_MAJOR="$(opam show -f version coq | cut -d. -f1 || echo 0)" +if opam show -f version rocq-core >/dev/null 2>&1; then + COQ_MAJOR="$(opam show -f version rocq-core | cut -d. -f1)" +elif opam show -f version coq >/dev/null 2>&1; then + COQ_MAJOR="$(opam show -f version coq | cut -d. -f1)" +else + COQ_MAJOR=0 +fi + if [ "${COQ_MAJOR:-0}" -ge 9 ]; then - echo "Coq >= 9 => Rocq branding" + echo "Rocq >= 9 => Rocq branding" ide_name="rocqide" APP_PREFIX="Rocq-Platform" NSIS_SCRIPT="Rocq.nsi" @@ -263,7 +270,11 @@ add_single_file "${MODDIR}/" "${PIXBUF_LOADER_CACHE_RELPATH}" "files_conf-gtk3" ###### Add system DLLs to some packages ##### -add_shared_library_dependencies "coqc" "/usr/${COQ_ARCH}-w64-mingw32/sys-root/" "files_coq" +if command -v rocq >/dev/null 2>&1; then + add_shared_library_dependencies "rocq" "/usr/${COQ_ARCH}-w64-mingw32/sys-root/" "files_coq" +else + add_shared_library_dependencies "coqc" "/usr/${COQ_ARCH}-w64-mingw32/sys-root/" "files_coq" +fi add_shared_library_dependencies "${ide_name}" "/usr/${COQ_ARCH}-w64-mingw32/sys-root/" "files_${ide_name}" add_shared_library_dependencies "gappa" "/usr/${COQ_ARCH}-w64-mingw32/sys-root/" "files_gappa" @@ -357,8 +368,25 @@ cp ../windows/*.ns* . # Extract some data from sources mkdir source -COQ_MAJOR="$(opam show -f version coq | cut -d. -f1 || echo 0)" -if [ "${COQ_MAJOR:-0}" -ge 9 ]; then +if opam show -f version rocq-core >/dev/null 2>&1; then + COQ_MAJOR2="$(opam show -f version rocq-core | cut -d. -f1)" +elif opam show -f version coq >/dev/null 2>&1; then + COQ_MAJOR2="$(opam show -f version coq | cut -d. -f1)" +else + COQ_MAJOR2=0 +fi + +if opam list --installed --silent rocq-core 2>/dev/null; then + echo "Rocq detected — sourcing split packages" + for pkg in rocq-core rocq-stdlib coqide-server rocq-runtime "${ide_name}" coq-compcert coq-vst coq-vst-32; do + if opam list --installed --silent "${pkg}" 2>/dev/null; then + packagefull=$(opam list --installed --short --columns=name,version "${pkg}" | sed 's/ /./') + echo "→ opam source ${packagefull}" + opam source --dir="source/${pkg}" "${packagefull}" + fi + done + LICENSE_SRC="source/rocq-core/LICENSE" +elif [ "${COQ_MAJOR2:-0}" -ge 9 ]; then echo "Coq >= 9 detected — sourcing split packages" for pkg in coq-core coq-stdlib coqide-server "${ide_name}" coq-compcert coq-vst coq-vst-32; do if opam list --installed --silent "${pkg}"; then