From bcdee0e6ce16c7feec1cc68220e243a64dec09ab Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Tue, 26 Sep 2023 14:18:35 +0200
Subject: [PATCH 1/3] [2023.11] [coq-lsp 0.2.0] [v8.20] Draft Windows build

Changes:

- Simplify some paths and logic
- Updated for 8.20
---
 .github/workflows/macos.yml                   | 216 ------------------
 .github/workflows/ubuntu.yml                  |  99 --------
 .github/workflows/ubuntu_dev.yml              |  79 -------
 .github/workflows/windows.yml                 |  66 +-----
 .../package-pick-8.20~2023.11-coq-lsp.sh      | 199 ++++++++++++++++
 shell_scripts/build.sh                        |   4 +-
 windows/create_installer_windows.sh           |   8 +-
 7 files changed, 208 insertions(+), 463 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.20~2023.11-coq-lsp.sh

diff --git a/.github/workflows/macos.yml b/.github/workflows/macos.yml
deleted file mode 100644
index 8d3f59e530..0000000000
--- a/.github/workflows/macos.yml
+++ /dev/null
@@ -1,216 +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:
-          # Keep this in sync with the Smoke test below
-          - '8.19~2024.01+beta1'
-          - '8.18~2023.11'
-          - '8.18~mc2'
-          - '8.17~2023.08'
-    steps:
-      - name: Git checkout
-        uses: actions/checkout@v4
-
-      - 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
-          # make sure we are using homebrew python, since we install some python packages via homebrew
-          brew install python3
-          brew link --overwrite python3
-          ls -l $(which python3)
-          ls -l $(which pip3)
-          # create a virtual environment so that we can use pip3
-          # (since python 3.12 using pip3 on package manager installed python requires a virtual environment)
-          python3 -m venv .venv
-          . .venv/bin/activate
-          # See https://docs.github.com/en/actions/using-workflows/workflow-commands-for-github-actions#setting-an-environment-variable
-          echo PATH=$PATH >> $GITHUB_ENV
-          ls -l $(which python3)
-          ls -l $(which pip3)
-
-      - 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: 'Upload opam log folder on failure'
-        uses: actions/upload-artifact@v4
-        if: failure()
-        with:
-          name: 'Opam log folder ${{matrix.variant}}'
-          path: /Users/runner/.opam/log/
-
-      - name: 'Upload opam build folder on failure'
-        uses: actions/upload-artifact@v4
-        if: failure()
-        with:
-          name: 'Opam build folder ${{matrix.variant}}'
-          path: /Users/runner/.opam/CP*${{matrix.variant}}/.opam-switch/build
-
-      - 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@v4
-        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'
-        uses: Wandalen/wretry.action@v3
-        with:
-          attempt_limit: 5
-          attempt_delay: 5000
-          command: |
-            eval $(opam env)
-            macos/create_installer_macos.sh
-
-      - name: 'Upload DMG script logs on failure'
-        uses: actions/upload-artifact@v4
-        if: failure()
-        with:
-          name: 'DMG script error logs ${{matrix.variant}}'
-          path: macos_installer/logs/
-
-      - name: 'Upload Artifact'
-        uses: actions/upload-artifact@v4
-        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.19~2024.01+beta1'
-          - '8.18~2023.11'
-          - '8.18~mc2'
-          - '8.17~2023.08'
-
-    steps:
-      - name: Install bash
-        run: brew install bash
-
-      - name: 'Download Artifact'
-        uses: actions/download-artifact@v4
-        id: download
-        with:
-          name: 'Macos installer ${{matrix.variant}} x86_64'
-
-      - name: 'Download smoke test kit'
-        uses: actions/download-artifact@v4
-        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: |
-          ls /Applications/Coq-Platform*.app
-          export PATH="$PATH:$(cd /Applications/Coq-Platform*.app/Contents/Resources/bin/; pwd)"
-          export COQLIB=$(coqc -where)
-          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 4376e0c7f0..0000000000
--- a/.github/workflows/ubuntu.yml
+++ /dev/null
@@ -1,99 +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'
-
-###############################################################################
-# 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:
-          # This should contain all picks introduced in the current release + all original picks of all Coq versions
-          - '8.19~2024.01+beta1'
-          - '8.18~2023.11'
-          - '8.18~mc2'
-          - '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@v4
-
-      - 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@v4
-        with:
-          name: 'Smoke Test Kit ${{matrix.variant}}'
-          path: smoke-test-kit
-          retention-days: 5
diff --git a/.github/workflows/ubuntu_dev.yml b/.github/workflows/ubuntu_dev.yml
deleted file mode 100644
index af94f92fd5..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@v4
-
-      - 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@v4
-        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 5c3921eaed..c23728f3c0 100644
--- a/.github/workflows/windows.yml
+++ b/.github/workflows/windows.yml
@@ -51,10 +51,7 @@ jobs:
           - '64'
         variant:
           # Keep this in sync with the Smoke test below
