Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
51 changes: 36 additions & 15 deletions .github/workflows/macos.yml
Original file line number Diff line number Diff line change
Expand Up @@ -222,12 +222,21 @@ jobs:
with:
name: 'DMG script error logs ${{matrix.variant}}'
path: macos_installer/logs/

- name: Set APP_PREFIX (Coq vs Rocq)
shell: bash
run: |
if [[ "${{ matrix.variant }}" == 9.* ]]; then
echo "APP_PREFIX=Rocq-Platform" >> "$GITHUB_ENV"
else
echo "APP_PREFIX=Coq-Platform" >> "$GITHUB_ENV"
fi

- name: 'Upload Artifact'
uses: actions/upload-artifact@v4
with:
name: 'Macos installer ${{matrix.variant}} x86_64'
path: macos_installer/Coq-Platform-*.dmg
path: macos_installer/${{ env.APP_PREFIX }}-*.dmg
retention-days: 5

Macos_smoke:
Expand Down Expand Up @@ -256,20 +265,29 @@ jobs:
id: download-smoke
with:
name: 'Smoke Test Kit Macos ${{matrix.variant}}'

- name: Set APP_PREFIX (Coq vs Rocq)
shell: bash
run: |
if [[ "${{ matrix.variant }}" == 9.* ]]; then
echo "APP_PREFIX=Rocq-Platform" >> "$GITHUB_ENV"
else
echo "APP_PREFIX=Coq-Platform" >> "$GITHUB_ENV"
fi

- name: 'Run Installer'
shell: bash
run: |
cd ${{steps.download.outputs.download-path}}
DMG=$(ls Coq-Platform-*.dmg)
hdiutil attach $DMG
cp -r /Volumes/${DMG%%.dmg}/Coq-Platform*.app /Applications/
hdiutil detach /Volumes/${DMG%%.dmg}/
DMG=$(ls "${APP_PREFIX}"-*.dmg)
hdiutil attach "$DMG"
cp -r "/Volumes/${DMG%%.dmg}/${APP_PREFIX}"*.app /Applications/
hdiutil detach "/Volumes/${DMG%%.dmg}/"

- name: 'Smoke coqc'
shell: bash
run: |
cd /Applications/Coq-Platform*.app/Contents/Resources/bin/
cd /Applications/${APP_PREFIX}*.app/Contents/Resources/bin/

# Try default coqc first
if ./coqc -v 2>/dev/null; then
Expand All @@ -293,18 +311,21 @@ jobs:
- name: 'Run Macos smoke test kit'
shell: bash
run: |
ls /Applications/Coq-Platform*.app
export PATH="$PATH:$(cd /Applications/Coq-Platform*.app/Contents/Resources/bin/; pwd)"

# Try to set COQLIB, but don't fail if it doesn't work
if COQLIB_TEMP=$(coqc -where 2>/dev/null); then
export COQLIB="$COQLIB_TEMP"
echo "COQLIB set to: $COQLIB"
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
export ROCQLIB="$ROCQLIB_TEMP"
export COQLIB="$ROCQLIB_TEMP"
echo "ROCQLIB set to: $ROCQLIB"
else
echo "Warning: coqc -where failed, COQLIB not set"
echo "Warning: coqc -where failed, ROCQLIB/COQLIB not set"
export ROCQLIB=""
export COQLIB=""
fi

cd ${{steps.download-smoke.outputs.download-path}}
chmod a+x ./run-smoke-test.sh
./run-smoke-test.sh

38 changes: 19 additions & 19 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,13 +6,13 @@

**In case you experience dead links, please replace `2025.08.0` with `2025.01.0`.**

