Skip to content

feat: new version of package pick 9.1 #512

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Justme0606 merged 2 commits into from
Apr 7, 2026
Merged

feat: new version of package pick 9.1 #512

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
be95c16
feat: new version of package pick 9.1
Justme0606 Feb 24, 2026
8572215
fix: sanitize invalid unicode character in coq-gappa file paths on Wi…
Justme0606 Apr 2, 2026
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
76 changes: 37 additions & 39 deletions .github/workflows/macos.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,15 +15,15 @@ on:
- main
pull_request:
branches:
- '**'
- "**"
schedule:
- cron: "0 0 * * *"
workflow_dispatch:
inputs:
platform:
description: 'Arguments for the platform script:'
description: "Arguments for the platform script:"
required: true
default: '-extent=x -parallel=p -jobs=2 -large=e -compcert=y -set-switch=y'
default: "-extent=x -parallel=p -jobs=2 -large=e -compcert=y -set-switch=y"

###############################################################################
# Platform script options shared among all jobs
Expand All @@ -49,14 +49,14 @@ jobs:
matrix:
variant:
# Keep this in sync with the Smoke test below
- '9.0~2025.08'
- '8.20~2025.01'
- "9.1~2026.01"
- "9.0~2025.08"

steps:
- name: Setup Xcode 16.0
uses: maxim-lobanov/setup-xcode@v1
with:
xcode-version: '16.0'
xcode-version: "16.0"

- name: Print toolchain info
run: |
Expand All @@ -65,7 +65,7 @@ jobs:
xcode-select -p
xcrun --show-sdk-path
xcrun --show-sdk-platform-version || true

- name: Git checkout
uses: actions/checkout@v4

Expand All @@ -77,7 +77,7 @@ jobs:
# This is to avoid errors of these kinds:
# - ==> Downloading https://ghcr.io/v2/homebrew/core/harfbuzz/manifests/5.1.0
# Error: adwaita-icon-theme: Failed to download resource "harfbuzz_bottle_manifest"
# The downloaded GitHub Packages manifest was corrupted or modified (it is not valid JSON):
# The downloaded GitHub Packages manifest was corrupted or modified (it is not valid JSON):
# - dyld[45184]: Library not loaded: '/usr/local/opt/libunistring/lib/libunistring.2.dylib'
# Referenced from: '/usr/local/Cellar/wget/1.21.3/bin/wget'
# Reason: tried: '/usr/local/opt/libunistring/lib/libunistring.2.dylib' (no such file),
Expand Down Expand Up @@ -114,18 +114,18 @@ jobs:
echo "Using ARGS=$ARGS"
./coq_platform_make.sh -packages=${{matrix.variant}} $ARGS -dumplogs

- name: 'Upload opam log folder on failure'
- name: "Upload opam log folder on failure"
uses: actions/upload-artifact@v4
if: failure()
with:
name: 'Opam log folder ${{matrix.variant}}'
name: "Opam log folder ${{matrix.variant}}"
path: /Users/runner/.opam/log/

- name: 'Upload opam build folder on failure'
- name: "Upload opam build folder on failure"
uses: actions/upload-artifact@v4
if: failure()
with:
name: 'Opam build folder ${{matrix.variant}}'
name: "Opam build folder ${{matrix.variant}}"
path: /Users/runner/.opam/CP*${{matrix.variant}}/.opam-switch/build

- name: Install bash (needed by smoke scripts)
Expand All @@ -137,10 +137,10 @@ jobs:
eval $(opam env)
shell_scripts/create_smoke_test_kit.sh

- name: 'Upload smoke test kit'
- name: "Upload smoke test kit"
uses: actions/upload-artifact@v4
with:
name: 'Smoke Test Kit Macos ${{matrix.variant}}'
name: "Smoke Test Kit Macos ${{matrix.variant}}"
path: smoke-test-kit/
retention-days: 5

Expand All @@ -151,7 +151,7 @@ jobs:
brew install findutils coreutils
. .venv/bin/activate
pip3 install macpack

# Patch macpack to create/set an asyncio loop on Python 3.14
python3 <<'EOF'
import sysconfig
Expand Down Expand Up @@ -200,17 +200,16 @@ jobs:
print("⚠ WARNING: Could not find or patch macpack/patcher.py")
print("This may cause issues with Python 3.14")
EOF

# Sanity check: show which macpack will run
which macpack
python3 -c "import macpack; print('macpack imported successfully')"

# Sanity check: show which macpack will run
which macpack
python3 -c "import macpack; print('macpack imported successfully')"


- name: 'Build DMG installer'
- name: "Build DMG installer"
uses: Wandalen/wretry.action@v3
with:
attempt_limit: 5
Expand All @@ -219,13 +218,13 @@ jobs:
eval $(opam env)
macos/create_installer_macos.sh