-          - '8.19~2024.01+beta1'
-          - '8.18~2023.11'
-          - '8.18~mc2'
-          - '8.17~2023.08'
+          - '8.20~2023.11-coq-lsp'
 
     steps:
       - name: Set git to use LF
@@ -71,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@v4
@@ -87,56 +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@v4
-        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'
-        variant:
-          - '8.19~2024.01+beta1'
-          - '8.18~2023.11'
-          - '8.18~mc2'
-          - '8.17~2023.08'
-
-    steps:
-      - name: 'Download Artifact'
-        uses: actions/download-artifact@v4
-        id: download
-        with:
-          name: 'Windows installer ${{matrix.variant}} ${{matrix.architecture}}'
-
-      - name: 'Download smoke test kit'
-        uses: actions/download-artifact@v4
-        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.20~2023.11-coq-lsp.sh b/package_picks/package-pick-8.20~2023.11-coq-lsp.sh
new file mode 100644
index 0000000000..38e1260739
--- /dev/null
+++ b/package_picks/package-pick-8.20~2023.11-coq-lsp.sh
@@ -0,0 +1,199 @@
+#!/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.20.0 (released Sep 2024)"
+COQ_PLATFORM_VERSION_SORTORDER=98
+
+# 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.20-lsp'
+
+# The corresponding Coq development branch and tag
+COQ_PLATFORM_COQ_BRANCH='v8.20'
+COQ_PLATFORM_COQ_TAG='8.20.0'
+
+# 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 2024.01.0 includes Coq 8.20.0 from Sep 2024. '
+
+# 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.
+# - 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"  # TODO port patch to 1.9.6
+# Since dune does support Coq, it is explicitly selected
+PACKAGES="${PACKAGES} dune.3.11.1"
+PACKAGES="${PACKAGES} dune-configurator.3.10.0"
+# The Coq compiler coqc and the Coq standard library
+PACKAGES="${PACKAGES} PIN.coq.8.20.0"
+
+########## Coq Language Server ##########
+PACKAGES="${PACKAGES} coq-lsp.0.2.0+8.20"
+
+########## IDE PACKAGES ##########
+
+# GTK based IDE for Coq - alternatives are VSCoq and Proofgeneral for Emacs
+if  [[ "${COQ_PLATFORM_EXTENT}"  =~ ^[iIfFxX] ]]
+then
+PACKAGES="${PACKAGES} coqide.8.19.0"
+fi
+
+########## "FULL" COQ PLATFORM PACKAGES ##########
+
+if  [[ "${COQ_PLATFORM_EXTENT}"  =~ ^[fFxX] ]]
+then
+  # Standard library extensions
+  PACKAGES="${PACKAGES} coq-bignums.9.0.0+coq8.19"
+  PACKAGES="${PACKAGES} coq-ext-lib.0.12.1"
+  #PACKAGES="${PACKAGES} coq-stdpp.1.9.0" does not build
+
+  # General mathematics
+  PACKAGES="${PACKAGES} coq-mathcomp-ssreflect.2.2.0"
+  PACKAGES="${PACKAGES} coq-mathcomp-fingroup.2.2.0"
+  PACKAGES="${PACKAGES} coq-mathcomp-algebra.2.2.0"
+  PACKAGES="${PACKAGES} coq-mathcomp-solvable.2.2.0"
+  PACKAGES="${PACKAGES} coq-mathcomp-field.2.2.0"
+  PACKAGES="${PACKAGES} coq-mathcomp-character.2.2.0"
+  PACKAGES="${PACKAGES} coq-mathcomp-bigenough.1.0.1"
+  PACKAGES="${PACKAGES} coq-mathcomp-finmap.2.1.0"
+  PACKAGES="${PACKAGES} coq-mathcomp-real-closed.2.0.0"
+  PACKAGES="${PACKAGES} coq-mathcomp-zify.1.5.0+2.0+8.16"
+  PACKAGES="${PACKAGES} coq-mathcomp-multinomials.2.2.0"
+  PACKAGES="${PACKAGES} coq-coquelicot.3.4.1"
+
+  # Number theory
+  PACKAGES="${PACKAGES} coq-coqprime.1.5.0"
+  PACKAGES="${PACKAGES} coq-coqprime-generator.1.1.1" #NOTE:THIS IS STILL TAGGED TO v8.14.1, SHOULD SOMETHING BE DONE?
+  
+  # Numerical mathematics
+  PACKAGES="${PACKAGES} coq-flocq.4.1.4"
+  #PACKAGES="${PACKAGES} coq-interval.4.9.0" #DOES NOT BUILD
+  #PACKAGES="${PACKAGES} coq-gappa.1.5.4" #DOES NOT BUILD
+  PACKAGES="${PACKAGES} gappa.1.4.1"
+
+  # Constructive mathematics
+  #PACKAGES="${PACKAGES} coq-math-classes.8.18.0" #DOES NOT BUILD
+  #PACKAGES="${PACKAGES} coq-corn.8.18.0" #DOES NOT BUILD
+
+  # Homotopy Type Theory (HoTT)
+  PACKAGES="${PACKAGES} coq-hott.8.19"
+
+  # 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.20240331" ;;
+    [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} coq-menhirlib.20231231 menhir.20231231"
+  PACKAGES="${PACKAGES} coq-equations.1.3+8.19"
+  PACKAGES="${PACKAGES} coq-aac-tactics.8.19.0"
+  #PACKAGES="${PACKAGES} coq-unicoq.1.6+8.18" #DOES NOT BUILD
+  #PACKAGES="${PACKAGES} coq-mtac2.1.4+8.18" #DOES NOT BUILD, DEPENDS ON UNICOQ
+  PACKAGES="${PACKAGES} elpi.1.19.6 coq-elpi.2.2.3"
+  PACKAGES="${PACKAGES} coq-hierarchy-builder.1.7.0"
+  PACKAGES="${PACKAGES} coq-quickchick.2.0.2"
+  #PACKAGES="${PACKAGES} coq-hammer-tactics.1.3.2+8.18" # DOES NOT BUILD
+  if [[ "$OSTYPE" != cygwin ]]
+  then
+    # coq-hammer does not work on Windows because it heavily relies on fork
+    #PACKAGES="${PACKAGES} coq-hammer.1.3.2+8.18" # DEPENDS ON COQ-HAMMER-TACTICS
+    PACKAGES="${PACKAGES} eprover.3.0"
+    PACKAGES="${PACKAGES} z3_tptp.4.11.2"  # 4.12.2-1 has build issues on ARM macOS
+  fi
+  PACKAGES="${PACKAGES} coq-paramcoq.1.1.3+coq8.19"
+  PACKAGES="${PACKAGES} coq-coqeal.2.0.1"
+  PACKAGES="${PACKAGES} coq-libhyps.2.0.8"
+  PACKAGES="${PACKAGES} coq-itauto.8.19.0"
+  
+  # General mathematics (which requires one of the above tools)
+  PACKAGES="${PACKAGES} coq-mathcomp-analysis.0.7.0"
+  PACKAGES="${PACKAGES} coq-mathcomp-algebra-tactics.1.2.3"
+  PACKAGES="${PACKAGES} coq-relation-algebra.1.7.10"
+
+  # Formal languages, compilers and code verification
+  PACKAGES="${PACKAGES} coq-reglang.1.2.1"
+  PACKAGES="${PACKAGES} coq-iris.4.1.0"
+  PACKAGES="${PACKAGES} coq-iris-heap-lang.4.1.0"
+  if [[ "$OSTYPE" != cygwin ]]
+  then
+    # Windows: some issues with executable extensions (ott.opt instead of ott.exe)
+    # Note: 0.32 does work on Windows!
+    PACKAGES="${PACKAGES} coq-ott.0.33"
+    PACKAGES="${PACKAGES} ott.0.33"
+  fi
+  PACKAGES="${PACKAGES} coq-mathcomp-word.3.0"
+  
+  case "$COQ_PLATFORM_COMPCERT" in
+    [yY]) PACKAGES="${PACKAGES} coq-compcert.3.13.1" ;;
+    [nN]) true ;;
+    *) echo "Illegal value for COQ_PLATFORM_COMPCERT - aborting"; false ;;
+  esac
+
+  case "$COQ_PLATFORM_VST" in
+    [yY])
+      PACKAGES="${PACKAGES} coq-vst.2.13"
+      true ;;
+    [nN]) true ;;
+    *) echo "Illegal value for COQ_PLATFORM_VST - aborting"; false ;;
+  esac
+
+  # # Proof analysis and other tools
+  PACKAGES="${PACKAGES} coq-dpdgraph.1.0+8.19"
+fi
+
+########## EXTENDED" COQ PLATFORM PACKAGES ##########
+
+if  [[ "${COQ_PLATFORM_EXTENT}"  =~ ^[xX] ]]
+then
+
+  # Proof automation / generation / helpers
+  PACKAGES="${PACKAGES} coq-deriving.0.2.0"
+  if [ "${BITSIZE}" == "64" ]
+  then
+    PACKAGES="${PACKAGES} coq-metacoq.1.2.1+8.18"
+  fi
+
+  # General mathematics
+  PACKAGES="${PACKAGES} coq-extructures.0.4.0"
+
+  # Gallina extensions
+  PACKAGES="${PACKAGES} coq-reduction-effects.0.1.5"
+  PACKAGES="${PACKAGES} coq-record-update.0.3.3"
+
+fi
diff --git a/shell_scripts/build.sh b/shell_scripts/build.sh
index fe0a91f35d..fd5ba95fcf 100644
--- a/shell_scripts/build.sh
+++ b/shell_scripts/build.sh
@@ -34,6 +34,8 @@ 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.20.0 https://github.com/ejgallego/coq.git#v8.20+lsp
+
 case "$COQ_PLATFORM_PARALLEL" in
   [pP]) 
     echo "===== INSTALL OPAM PACKAGES (PARALLEL) ====="
