From f278bdc0d3d38c1c6d710252e61ed90073f40f12 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 26 Sep 2023 14:18:35 +0200 Subject: [PATCH] [2023.08] [coq-lsp 0.1.8] [v8.17] Draft Windows build Changes: - Simplify some paths and logic - Don't exclude `sexplib0` - Pin to latest Coq's v8.17+lsp branch - Pin to latest coq-lsp's branch for 8.17 - Slightly reduced package set - Added waterproof --- .github/workflows/macos.yml | 180 ----------------- .github/workflows/ubuntu.yml | 190 ------------------ .github/workflows/ubuntu_dev.yml | 79 -------- .github/workflows/windows.yml | 64 +----- .../package-pick-8.17~2023.08-coq-lsp.sh | 157 +++++++++++++++ shell_scripts/build.sh | 5 +- shell_scripts/installer_create_tree.sh | 2 +- 7 files changed, 165 insertions(+), 512 deletions(-) delete mode 100644 .github/workflows/macos.yml delete mode 100644 .github/workflows/ubuntu.yml delete mode 100644 .github/workflows/ubuntu_dev.yml create mode 100644 package_picks/package-pick-8.17~2023.08-coq-lsp.sh diff --git a/.github/workflows/macos.yml b/.github/workflows/macos.yml deleted file mode 100644 index b815d3fc88..0000000000 --- a/.github/workflows/macos.yml +++ /dev/null @@ -1,180 +0,0 @@ -# Main doc: https://docs.github.com/en/free-pro-team@latest/actions/learn-github-actions/introduction-to-github-actions -# Runners spec: https://docs.github.com/en/free-pro-team@latest/actions/reference/specifications-for-github-hosted-runners -# Glob expressions: https://github.com/actions/toolkit/tree/main/packages/glob - -name: Macos - -############################################################################### -# Schedule: -# - push on any branch whose name matches v** or master -# - any pull request -############################################################################### -on: - push: - branches: - - 2021.02 - - 2021.09 - - main - pull_request: - branches: - - '**' - schedule: - - cron: "0 0 * * *" - workflow_dispatch: - inputs: - platform: - description: 'Arguments for the platform script:' - required: true - default: '-extent=x -parallel=p -jobs=2 -large=e -compcert=y -set-switch=y' - -############################################################################### -# Platform script options shared among all jobs -############################################################################### -env: - PLATFORM_ARGS: -extent=x -parallel=p -jobs=2 -large=e -compcert=y -set-switch=y - COQREGTESTING: y - HOMEBREW_NO_INSTALL_FROM_API: - # See https://github.com/orgs/Homebrew/discussions/4612#discussioncomment-6351357 - -############################################################################### -# Macos -# -# CAVEATS: -# - COQREGTESTING broken, it makes the script loop, so we install opam by hand -############################################################################### -jobs: - Macos_platform: - name: Macos - runs-on: macos-latest - strategy: - fail-fast: false - matrix: - variant: - - '8.17~2023.08' - - '8.16~2022.09' - - steps: - - name: Git checkout - uses: actions/checkout@v2 - - - name: Set PLATFORM - if: ${{ github.event.inputs.platform != '' }} - run: echo "PLATFORM=${{ github.event.inputs.platform }}" >> $GITHUB_ENV - - - name: Cleanup, update and upgrade HomeBrew - # 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): - # - 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), - run: | - brew cleanup - # See https://github.com/orgs/Homebrew/discussions/4612#discussioncomment-6351357 - brew config - brew untap homebrew/core homebrew/cask - brew config - brew update - # Note: brew upgrade does fail regularly, but brew is anyway in a better state afterwards - brew upgrade || true - - - name: Install homebrew packages required by main script - run: brew install wget - - - name: Run common platform script - shell: bash - run: ./coq_platform_make.sh -packages=${{matrix.variant}} $PLATFORM_ARGS -dumplogs - - - name: Install bash (needed by smoke scripts) - run: brew install bash - - - name: Create smoke test kit - shell: bash - run: | - eval $(opam env) - export MACOSX_DEPLOYMENT_TARGET=10.13 - shell_scripts/create_smoke_test_kit.sh - - - name: 'Upload smoke test kit' - uses: actions/upload-artifact@v2 - with: - name: 'Smoke Test Kit Macos ${{matrix.variant}}' - path: smoke-test-kit/ - retention-days: 5 - - - name: Install findutils, coreutils and macpack (needed by DMG script) - run: | - brew install findutils - brew install coreutils - pip3 install macpack - - - name: 'Build DMG installer' - shell: bash - run: | - eval $(opam env) - macos/create_installer_macos.sh - - - name: 'Upload DMG script logs on failure' - uses: actions/upload-artifact@v2 - if: failure() - with: - name: 'DMG script error logs ${{matrix.variant}}' - path: macos_installer/logs/ - - - name: 'Upload Artifact' - uses: actions/upload-artifact@v2 - with: - name: 'Macos installer ${{matrix.variant}} x86_64' - path: macos_installer/Coq-Platform-*.dmg - retention-days: 5 - - Macos_smoke: - name: Smoke test Macos - needs: Macos_platform - runs-on: macos-latest - strategy: - fail-fast: false - matrix: - variant: - - '8.17~2023.08' - - '8.16~2022.09' - - steps: - - name: Install bash - run: brew install bash - - - name: 'Download Artifact' - uses: actions/download-artifact@v2 - id: download - with: - name: 'Macos installer ${{matrix.variant}} x86_64' - - - name: 'Download smoke test kit' - uses: actions/download-artifact@v2 - id: download-smoke - with: - name: 'Smoke Test Kit Macos ${{matrix.variant}}' - - - 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}/ - - - name: 'Smoke coqc' - shell: bash - run: | - cd /Applications/Coq-Platform*.app/Contents/Resources/bin/ - ./coqc -v - - - name: 'Run Macos smoke test kit' - shell: bash - run: | - export PATH="$PATH:$(cd /Applications/Coq-Platform*.app/Contents/Resources/bin/; pwd)" - cd ${{steps.download-smoke.outputs.download-path}} - chmod a+x ./run-smoke-test.sh - ./run-smoke-test.sh diff --git a/.github/workflows/ubuntu.yml b/.github/workflows/ubuntu.yml deleted file mode 100644 index 30f31cbd93..0000000000 --- a/.github/workflows/ubuntu.yml +++ /dev/null @@ -1,190 +0,0 @@ -# Main doc: https://docs.github.com/en/free-pro-team@latest/actions/learn-github-actions/introduction-to-github-actions -# Runners spec: https://docs.github.com/en/free-pro-team@latest/actions/reference/specifications-for-github-hosted-runners -# Glob expressions: https://github.com/actions/toolkit/tree/main/packages/glob - -name: Ubuntu - -############################################################################### -# Schedule: -# - push on any branch whose name matches v** or master -# - any pull request -############################################################################### -on: - push: - branches: - - 2021.02 - - 2021.09 - - main - pull_request: - branches: - - '**' - schedule: - - cron: "0 0 * * *" - workflow_dispatch: - inputs: - platform: - description: 'Arguments for the platform script:' - required: true - default: '-extent=x -parallel=p -jobs=2 -large=i -compcert=y -unimath=n -set-switch=y' - snap_pick: - description: 'Package pick for the snap package:' - default: 8.17~2023.08 - upload: - description: 'Upload artifact to Snap Store? (true/false, default false)' - default: false - -############################################################################### -# Platform script options shared among all jobs -############################################################################### -env: - PLATFORM: -extent=x -parallel=p -jobs=2 -large=i -compcert=y -unimath=n -set-switch=y - COQREGTESTING: y - SNAP_PICK: 8.17~2023.08 - - -############################################################################### -# Ubuntu -# -# CAVEATS: -# - you need bubblewrap or the script fails -# - build-essential pulls in the C toolchain -############################################################################### -jobs: - Ubuntu_platform: - name: Ubuntu - runs-on: ubuntu-latest - strategy: - fail-fast: false - matrix: - variant: - # This should contain all picks introduced in the current release + all original picks of all Coq versions - - '8.17~2023.08' - - '8.16~2022.09' - - '8.15~2022.09' - - '8.15~2022.04' - - '8.14~2022.01' - - '8.13~2021.02' - - '8.12' - - steps: - - name: Git checkout - uses: actions/checkout@v2 - - - name: Set PLATFORM - if: ${{ github.event.inputs.platform != '' }} - run: echo "PLATFORM=${{ github.event.inputs.platform }}" >> $GITHUB_ENV - - - name: Install bubblewrap and build-essential - run: | - sudo apt-get update - sudo apt-get install bubblewrap build-essential - - - name: Run common platform script - shell: bash - run: ./coq_platform_make.sh -packages=${{matrix.variant}} $PLATFORM -dumplogs - - - name: Create smoke test kit - shell: bash - run: | - eval $(opam env) - shell_scripts/create_smoke_test_kit.sh - - - name: 'Run Linux smoke test kit' - shell: bash - run: | - eval $(opam env) - smoke-test-kit/run-smoke-test.sh - - - name: 'Upload smoke test kit' - uses: actions/upload-artifact@v2 - with: - name: 'Smoke Test Kit ${{matrix.variant}}' - path: smoke-test-kit - retention-days: 5 - - Ubuntu_snap: - name: Snap package - # Since we build the snap with --destructive-mode, the runner version must match the snap core version - runs-on: ubuntu-20.04 - - steps: - - name: Git checkout - uses: actions/checkout@v2 - - - name: Set PLATFORM - if: ${{ github.event.inputs.platform != '' }} - run: echo "PLATFORM=${{ github.event.inputs.platform }}" >> $GITHUB_ENV - - - name: Set SNAP_PICK - if: ${{ github.event.inputs.snap_pick != '' }} - run: echo "SNAP_PICK=${{ github.event.inputs.snap_pick }}" >> $GITHUB_ENV - - - name: Generate snapcraft file - run: linux/create_snapcraft_yaml.sh -packages=$SNAP_PICK $PLATFORM - - - name: Print snapcraft file - run: cat snap/snapcraft.yaml - - - name: Run snapcraft - uses: MSoegtropIMC/action-snapcraft-build@v1.1.2-dm - id: build - - - name: Dump snapcraft logs - if: ${{ always() }} - run: cat /home/runner/.local/state/snapcraft/log/* - - - name: Save Artifact - uses: actions/upload-artifact@v2 - with: - name: 'Snap package' - path: ${{ steps.build.outputs.snap }} - - - name: Upload Artifact to the Snap Store - if: ${{ github.event.inputs.upload }} - uses: snapcore/action-publish@v1 - with: - store_login: ${{ secrets.STORE_LOGIN }} - snap: ${{ steps.build.outputs.snap }} - release: edge - - # We run this one always because the Ubuntu_platform job - # has a matrix and contains the flaky dev job - # but here we really only need the SNAP_PICK one - # - # In any case the job will fail fast if it can't download - # the snap or the smoke test - - Ubuntu_smoke: - name: Snap package smoke test - if: ${{ always() }} - needs: [Ubuntu_platform, Ubuntu_snap] - runs-on: ubuntu-latest - - steps: - - - name: Set SNAP_PICK - if: ${{ github.event.inputs.snap_pick != '' }} - run: echo "SNAP_PICK=${{ github.event.inputs.snap_pick }}" >> $GITHUB_ENV - - - name: Download Artifact - uses: actions/download-artifact@v2 - id: download-snap - with: - name: 'Snap package' - - - name: 'Download smoke test kit' - uses: actions/download-artifact@v2 - id: download-smoke - with: - name: 'Smoke Test Kit ${{ env.SNAP_PICK }}' - - - name: 'Install Snap' - run: | - sudo snap install --dangerous ${{ steps.download-snap.outputs.download-path }}/coq-prover_*.snap - sudo snap alias coq-prover.coqc coqc - - - name: 'Run Smoke Test Kit' - run: | - cd ${{steps.download-smoke.outputs.download-path}} - chmod a+x ./run-smoke-test.sh - ./run-smoke-test.sh diff --git a/.github/workflows/ubuntu_dev.yml b/.github/workflows/ubuntu_dev.yml deleted file mode 100644 index b279d83560..0000000000 --- a/.github/workflows/ubuntu_dev.yml +++ /dev/null @@ -1,79 +0,0 @@ -# Main doc: https://docs.github.com/en/free-pro-team@latest/actions/learn-github-actions/introduction-to-github-actions -# Runners spec: https://docs.github.com/en/free-pro-team@latest/actions/reference/specifications-for-github-hosted-runners -# Glob expressions: https://github.com/actions/toolkit/tree/main/packages/glob - -name: Ubuntu_dev - -############################################################################### -# Schedule: -# - daily -############################################################################### -on: - schedule: - - cron: "0 0 * * *" - workflow_dispatch: - inputs: - platform: - description: 'Arguments for the platform script:' - required: true - default: '-extent=x -parallel=p -jobs=2 -large=i -compcert=y -unimath=n -set-switch=y' - -############################################################################### -# Platform script options shared among all jobs -############################################################################### -env: - PLATFORM: -extent=x -parallel=p -jobs=2 -large=i -compcert=y -unimath=n -set-switch=y - COQREGTESTING: y - -############################################################################### -# Ubuntu -# -# CAVEATS: -# - you need bubblewrap or the script fails -# - build-essential pulls in the C toolchain -############################################################################### -jobs: - Ubuntu_platform: - name: Ubuntu - runs-on: ubuntu-latest - strategy: - fail-fast: false - matrix: - variant: - - 'dev' - - steps: - - name: Git checkout - uses: actions/checkout@v2 - - - name: Set PLATFORM - if: ${{ github.event.inputs.platform != '' }} - run: echo "PLATFORM=${{ github.event.inputs.platform }}" >> $GITHUB_ENV - - - name: Install bubblewrap and build-essential - run: | - sudo apt-get update - sudo apt-get install bubblewrap build-essential - - - name: Run common platform script - shell: bash - run: ./coq_platform_make.sh -packages=${{matrix.variant}} $PLATFORM -dumplogs - - - name: Create smoke test kit - shell: bash - run: | - eval $(opam env) - shell_scripts/create_smoke_test_kit.sh - - - name: 'Run Linux smoke test kit' - shell: bash - run: | - eval $(opam env) - smoke-test-kit/run-smoke-test.sh - - - name: 'Upload smoke test kit' - uses: actions/upload-artifact@v2 - with: - name: 'Smoke Test Kit ${{matrix.variant}}' - path: smoke-test-kit - retention-days: 5 diff --git a/.github/workflows/windows.yml b/.github/workflows/windows.yml index f41a37534b..f9e4d344d7 100644 --- a/.github/workflows/windows.yml +++ b/.github/workflows/windows.yml @@ -49,11 +49,9 @@ jobs: matrix: architecture: - '64' - - '32' variant: # Keep this in sync with the Smoke test below - - '8.17~2023.08' - - '8.16~2022.09' + - '8.17~2023.08-coq-lsp' steps: - name: Set git to use LF @@ -70,15 +68,11 @@ jobs: - name: Run common platform script shell: cmd - run: coq_platform_make_windows.bat -destcyg=C:\cygwin_coq_platform -arch=${{matrix.architecture}} -packages=${{matrix.variant}} %PLATFORM_ARGS% -dumplogs + run: coq_platform_make_windows.bat -destcyg=C:\coq_lsp -arch=${{matrix.architecture}} -packages=${{matrix.variant}} %PLATFORM_ARGS% -dumplogs - name: Create installer shell: cmd - run: C:\cygwin_coq_platform\bin\bash --login -c "cd platform/ && windows/create_installer_windows.sh && mkdir /cygdrive/c/installer && cp windows_installer/*exe /cygdrive/c/installer/" - - - name: Create smoke test kit - shell: cmd - run: C:\cygwin_coq_platform\bin\bash --login -c "cd platform/ && shell_scripts/create_smoke_test_kit.sh && mkdir /cygdrive/c/smoke && cp -ra smoke-test-kit/* /cygdrive/c/smoke/" + run: C:\coq_lsp\bin\bash --login -c "cd platform/ && windows/create_installer_windows.sh && mkdir /cygdrive/c/installer && cp windows_installer/*exe /cygdrive/c/installer/" - name: 'Upload Artifact' uses: actions/upload-artifact@v2 @@ -86,55 +80,3 @@ jobs: name: 'Windows installer ${{matrix.variant}} ${{matrix.architecture}}' path: C:\installer\*.exe retention-days: 5 - - - name: 'Upload smoke test kit' - uses: actions/upload-artifact@v2 - with: - name: 'Smoke Test Kit Windows ${{matrix.variant}} ${{matrix.architecture}}' - path: C:\smoke\ - retention-days: 5 - - Windows_smoke: - name: Smoke test Windows - needs: Windows_platform - runs-on: windows-latest - strategy: - fail-fast: false - matrix: - architecture: - - '64' - - '32' - variant: - - '8.17~2023.08' - - '8.16~2022.09' - - steps: - - name: 'Download Artifact' - uses: actions/download-artifact@v2 - id: download - with: - name: 'Windows installer ${{matrix.variant}} ${{matrix.architecture}}' - - - name: 'Download smoke test kit' - uses: actions/download-artifact@v2 - id: download-smoke - with: - name: 'Smoke Test Kit Windows ${{matrix.variant}} ${{matrix.architecture}}' - - - name: 'Run Installer' - shell: cmd - run: | - cd ${{steps.download.outputs.download-path}} - FOR %%f IN (*.exe) DO %%f /S /D=C:\Coq - - - name: 'Smoke coqc' - shell: cmd - run: C:\Coq\bin\coqc.exe -v - - - name: 'Run Windows smoke test kit' - shell: cmd - run: | - CD ${{steps.download-smoke.outputs.download-path}} - DIR - SET PATH=C:\Coq\bin\;%PATH% - CALL run-smoke-test.bat diff --git a/package_picks/package-pick-8.17~2023.08-coq-lsp.sh b/package_picks/package-pick-8.17~2023.08-coq-lsp.sh new file mode 100644 index 0000000000..7b0f20eb01 --- /dev/null +++ b/package_picks/package-pick-8.17~2023.08-coq-lsp.sh @@ -0,0 +1,157 @@ +#!/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="Coq 8.17.1 (released Jun 2023) with Coq LSP" +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='~8.17-lsp' + +# The corresponding Coq development branch and tag +COQ_PLATFORM_COQ_BRANCH='v8.17' +COQ_PLATFORM_COQ_TAG='8.17.1' + +# This controls if opam repositories for development packages are selected +COQ_PLATFORM_USE_DEV_REPOSITORY='N' + +# This extended descriptions is used for readme files +COQ_PLATFORM_VERSION_DESCRIPTION='This version of Coq Platform 2023.03.0 includes Coq 8.17.1 from Jun 2023. ' +COQ_PLATFORM_VERSION_DESCRIPTION+='This is the **latest release version** of the Coq Platform and recommended for general application. ' + +# 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.1' + +###################### 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. +# - The picking tracker issue is https://github.com/coq/platform/issues/193 + +########## BASE PACKAGES ########## + +# Coq needs a patched ocamlfind to be relocatable by installers +PACKAGES="${PACKAGES} PIN.ocamlfind.1.9.5~relocatable" +# Since dune does support Coq, it is explicitly selected +PACKAGES="${PACKAGES} dune.3.7.0" +PACKAGES="${PACKAGES} dune-configurator.3.7.0" +# The Coq compiler coqc and the Coq standard library +PACKAGES="${PACKAGES} PIN.coq.8.17.1" + +########## Coq Language Server ########## +PACKAGES="${PACKAGES} coq-serapi.8.17.0+0.17.1" +PACKAGES="${PACKAGES} coq-lsp.0.1.7+8.17" + +# Coq WaterProof +PACKAGES="${PACKAGES} coq-waterproof.2.0.1+8.17" + +########## IDE PACKAGES ########## + +# GTK based IDE for Coq - alternatives are VSCoq and Proofgeneral for Emacs +if [[ "${COQ_PLATFORM_EXTENT}" =~ ^[iIfFxX] ]] +then +PACKAGES="${PACKAGES} coqide.8.17.1" +fi + +########## "FULL" COQ PLATFORM PACKAGES ########## + +## EJGA: This is still just a subset of the main pick, for testing on +## Win + +if [[ "${COQ_PLATFORM_EXTENT}" =~ ^[fFxX] ]] +then + # Standard library extensions + PACKAGES="${PACKAGES} coq-bignums.9.0.0+coq8.17" + PACKAGES="${PACKAGES} coq-stdpp.1.8.0" + + # General mathematics + PACKAGES="${PACKAGES} coq-mathcomp-ssreflect.1.17.0" + PACKAGES="${PACKAGES} coq-mathcomp-fingroup.1.17.0" + PACKAGES="${PACKAGES} coq-mathcomp-algebra.1.17.0" + PACKAGES="${PACKAGES} coq-mathcomp-solvable.1.17.0" + PACKAGES="${PACKAGES} coq-mathcomp-field.1.17.0" + PACKAGES="${PACKAGES} coq-mathcomp-character.1.17.0" + PACKAGES="${PACKAGES} coq-mathcomp-bigenough.1.0.1" + PACKAGES="${PACKAGES} coq-mathcomp-finmap.1.5.2" + PACKAGES="${PACKAGES} coq-mathcomp-real-closed.1.1.4" + PACKAGES="${PACKAGES} coq-mathcomp-zify.1.3.0+1.12+8.13" + PACKAGES="${PACKAGES} coq-mathcomp-multinomials.1.6.0" + PACKAGES="${PACKAGES} coq-coquelicot.3.4.0" + + # Number theory + PACKAGES="${PACKAGES} coq-coqprime.1.3.0" + PACKAGES="${PACKAGES} coq-coqprime-generator.1.1.1" + + # Numerical mathematics + PACKAGES="${PACKAGES} coq-flocq.4.1.1" + PACKAGES="${PACKAGES} coq-interval.4.8.0" + PACKAGES="${PACKAGES} coq-gappa.1.5.3" + PACKAGES="${PACKAGES} gappa.1.4.1" + + # Constructive mathematics + PACKAGES="${PACKAGES} coq-math-classes.8.17.0" + PACKAGES="${PACKAGES} coq-corn.8.16.0" + + # Homotopy Type Theory (HoTT) + PACKAGES="${PACKAGES} coq-hott.8.17" + + # Univalent Mathematics (UniMath) + # Note: coq-unimath requires too much memory for 32 bit architectures + if [ "${BITSIZE}" == "64" ] + then + case "$COQ_PLATFORM_UNIMATH" in + [yY]) PACKAGES="${PACKAGES} coq-unimath.20230321" ;; + [nN]) true ;; + *) echo "Illegal value for COQ_PLATFORM_UNIMATH - aborting"; false ;; + esac + fi + + # Code extraction + PACKAGES="${PACKAGES} coq-simple-io.1.8.0" + + # Proof automation / generation / helpers + PACKAGES="${PACKAGES} elpi.1.16.9 coq-elpi.1.17.1" + PACKAGES="${PACKAGES} coq-hierarchy-builder.1.4.0" + PACKAGES="${PACKAGES} coq-quickchick.1.6.5" + + # General mathematics (which requires one of the above tools) + PACKAGES="${PACKAGES} coq-mathcomp-analysis.0.6.3" + PACKAGES="${PACKAGES} coq-mathcomp-algebra-tactics.1.1.1" + PACKAGES="${PACKAGES} coq-relation-algebra.1.7.9" + + # Formal languages, compilers and code verification + PACKAGES="${PACKAGES} coq-iris.4.0.0" + PACKAGES="${PACKAGES} coq-iris-heap-lang.4.0.0" + + case "$COQ_PLATFORM_COMPCERT" in + [yY]) PACKAGES="${PACKAGES} coq-compcert.3.12" ;; + [nN]) true ;; + *) echo "Illegal value for COQ_PLATFORM_COMPCERT - aborting"; false ;; + esac + + case "$COQ_PLATFORM_VST" in + [yY]) + PACKAGES="${PACKAGES} coq-vst.2.12" + true ;; + [nN]) true ;; + *) echo "Illegal value for COQ_PLATFORM_VST - aborting"; false ;; + esac + +fi diff --git a/shell_scripts/build.sh b/shell_scripts/build.sh index f4bbec2f71..48cdef93e1 100644 --- a/shell_scripts/build.sh +++ b/shell_scripts/build.sh @@ -34,6 +34,9 @@ opam config set jobs $COQ_PLATFORM_JOBS # One can rise it as root on MacOS, but only for a root shell, not for the current shell ulimit -S -s 65520 +opam pin add -k git -n coq-core.8.17.1 https://github.com/ejgallego/coq.git#v8.17+lsp +opam pin add -k git -n coq-lsp.0.1.7+8.17 https://github.com/ejgallego/coq-lsp.git#v8.17 + case "$COQ_PLATFORM_PARALLEL" in [pP]) echo "===== INSTALL OPAM PACKAGES (PARALLEL) =====" @@ -45,7 +48,7 @@ case "$COQ_PLATFORM_PARALLEL" in echo PINNING $package package_name="$(echo "$package" | cut -d '.' -f 2)" package_version="$(echo "$package" | cut -d '.' -f 3-)" - if ! $COQ_PLATFORM_TIME opam pin ${package_name} ${package_version}; then dump_opam_logs; fi + if ! $COQ_PLATFORM_TIME opam pin add -k version ${package_name} ${package_version}; then dump_opam_logs; fi ;; esac done diff --git a/shell_scripts/installer_create_tree.sh b/shell_scripts/installer_create_tree.sh index 1f9e4c58f1..c51bd643ba 100644 --- a/shell_scripts/installer_create_tree.sh +++ b/shell_scripts/installer_create_tree.sh @@ -82,7 +82,7 @@ OPAM_FILE_EXCLUSION_LIST[coq-compcert-32]=OPAM_FILE_EXCLUSION_LIST[coq-compcert] # Since QuickChick requires OCamlc at run time, it is also excluded OPAM_PACKAGE_EXCLUSION_LIST="ocaml"$'\n'"ocaml-variants"$'\n'"ocaml-base-compiler"$'\n'"ocaml-compiler-libs"$'\n'"ocaml-config"$'\n'"ocaml-secondary-compiler"$'\n'"ocamlfind-secondary"$'\n'"coq-quickchick" -OPAM_PACKAGE_EXCLUSION_LIST="${OPAM_PACKAGE_EXCLUSION_LIST}"$'\n'"sexplib0"$'\n'"csexp"$'\n'"ocamlbuild"$'\n'"cppo" +OPAM_PACKAGE_EXCLUSION_LIST="${OPAM_PACKAGE_EXCLUSION_LIST}"$'\n'"csexp"$'\n'"ocamlbuild"$'\n'"cppo" # Regexp for packages to ignore