- name: 'Upload DMG script logs on failure'
- name: "Upload DMG script logs on failure"
uses: actions/upload-artifact@v4
if: failure()
with:
name: 'DMG script error logs ${{matrix.variant}}'
name: "DMG script error logs ${{matrix.variant}}"
path: macos_installer/logs/

- name: Set APP_PREFIX (Coq vs Rocq)
shell: bash
run: |
Expand All @@ -235,10 +234,10 @@ jobs:
echo "APP_PREFIX=Coq-Platform" >> "$GITHUB_ENV"
fi

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

Expand All @@ -250,25 +249,25 @@ jobs:
fail-fast: false
matrix:
variant:
- '9.0~2025.08'
- '8.20~2025.01'
- "9.1~2026.01"
- "9.0~2025.08"

steps:
- name: Install bash
run: brew install bash

- name: 'Download Artifact'
- name: "Download Artifact"
uses: actions/download-artifact@v4
id: download
with:
name: 'Macos installer ${{matrix.variant}} x86_64'
name: "Macos installer ${{matrix.variant}} x86_64"

- name: 'Download smoke test kit'
- name: "Download smoke test kit"
uses: actions/download-artifact@v4
id: download-smoke
with:
name: 'Smoke Test Kit Macos ${{matrix.variant}}'
name: "Smoke Test Kit Macos ${{matrix.variant}}"

- name: Set APP_PREFIX (Coq vs Rocq)
shell: bash
run: |
Expand All @@ -278,7 +277,7 @@ jobs:
echo "APP_PREFIX=Coq-Platform" >> "$GITHUB_ENV"
fi

- name: 'Run Installer'
- name: "Run Installer"
shell: bash
run: |
cd ${{steps.download.outputs.download-path}}
Expand All @@ -287,31 +286,31 @@ jobs:
cp -r "/Volumes/${DMG%%.dmg}/${APP_PREFIX}"*.app /Applications/
hdiutil detach "/Volumes/${DMG%%.dmg}/"

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

# Try default coqc first
if ./coqc -v 2>/dev/null; then
exit 0
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'
- name: "Run Macos smoke test kit"
shell: bash
run: |
ls /Applications/${APP_PREFIX}*.app
Expand All @@ -331,4 +330,3 @@ jobs:
cd ${{steps.download-smoke.outputs.download-path}}
chmod a+x ./run-smoke-test.sh
./run-smoke-test.sh

40 changes: 20 additions & 20 deletions .github/workflows/ubuntu.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,15 +15,15 @@ on:
- main
pull_request:
branches:
- '**'
- "**"
schedule:
- cron: "0 0 * * *"
workflow_dispatch:
inputs:
platform:
description: 'Arguments for the platform script:'
description: "Arguments for the platform script:"
required: true
default: '-extent=x -parallel=p -jobs=2 -large=i -compcert=y -unimath=n -set-switch=y'
default: "-extent=x -parallel=p -jobs=2 -large=i -compcert=y -unimath=n -set-switch=y"

###############################################################################
# Platform script options shared among all jobs
Expand All @@ -32,7 +32,6 @@ env:
PLATFORM: -extent=x -parallel=p -jobs=2 -large=i -compcert=y -unimath=n -set-switch=y
COQREGTESTING: y


###############################################################################
# Ubuntu
#
Expand All @@ -49,21 +48,22 @@ jobs:
matrix:
variant:
# This should contain all picks introduced in the current release + all original picks of all Coq versions
- '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'
- "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"

steps:
- name: Git checkout
uses: actions/checkout@v4

- name: Initial disk usage
run: |
echo "=== Initial df -h ==="
Expand Down Expand Up @@ -134,7 +134,7 @@ jobs:
sudo apt-get install bubblewrap build-essential
echo "=== Disk after apt install ==="
df -h

- name: Free additional disk space
run: |
echo "=== Disk before cleanup ==="
Expand All @@ -148,7 +148,7 @@ jobs:
echo
echo "=== Top 15 biggest directories in ~ ==="
du -xhd1 ~ 2>/dev/null | sort -hr | head -n 15 || true

- name: Free Disk Space (Ubuntu)
uses: jlumbroso/free-disk-space@main
with:
Expand Down Expand Up @@ -192,15 +192,15 @@ jobs:
eval $(opam env)
shell_scripts/create_smoke_test_kit.sh

- name: 'Run Linux smoke test kit'
- name: "Run Linux smoke test kit"
shell: bash
run: |
eval $(opam env)
smoke-test-kit/run-smoke-test.sh

- name: 'Upload smoke test kit'
- name: "Upload smoke test kit"
uses: actions/upload-artifact@v4
with:
name: 'Smoke Test Kit ${{matrix.variant}}'
name: "Smoke Test Kit ${{matrix.variant}}"
path: smoke-test-kit
retention-days: 5
Loading
Loading