@@ -45,7 +47,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 --no-action ${package_name} ${package_version}; then dump_opam_logs; fi
+        if ! $COQ_PLATFORM_TIME opam pin --no-action add -k version ${package_name} ${package_version}; then dump_opam_logs; fi
         ;;
       esac
     done
diff --git a/windows/create_installer_windows.sh b/windows/create_installer_windows.sh
index b9564d2da1..404ee882cf 100755
--- a/windows/create_installer_windows.sh
+++ b/windows/create_installer_windows.sh
@@ -462,11 +462,9 @@ cp source/coq/LICENSE .
 cp source/coqide/ide/coqide/coq.ico .
 mkdir -p files/bin
 cp source/coqide/ide/coqide/coq.ico files/bin/
-cp source/coq-compcert/LICENSE coq-compcert-license.txt
-if [ -n "$NSIS_VST_CHECK" ]
-then
-  cp source/$vst_pkg/LICENSE coq-vst-license.txt
-fi
+# cp source/coq-compcert/LICENSE coq-compcert-license.txt
+echo "FAKE COMPCERT LICENSE" > coq-compcert-license.txt
+echo "FAKE VST LICENSE" > coq-vst-license.txt
 rm -rf source
 
 echo "==============================================================================="

From c1dd3285ac7fd0184cf32a15606879515903f27f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Thu, 8 Feb 2024 12:57:37 +0100
Subject: [PATCH 2/3] [tmp] removed some stuff seemingly not ready for 8.20