The [Coq proof assistant](https://coq.inria.fr) provides a formal language
The [Rocq proof assistant](https://rocq-prover.org/) provides a formal language
to write mathematical definitions, executable algorithms, and theorems, together
with an environment for semi-interactive development of machine-checked proofs.

The **Coq Platform** is a distribution of Coq together with a selection of
libraries and plugins. The main goal of the Coq Platform is to provide a
distribution for developing and teaching with Coq that is:
The **Rocq Platform** is a distribution of Rocq together with a selection of
libraries and plugins. The main goal of the Rocq Platform is to provide a
distribution for developing and teaching with Rocq that is:

- operating system independent
- dependable
Expand All @@ -21,27 +21,27 @@ distribution for developing and teaching with Coq that is:

See the [Charter](charter.md) for more on the Platform concept, and
[CEP 52](https://github.com/coq/ceps/blob/master/text/052-platform-release-cycle.md)
for more on how the Platform is related to the Coq release cycle.
for more on how the Platform is related to the Rocq release cycle.

The Coq Platform is based on the OCaml package manager **opam** and provides a set
of scripts to compile and/or install opam, Coq and the platform contents on macOS,
The Rocq Platform is based on the OCaml package manager **opam** and provides a set
of scripts to compile and/or install opam, Rocq and the platform contents on macOS,
Windows and many Linux distributions in a reliable way with consistent results.
In addition **pre-compiled binary packages** or **installers** are provided for **macOS** and
**Windows** (Docker is in preparation). Note that snap for Linux is no longer supported
(the maintenance effort was too high).

The Coq Platform supports installing several versions of Coq - also in parallel,
e.g., for porting developments from one version of Coq to another. For the
previous release version of Coq, Coq Platform provides extended and updated
The Rocq Platform supports installing several versions of Coq - also in parallel,
e.g., for porting developments from one version of Rocq to another. For the
previous release version of Rocq, Rocq Platform provides extended and updated
package picks which are as much as possible compatible to the pick of the latest
release version of Coq. For this reason for some Coq versions several different
release version of Rocq. For this reason for some Rocq versions several different
package picks are provided.

The table below contains links to the README files for the supported versions
of Coq and libraries. Each README file contains a list of included packages with
of Rocq and libraries. Each README file contains a list of included packages with
detailed information for each package.

- [Coq 9.0.1 (released Aug 2025) with the first package pick from Aug 2025](doc/README~9.0~2025.08.md)
- [Rocq 9.0.1 (released Aug 2025) with the first package pick from Aug 2025](doc/README~9.0~2025.08.md)
- [Coq 8.20.1 (released Jan 2025) with the first package pick from Jan 2025](doc/README~8.20~2025.01.md)
- [Coq 8.19.2 (released Jun 2024) with the first package pick from Oct 2024](doc/README~8.19~2024.10.md)
- [Coq 8.18.0 (released Sep 2023) with the first package pick from Nov 2023](doc/README~8.18~2023.11.md)
Expand All @@ -59,12 +59,12 @@ detailed information for each package.
- [Coq 8.12.2 (released Dec 2020)](doc/README~8.12.md)
- [Coq Developer (latest developer branch)](doc/README~dev.md)

If you have questions on the Coq Platform, please contact us on zulip chat [Coq-Platform & users](https://coq.zulipchat.com/#narrow/stream/250632-Coq-Platform.20devs.20.26.20users)
If you have questions on the Rocq Platform, please contact us on zulip chat [Rocq-Platform & users](https://rocq-prover.zulipchat.com/#narrow/stream/250632-Coq-Platform.20devs.20.26.20users)

## Installation

The Coq platform is the recommended way to install Coq for both beginners and experts.
Beginners are encouraged to use one of the binary installers. Experienced users are advised to run the scripts provided by the Coq platform to install from sources as this will allow them to install additional packages with opam.
The Rocq platform is the recommended way to install Rocq for both beginners and experts.
Beginners are encouraged to use one of the binary installers. Experienced users are advised to run the scripts provided by the Rocq platform to install from sources as this will allow them to install additional packages with opam.
Please refer to the ReadMe file for your operating system, which contains information on both methods respectively.

- macOS: see [README_macOS](doc/README_macOS.md).
Expand All @@ -75,12 +75,12 @@ Please refer to the ReadMe file for your operating system, which contains inform

<details><summary><font size="+1">Licenses</font></summary>

The Coq Platform setup scripts and the selection of package recipes and patches are licensed Creative Commons CC0.
This license does **not** apply to the packages installed by the Coq Platform.
The Rocq Platform setup scripts and the selection of package recipes and patches are licensed Creative Commons CC0.
This license does **not** apply to the packages installed by the Rocq Platform.
The README files linked above provide license information for each package.
This information is also available as .CSV files here [doc](doc).
Please note that the license information is obtained from opam.
The Coq Platform team does no double check this information.
The Rocq Platform team does no double check this information.

</details>

Expand Down
9 changes: 9 additions & 0 deletions macos/coq-env.sh.template
Original file line number Diff line number Diff line change
@@ -1,7 +1,16 @@
#!/bin/bash

# Coq-Platform (ancien nom)
if [ -f "/Applications/Coq-Platform@@VERSION@@.app/Contents/Resources/bin/coqc" ]
then
echo "export PATH='/Applications/Coq-Platform@@VERSION@@.app/Contents/Resources/bin':"'"$PATH"'
echo "export COQLIB='/Applications/Coq-Platform@@VERSION@@.app/Contents/Resources/lib/coq'"
fi

# Rocq-Platform (nouveau nom)
if [ -f "/Applications/Rocq-Platform@@VERSION@@.app/Contents/Resources/bin/coqc" ]
then
echo "export PATH='/Applications/Rocq-Platform@@VERSION@@.app/Contents/Resources/bin':"'"$PATH"'
echo "export ROCQLIB='/Applications/Rocq-Platform@@VERSION@@.app/Contents/Resources/lib/coq'"
echo "export COQLIB='/Applications/Rocq-Platform@@VERSION@@.app/Contents/Resources/lib/coq'"
fi
15 changes: 13 additions & 2 deletions macos/create_installer_macos.sh
Original file line number Diff line number Diff line change
Expand Up @@ -261,11 +261,22 @@ function callback_file {

###################### Create installer folder structure ######################

# Determine major version from COQ_VERSION (already computed above)
coq_major="${COQ_VERSION%%.*}"

SHELL_PREFIX="coq"
PRODUCT_PREFIX="Coq-Platform"
if [ -n "${coq_major}" ] && [ "${coq_major}" -ge 9 ]; then
PRODUCT_PREFIX="Rocq-Platform"
SHELL_PREFIX="rocq"
fi

APP_NAME="${PRODUCT_PREFIX}${COQ_PLATFORM_PACKAGE_PICK_POSTFIX}.app"
DMG_NAME="${PRODUCT_PREFIX}-release-${COQ_PLATFORM_RELEASE}-version${COQ_PLATFORM_PACKAGE_PICK_POSTFIX}-MacOS-$(uname -m)"


# Folder and image names

APP_NAME="Coq-Platform${COQ_PLATFORM_PACKAGE_PICK_POSTFIX}.app"
DMG_NAME="Coq-Platform-release-${COQ_PLATFORM_RELEASE}-version${COQ_PLATFORM_PACKAGE_PICK_POSTFIX}-MacOS-$(uname -m)"
APP_ABSDIR="_dmg/${APP_NAME}"
RSRC_ABSDIR="${APP_ABSDIR}/Contents/Resources"
BIN_ABSDIR="$RSRC_ABSDIR/bin"
Expand Down
21 changes: 19 additions & 2 deletions macos/wrapper_bin_folder.c
Original file line number Diff line number Diff line change
Expand Up @@ -37,9 +37,20 @@ int main (int argc, char* argv[])
strncpy(bin_folder, resources_folder, sizeof(bin_folder)-1);
strncat(bin_folder, "/bin", sizeof(bin_folder)-1);

// Generate CoqIDE exe path
// Decide which IDE to launch based on wrapper name
char wrapper_name[PROC_PIDPATHINFO_MAXSIZE];
strncpy(wrapper_name, basename(normalized_full_exe_path), sizeof(wrapper_name)-1);
wrapper_name[sizeof(wrapper_name)-1] = '\0';

const char *ide_exe = "coqide.exe";
if (strcmp(wrapper_name, "rocqide") == 0 || strcmp(wrapper_name, "rocqide.exe") == 0) {
ide_exe = "rocqide.exe";
}

// Generate CoqIDE exe path (now conditional)
strncpy(coqide_path, bin_folder, sizeof(value)-1);
strncat(coqide_path, "/coqide.exe", sizeof(coqide_path)-1);
strncat(coqide_path, "/", sizeof(coqide_path)-1);
strncat(coqide_path, ide_exe, sizeof(coqide_path)-1);

// Generate and set GDK_PIXBUF_MODULE_FILE value
strncpy(value, resources_folder, sizeof(value)-1);
Expand Down Expand Up @@ -71,6 +82,12 @@ int main (int argc, char* argv[])
free(path_new);
}

// Generate and set COQLIB value (Coq/Rocq standard library inside the bundle)
strncpy(value, resources_folder, sizeof(value)-1);
value[sizeof(value)-1] = '\0';
strncat(value, "/lib/coq", sizeof(value)-strlen(value)-1);
setenv("COQLIB", value, 1);

// call executable
{
char ** newargs = (char**)calloc(argc+1, sizeof(char*));
Expand Down
21 changes: 19 additions & 2 deletions macos/wrapper_macos_folder.c
Original file line number Diff line number Diff line change
Expand Up @@ -36,9 +36,20 @@ int main (int argc, char* argv[])
strncpy(bin_folder, resources_folder, sizeof(bin_folder)-1);
strncat(bin_folder, "/bin", sizeof(bin_folder)-1);

// Generate CoqIDE exe path
// Decide which IDE to launch based on wrapper name
char wrapper_name[PROC_PIDPATHINFO_MAXSIZE];
strncpy(wrapper_name, basename(normalized_full_exe_path), sizeof(wrapper_name)-1);
wrapper_name[sizeof(wrapper_name)-1] = '\0';

const char *ide_exe = "coqide.exe";
if (strcmp(wrapper_name, "rocqide") == 0 || strcmp(wrapper_name, "rocqide.exe") == 0) {
ide_exe = "rocqide.exe";
}

// Generate CoqIDE exe path (now conditional)
strncpy(coqide_path, bin_folder, sizeof(value)-1);
strncat(coqide_path, "/coqide.exe", sizeof(coqide_path)-1);
strncat(coqide_path, "/", sizeof(coqide_path)-1);
strncat(coqide_path, ide_exe, sizeof(coqide_path)-1);

// Generate and set GDK_PIXBUF_MODULE_FILE value
strncpy(value, resources_folder, sizeof(value)-1);
Expand Down Expand Up @@ -70,6 +81,12 @@ int main (int argc, char* argv[])
free(path_new);
}

// Generate and set COQLIB value (Coq/Rocq standard library inside the bundle)
strncpy(value, resources_folder, sizeof(value)-1);
value[sizeof(value)-1] = '\0';
strncat(value, "/lib/coq", sizeof(value)-strlen(value)-1);
setenv("COQLIB", value, 1);

// call executable
{
char ** newargs = (char**)calloc(argc+1, sizeof(char*));
Expand Down
Loading
Loading