---
 .../package-pick-8.20~2023.11-coq-lsp.sh      | 98 +++----------------
 1 file changed, 15 insertions(+), 83 deletions(-)

diff --git a/package_picks/package-pick-8.20~2023.11-coq-lsp.sh b/package_picks/package-pick-8.20~2023.11-coq-lsp.sh
index 38e1260739..5e52dacff5 100644
--- a/package_picks/package-pick-8.20~2023.11-coq-lsp.sh
+++ b/package_picks/package-pick-8.20~2023.11-coq-lsp.sh
@@ -89,111 +89,43 @@ then
   PACKAGES="${PACKAGES} coq-coquelicot.3.4.1"
 
   # Number theory
-  PACKAGES="${PACKAGES} coq-coqprime.1.5.0"
-  PACKAGES="${PACKAGES} coq-coqprime-generator.1.1.1" #NOTE:THIS IS STILL TAGGED TO v8.14.1, SHOULD SOMETHING BE DONE?
-  
+  # PACKAGES="${PACKAGES} coq-coqprime.1.5.0"
+  # PACKAGES="${PACKAGES} coq-coqprime-generator.1.1.1" #NOTE:THIS IS STILL TAGGED TO v8.14.1, SHOULD SOMETHING BE DONE?
+
   # Numerical mathematics
-  PACKAGES="${PACKAGES} coq-flocq.4.1.4"
+  # PACKAGES="${PACKAGES} coq-flocq.4.1.4"
   #PACKAGES="${PACKAGES} coq-interval.4.9.0" #DOES NOT BUILD
   #PACKAGES="${PACKAGES} coq-gappa.1.5.4" #DOES NOT BUILD
-  PACKAGES="${PACKAGES} gappa.1.4.1"
+  # PACKAGES="${PACKAGES} gappa.1.4.1"
 
   # Constructive mathematics
   #PACKAGES="${PACKAGES} coq-math-classes.8.18.0" #DOES NOT BUILD
   #PACKAGES="${PACKAGES} coq-corn.8.18.0" #DOES NOT BUILD
 
   # Homotopy Type Theory (HoTT)
-  PACKAGES="${PACKAGES} coq-hott.8.19"
-
-  # 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.20240331" ;;
-    [nN]) true ;;
-    *) echo "Illegal value for COQ_PLATFORM_UNIMATH - aborting"; false ;;
-    esac
-  fi 
+  # PACKAGES="${PACKAGES} coq-hott.8.18"
 
   # Code extraction
   PACKAGES="${PACKAGES} coq-simple-io.1.8.0"
 
   # Proof automation / generation / helpers
-  PACKAGES="${PACKAGES} coq-menhirlib.20231231 menhir.20231231"
+  # PACKAGES="${PACKAGES} coq-menhirlib.20231231 menhir.20231231"
   PACKAGES="${PACKAGES} coq-equations.1.3+8.19"
   PACKAGES="${PACKAGES} coq-aac-tactics.8.19.0"
-  #PACKAGES="${PACKAGES} coq-unicoq.1.6+8.18" #DOES NOT BUILD
-  #PACKAGES="${PACKAGES} coq-mtac2.1.4+8.18" #DOES NOT BUILD, DEPENDS ON UNICOQ
   PACKAGES="${PACKAGES} elpi.1.19.6 coq-elpi.2.2.3"
   PACKAGES="${PACKAGES} coq-hierarchy-builder.1.7.0"
-  PACKAGES="${PACKAGES} coq-quickchick.2.0.2"
-  #PACKAGES="${PACKAGES} coq-hammer-tactics.1.3.2+8.18" # DOES NOT BUILD
-  if [[ "$OSTYPE" != cygwin ]]
-  then
-    # coq-hammer does not work on Windows because it heavily relies on fork
-    #PACKAGES="${PACKAGES} coq-hammer.1.3.2+8.18" # DEPENDS ON COQ-HAMMER-TACTICS
-    PACKAGES="${PACKAGES} eprover.3.0"
-    PACKAGES="${PACKAGES} z3_tptp.4.11.2"  # 4.12.2-1 has build issues on ARM macOS
-  fi
+
+  # BROKEN in CI
+  # PACKAGES="${PACKAGES} coq-quickchick.2.0.2"
+
   PACKAGES="${PACKAGES} coq-paramcoq.1.1.3+coq8.19"
   PACKAGES="${PACKAGES} coq-coqeal.2.0.1"
   PACKAGES="${PACKAGES} coq-libhyps.2.0.8"
-  PACKAGES="${PACKAGES} coq-itauto.8.19.0"
-  
+  # BROKEN in CI
+  # PACKAGES="${PACKAGES} coq-itauto.8.19.0"
+
   # General mathematics (which requires one of the above tools)
-  PACKAGES="${PACKAGES} coq-mathcomp-analysis.0.7.0"
+  PACKAGES="${PACKAGES} coq-mathcomp-analysis.1.0.0"
   PACKAGES="${PACKAGES} coq-mathcomp-algebra-tactics.1.2.3"
-  PACKAGES="${PACKAGES} coq-relation-algebra.1.7.10"
-
-  # Formal languages, compilers and code verification
-  PACKAGES="${PACKAGES} coq-reglang.1.2.1"
-  PACKAGES="${PACKAGES} coq-iris.4.1.0"
-  PACKAGES="${PACKAGES} coq-iris-heap-lang.4.1.0"
-  if [[ "$OSTYPE" != cygwin ]]
-  then
-    # Windows: some issues with executable extensions (ott.opt instead of ott.exe)
-    # Note: 0.32 does work on Windows!
-    PACKAGES="${PACKAGES} coq-ott.0.33"
-    PACKAGES="${PACKAGES} ott.0.33"
-  fi
-  PACKAGES="${PACKAGES} coq-mathcomp-word.3.0"
-  
-  case "$COQ_PLATFORM_COMPCERT" in
-    [yY]) PACKAGES="${PACKAGES} coq-compcert.3.13.1" ;;
-    [nN]) true ;;
-    *) echo "Illegal value for COQ_PLATFORM_COMPCERT - aborting"; false ;;
-  esac
-
-  case "$COQ_PLATFORM_VST" in
-    [yY])
-      PACKAGES="${PACKAGES} coq-vst.2.13"
-      true ;;
-    [nN]) true ;;
-    *) echo "Illegal value for COQ_PLATFORM_VST - aborting"; false ;;
-  esac
-
-  # # Proof analysis and other tools
-  PACKAGES="${PACKAGES} coq-dpdgraph.1.0+8.19"
-fi
-
-########## EXTENDED" COQ PLATFORM PACKAGES ##########
-
-if  [[ "${COQ_PLATFORM_EXTENT}"  =~ ^[xX] ]]
-then
-
-  # Proof automation / generation / helpers
-  PACKAGES="${PACKAGES} coq-deriving.0.2.0"
-  if [ "${BITSIZE}" == "64" ]
-  then
-    PACKAGES="${PACKAGES} coq-metacoq.1.2.1+8.18"
-  fi
-
-  # General mathematics
-  PACKAGES="${PACKAGES} coq-extructures.0.4.0"
-
-  # Gallina extensions
-  PACKAGES="${PACKAGES} coq-reduction-effects.0.1.5"
-  PACKAGES="${PACKAGES} coq-record-update.0.3.3"
 
 fi

From 71c1234a51455c3098ec8c621429edebedaf7fad Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 16 Sep 2024 10:19:09 +0200
Subject: [PATCH 3/3] [tmp] More 8.20 stuff

---
 .../package-pick-8.20~2023.11-coq-lsp.sh      | 20 +++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/package_picks/package-pick-8.20~2023.11-coq-lsp.sh b/package_picks/package-pick-8.20~2023.11-coq-lsp.sh
index 5e52dacff5..4a35cb3619 100644
--- a/package_picks/package-pick-8.20~2023.11-coq-lsp.sh
+++ b/package_picks/package-pick-8.20~2023.11-coq-lsp.sh
@@ -49,7 +49,7 @@ PACKAGES=""
 # Coq needs a patched ocamlfind to be relocatable by installers
 PACKAGES="${PACKAGES} PIN.ocamlfind.1.9.5~relocatable"  # TODO port patch to 1.9.6
 # Since dune does support Coq, it is explicitly selected
-PACKAGES="${PACKAGES} dune.3.11.1"
+PACKAGES="${PACKAGES} dune.3.16.0"
 PACKAGES="${PACKAGES} dune-configurator.3.10.0"
 # The Coq compiler coqc and the Coq standard library
 PACKAGES="${PACKAGES} PIN.coq.8.20.0"
@@ -70,8 +70,8 @@ fi
 if  [[ "${COQ_PLATFORM_EXTENT}"  =~ ^[fFxX] ]]
 then
   # Standard library extensions
-  PACKAGES="${PACKAGES} coq-bignums.9.0.0+coq8.19"
-  PACKAGES="${PACKAGES} coq-ext-lib.0.12.1"
+  PACKAGES="${PACKAGES} coq-bignums.9.0.0+coq8.20"
+  PACKAGES="${PACKAGES} coq-ext-lib.0.12.2"
   #PACKAGES="${PACKAGES} coq-stdpp.1.9.0" does not build
 
   # General mathematics
@@ -85,8 +85,8 @@ then
   PACKAGES="${PACKAGES} coq-mathcomp-finmap.2.1.0"
   PACKAGES="${PACKAGES} coq-mathcomp-real-closed.2.0.0"
   PACKAGES="${PACKAGES} coq-mathcomp-zify.1.5.0+2.0+8.16"
-  PACKAGES="${PACKAGES} coq-mathcomp-multinomials.2.2.0"
-  PACKAGES="${PACKAGES} coq-coquelicot.3.4.1"
+  # PACKAGES="${PACKAGES} coq-mathcomp-multinomials.2.2.0"
+  PACKAGES="${PACKAGES} coq-coquelicot.3.4.2"
 
   # Number theory
   # PACKAGES="${PACKAGES} coq-coqprime.1.5.0"
@@ -103,22 +103,22 @@ then
   #PACKAGES="${PACKAGES} coq-corn.8.18.0" #DOES NOT BUILD
 
   # Homotopy Type Theory (HoTT)
-  # PACKAGES="${PACKAGES} coq-hott.8.18"
+  # PACKAGES="${PACKAGES} coq-hott.8.20"
 
   # Code extraction
-  PACKAGES="${PACKAGES} coq-simple-io.1.8.0"
+  PACKAGES="${PACKAGES} coq-simple-io.1.9.0"
 
   # Proof automation / generation / helpers
   # PACKAGES="${PACKAGES} coq-menhirlib.20231231 menhir.20231231"
-  PACKAGES="${PACKAGES} coq-equations.1.3+8.19"
-  PACKAGES="${PACKAGES} coq-aac-tactics.8.19.0"
+  PACKAGES="${PACKAGES} coq-equations.1.3.1+8.20"
+  # PACKAGES="${PACKAGES} coq-aac-tactics.8.19.0"
   PACKAGES="${PACKAGES} elpi.1.19.6 coq-elpi.2.2.3"
   PACKAGES="${PACKAGES} coq-hierarchy-builder.1.7.0"
 
   # BROKEN in CI
   # PACKAGES="${PACKAGES} coq-quickchick.2.0.2"
 
-  PACKAGES="${PACKAGES} coq-paramcoq.1.1.3+coq8.19"
+  PACKAGES="${PACKAGES} coq-paramcoq.1.1.3+coq8.20"
   PACKAGES="${PACKAGES} coq-coqeal.2.0.1"
   PACKAGES="${PACKAGES} coq-libhyps.2.0.8"
   # BROKEN in CI