From d278742f77deca14a72ddf158e0e5226526179c3 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 11 Apr 2024 09:46:02 +0200
Subject: [PATCH 01/38] Test tactician

---
 .github/workflows/macos.yml                  | 18 +++---
 .github/workflows/ubuntu.yml                 | 21 +++----
 .github/workflows/windows.yml                | 18 +++---
 package_picks/package-pick-8.18~tactician.sh | 61 ++++++++++++++++++++
 4 files changed, 92 insertions(+), 26 deletions(-)
 create mode 100644 package_picks/package-pick-8.18~tactician.sh

diff --git a/.github/workflows/macos.yml b/.github/workflows/macos.yml
index 4f5989691e..5ebe938a61 100644
--- a/.github/workflows/macos.yml
+++ b/.github/workflows/macos.yml
@@ -51,10 +51,11 @@ jobs:
       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'
+          - '8.18~tactician'
+          # - '8.19~2024.01+beta1'
+          # - '8.18~2023.11'
+          # - '8.18~mc2'
+          # - '8.17~2023.08'
     steps:
       - name: Git checkout
         uses: actions/checkout@v3
@@ -155,10 +156,11 @@ jobs:
       fail-fast: false
       matrix:
         variant:
-          - '8.19~2024.01+beta1'
-          - '8.18~2023.11'
-          - '8.18~mc2'
-          - '8.17~2023.08'
+          - '8.18~tactician'
+          # - '8.19~2024.01+beta1'
+          # - '8.18~2023.11'
+          # - '8.18~mc2'
+          # - '8.17~2023.08'
 
     steps:
       - name: Install bash
diff --git a/.github/workflows/ubuntu.yml b/.github/workflows/ubuntu.yml
index 58da356181..4bcea90c6d 100644
--- a/.github/workflows/ubuntu.yml
+++ b/.github/workflows/ubuntu.yml
@@ -58,16 +58,17 @@ jobs:
       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'
+          - '8.18~tactician'
+          # - '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
diff --git a/.github/workflows/windows.yml b/.github/workflows/windows.yml
index 3333335c06..4407904010 100644
--- a/.github/workflows/windows.yml
+++ b/.github/workflows/windows.yml
@@ -52,10 +52,11 @@ jobs:
           - '32'
         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.18~tactician'
+          # - '8.19~2024.01+beta1'
+          # - '8.18~2023.11'
+          # - '8.18~mc2'
+          # - '8.17~2023.08'
 
     steps:
       - name: Set git to use LF
@@ -107,10 +108,11 @@ jobs:
           - '64'
           - '32'
         variant:
-          - '8.19~2024.01+beta1'
-          - '8.18~2023.11'
-          - '8.18~mc2'
-          - '8.17~2023.08'
+          - '8.18~tactician'
+          # - '8.19~2024.01+beta1'
+          # - '8.18~2023.11'
+          # - '8.18~mc2'
+          # - '8.17~2023.08'
 
     steps:
       - name: 'Download Artifact'
diff --git a/package_picks/package-pick-8.18~tactician.sh b/package_picks/package-pick-8.18~tactician.sh
new file mode 100644
index 0000000000..0a0c08d6e2
--- /dev/null
+++ b/package_picks/package-pick-8.18~tactician.sh
@@ -0,0 +1,61 @@
+#!/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.18.0 (released Sep 2023) with Tactician"
+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.18~tactician'
+
+# The corresponding Coq development branch and tag
+COQ_PLATFORM_COQ_BRANCH='v8.18'
+COQ_PLATFORM_COQ_TAG='8.18.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 2023.11.0 includes Coq 8.18.0 from Sep 2023 and Tactician.'
+
+# 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"  # 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.18.0"
+
+########## IDE PACKAGES ##########
+
+PACKAGES="${PACKAGES} coqide.8.18.0"
+
+PACKAGES="${PACKAGES} coq-tactician-dummy.1.0~beta2+8.17 1.0~beta2.1+8.18"

From 98f9f0bad1d2b9a263f1de148057a1b3e0420a5d Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 11 Apr 2024 09:48:23 +0200
Subject: [PATCH 02/38] Run CI on tactician branch

---
 .github/workflows/macos.yml   | 1 +
 .github/workflows/ubuntu.yml  | 1 +
 .github/workflows/windows.yml | 1 +
 3 files changed, 3 insertions(+)

diff --git a/.github/workflows/macos.yml b/.github/workflows/macos.yml
index 4f5989691e..bb61d74d47 100644
--- a/.github/workflows/macos.yml
+++ b/.github/workflows/macos.yml
@@ -15,6 +15,7 @@ on:
       - 2021.02
       - 2021.09
       - main
+      - tactician
   pull_request:
     branches:
       - '**'
diff --git a/.github/workflows/ubuntu.yml b/.github/workflows/ubuntu.yml
index 58da356181..010f20303a 100644
--- a/.github/workflows/ubuntu.yml
+++ b/.github/workflows/ubuntu.yml
@@ -15,6 +15,7 @@ on:
       - 2021.02
       - 2021.09
       - main
+      - tactician
   pull_request:
     branches:
       - '**'
diff --git a/.github/workflows/windows.yml b/.github/workflows/windows.yml
index 3333335c06..bde78339da 100644
--- a/.github/workflows/windows.yml
+++ b/.github/workflows/windows.yml
@@ -13,6 +13,7 @@ on:
   push:
     branches:
       - main
+      - tactician
   pull_request:
     branches:
       - '**'

From 09c13ad4e56ea1cac8dd6915f8e31f5f8e021ed8 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 11 Apr 2024 09:55:43 +0200
Subject: [PATCH 03/38] Typo

---
 package_picks/package-pick-8.18~tactician.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/package_picks/package-pick-8.18~tactician.sh b/package_picks/package-pick-8.18~tactician.sh
index 0a0c08d6e2..2c560f6199 100644
--- a/package_picks/package-pick-8.18~tactician.sh
+++ b/package_picks/package-pick-8.18~tactician.sh
@@ -58,4 +58,4 @@ PACKAGES="${PACKAGES} PIN.coq.8.18.0"
 
 PACKAGES="${PACKAGES} coqide.8.18.0"
 
-PACKAGES="${PACKAGES} coq-tactician-dummy.1.0~beta2+8.17 1.0~beta2.1+8.18"
+PACKAGES="${PACKAGES} coq-tactician-dummy.1.0~beta2+8.17 coq-tactician.1.0~beta2.1+8.18"

From 6ae7b8b476de5d3c9b610f38af01a1d65ebdccaf Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 11 Apr 2024 10:02:16 +0200
Subject: [PATCH 04/38] downgrade dune

---
 package_picks/package-pick-8.18~tactician.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/package_picks/package-pick-8.18~tactician.sh b/package_picks/package-pick-8.18~tactician.sh
index 2c560f6199..d08b679410 100644
--- a/package_picks/package-pick-8.18~tactician.sh
+++ b/package_picks/package-pick-8.18~tactician.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.7.1"
 PACKAGES="${PACKAGES} dune-configurator.3.10.0"
 # The Coq compiler coqc and the Coq standard library
 PACKAGES="${PACKAGES} PIN.coq.8.18.0"

From 8da081020f54e9f77aff5eca6ab5fe4579bbb929 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 11 Apr 2024 10:32:12 +0200
Subject: [PATCH 05/38] Inject tactician

---
 shell_scripts/build.sh | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/shell_scripts/build.sh b/shell_scripts/build.sh
index f4bbec2f71..f0bc334c20 100644
--- a/shell_scripts/build.sh
+++ b/shell_scripts/build.sh
@@ -34,11 +34,15 @@ 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
 
+if ! $COQ_PLATFORM_TIME opam install coq-core.8.18.0 coq-tactician.1.0~beta2.1+8.18; then dump_opam_logs; fi
+
+tactician inject
+
 case "$COQ_PLATFORM_PARALLEL" in
-  [pP]) 
-    echo "===== INSTALL OPAM PACKAGES (PARALLEL) ====="
-    if ! $COQ_PLATFORM_TIME opam install ${PACKAGES//PIN.}; then dump_opam_logs; fi
-    for package in ${PACKAGES}
+    [pP]) 
+        echo "===== INSTALL OPAM PACKAGES (PARALLEL) ====="
+        if ! $COQ_PLATFORM_TIME opam install ${PACKAGES//PIN.}; then dump_opam_logs; fi
+        for package in ${PACKAGES}
     do
       case $package in
       PIN.*)

From 96438063bba117aac106a08e07e07eff491f1b80 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 11 Apr 2024 11:01:50 +0200
Subject: [PATCH 06/38] Debug

---
 shell_scripts/build.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/shell_scripts/build.sh b/shell_scripts/build.sh
index f0bc334c20..f7964fd4b0 100644
--- a/shell_scripts/build.sh
+++ b/shell_scripts/build.sh
@@ -36,7 +36,7 @@ ulimit -S -s 65520
 
 if ! $COQ_PLATFORM_TIME opam install coq-core.8.18.0 coq-tactician.1.0~beta2.1+8.18; then dump_opam_logs; fi
 
-tactician inject
+eval $(opam env --set-switch --switch ${COQ_PLATFORM_SWITCH_NAME}) && tactician inject
 
 case "$COQ_PLATFORM_PARALLEL" in
     [pP]) 

From 6b00bdd3431ed59052d627a565d8676250db15dc Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 11 Apr 2024 11:18:45 +0200
Subject: [PATCH 07/38] Debug

---
 shell_scripts/build.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/shell_scripts/build.sh b/shell_scripts/build.sh
index f7964fd4b0..2070bd77b8 100644
--- a/shell_scripts/build.sh
+++ b/shell_scripts/build.sh
@@ -36,7 +36,7 @@ ulimit -S -s 65520
 
 if ! $COQ_PLATFORM_TIME opam install coq-core.8.18.0 coq-tactician.1.0~beta2.1+8.18; then dump_opam_logs; fi
 
-eval $(opam env --set-switch --switch ${COQ_PLATFORM_SWITCH_NAME}) && tactician inject
+eval $(opam env --switch ${COQ_PLATFORM_SWITCH_NAME}) && tactician inject
 
 case "$COQ_PLATFORM_PARALLEL" in
     [pP]) 

From aac260c03766d341b4f05129a1568700170b298f Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 11 Apr 2024 11:19:53 +0200
Subject: [PATCH 08/38] Debug

---
 shell_scripts/build.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/shell_scripts/build.sh b/shell_scripts/build.sh
index 2070bd77b8..6e3c68e3a8 100644
--- a/shell_scripts/build.sh
+++ b/shell_scripts/build.sh
@@ -36,7 +36,7 @@ ulimit -S -s 65520
 
 if ! $COQ_PLATFORM_TIME opam install coq-core.8.18.0 coq-tactician.1.0~beta2.1+8.18; then dump_opam_logs; fi
 
-eval $(opam env --switch ${COQ_PLATFORM_SWITCH_NAME}) && tactician inject
+opam exec -- tactician inject
 
 case "$COQ_PLATFORM_PARALLEL" in
     [pP]) 

From 1468bf2d986aa6479c06046c0725119c938572e7 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 11 Apr 2024 11:37:36 +0200
Subject: [PATCH 09/38] debug3

---
 shell_scripts/build.sh | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/shell_scripts/build.sh b/shell_scripts/build.sh
index 6e3c68e3a8..36fbaa706c 100644
--- a/shell_scripts/build.sh
+++ b/shell_scripts/build.sh
@@ -36,6 +36,10 @@ ulimit -S -s 65520
 
 if ! $COQ_PLATFORM_TIME opam install coq-core.8.18.0 coq-tactician.1.0~beta2.1+8.18; then dump_opam_logs; fi
 
+opam switch
+
+opam env
+
 opam exec -- tactician inject
 
 case "$COQ_PLATFORM_PARALLEL" in

From 2ddddd327a02dd84d9cb6ad6ca6e2424119bcd1c Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 11 Apr 2024 11:56:57 +0200
Subject: [PATCH 10/38] debug4

---
 shell_scripts/build.sh | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/shell_scripts/build.sh b/shell_scripts/build.sh
index 36fbaa706c..84fa03db7d 100644
--- a/shell_scripts/build.sh
+++ b/shell_scripts/build.sh
@@ -37,8 +37,10 @@ ulimit -S -s 65520
 if ! $COQ_PLATFORM_TIME opam install coq-core.8.18.0 coq-tactician.1.0~beta2.1+8.18; then dump_opam_logs; fi
 
 opam switch
-
-opam env
+opam switch set ${COQ_PLATFORM_SWITCH_NAME}
+opam switch
+eval $(opam env --set-switch --switch ${COQ_PLATFORM_SWITCH_NAME})
+opam switch
 
 opam exec -- tactician inject
 

From bd8cab817c8bf71151d9d358fad4ffd75f084546 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 11 Apr 2024 12:56:39 +0200
Subject: [PATCH 11/38] debug5

---
 package_picks/package-pick-8.18~tactician.sh | 5 +----
 shell_scripts/build.sh                       | 2 +-
 2 files changed, 2 insertions(+), 5 deletions(-)

diff --git a/package_picks/package-pick-8.18~tactician.sh b/package_picks/package-pick-8.18~tactician.sh
index d08b679410..029d03a936 100644
--- a/package_picks/package-pick-8.18~tactician.sh
+++ b/package_picks/package-pick-8.18~tactician.sh
@@ -25,7 +25,7 @@ COQ_PLATFORM_COQ_BRANCH='v8.18'
 COQ_PLATFORM_COQ_TAG='8.18.0'
 
 # This controls if opam repositories for development packages are selected
-COQ_PLATFORM_USE_DEV_REPOSITORY='N'
+COQ_PLATFORM_USE_DEV_REPOSITORY='Y'
 
 # This extended descriptions is used for readme files
 COQ_PLATFORM_VERSION_DESCRIPTION='This version of Coq Platform 2023.11.0 includes Coq 8.18.0 from Sep 2023 and Tactician.'
@@ -48,9 +48,6 @@ 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.7.1"
-PACKAGES="${PACKAGES} dune-configurator.3.10.0"
 # The Coq compiler coqc and the Coq standard library
 PACKAGES="${PACKAGES} PIN.coq.8.18.0"
 
diff --git a/shell_scripts/build.sh b/shell_scripts/build.sh
index 84fa03db7d..d1b388a9c0 100644
--- a/shell_scripts/build.sh
+++ b/shell_scripts/build.sh
@@ -34,7 +34,7 @@ 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
 
-if ! $COQ_PLATFORM_TIME opam install coq-core.8.18.0 coq-tactician.1.0~beta2.1+8.18; then dump_opam_logs; fi
+if ! $COQ_PLATFORM_TIME opam install --ignore-constraints-on=coq-tactician dune.3.15.0 coq-core.8.18.0 coq-tactician.1.0~beta2.1+8.18; then dump_opam_logs; fi
 
 opam switch
 opam switch set ${COQ_PLATFORM_SWITCH_NAME}

From dbd34f7aa451b90a9124bcc04c43771f1449ff61 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 11 Apr 2024 13:04:58 +0200
Subject: [PATCH 12/38] debug6

---
 shell_scripts/build.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/shell_scripts/build.sh b/shell_scripts/build.sh
index d1b388a9c0..84c0bb8a8f 100644
--- a/shell_scripts/build.sh
+++ b/shell_scripts/build.sh
@@ -34,7 +34,7 @@ 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
 
-if ! $COQ_PLATFORM_TIME opam install --ignore-constraints-on=coq-tactician dune.3.15.0 coq-core.8.18.0 coq-tactician.1.0~beta2.1+8.18; then dump_opam_logs; fi
+if ! $COQ_PLATFORM_TIME opam install --ignore-constraints-on="coq-tactician,dune,coq-core" dune.3.15.0 coq-core.8.18.0 coq-tactician.1.0~beta2.1+8.18; then dump_opam_logs; fi
 
 opam switch
 opam switch set ${COQ_PLATFORM_SWITCH_NAME}

From 51066ff7c3596dd1e321cfc8614529d8e17ce6a9 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 11 Apr 2024 14:05:59 +0200
Subject: [PATCH 13/38] Debug 7

---
 package_picks/package-pick-8.18~tactician.sh | 2 --
 shell_scripts/build.sh                       | 2 +-
 2 files changed, 1 insertion(+), 3 deletions(-)

diff --git a/package_picks/package-pick-8.18~tactician.sh b/package_picks/package-pick-8.18~tactician.sh
index 029d03a936..5b4d969fb9 100644
--- a/package_picks/package-pick-8.18~tactician.sh
+++ b/package_picks/package-pick-8.18~tactician.sh
@@ -54,5 +54,3 @@ PACKAGES="${PACKAGES} PIN.coq.8.18.0"
 ########## IDE PACKAGES ##########
 
 PACKAGES="${PACKAGES} coqide.8.18.0"
-
-PACKAGES="${PACKAGES} coq-tactician-dummy.1.0~beta2+8.17 coq-tactician.1.0~beta2.1+8.18"
diff --git a/shell_scripts/build.sh b/shell_scripts/build.sh
index 84c0bb8a8f..e285e7b199 100644
--- a/shell_scripts/build.sh
+++ b/shell_scripts/build.sh
@@ -34,7 +34,7 @@ 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
 
-if ! $COQ_PLATFORM_TIME opam install --ignore-constraints-on="coq-tactician,dune,coq-core" dune.3.15.0 coq-core.8.18.0 coq-tactician.1.0~beta2.1+8.18; then dump_opam_logs; fi
+if ! $COQ_PLATFORM_TIME opam install --ignore-constraints-on="coq-tactician,dune,coq-core" dune.3.15.0 coq-tactician-dummy.1.0~beta2+8.17 coq-core.8.18.0 coq-tactician.1.0~beta2.1+8.18; then dump_opam_logs; fi
 
 opam switch
 opam switch set ${COQ_PLATFORM_SWITCH_NAME}

From 124dbf641763c9e5dc47b4f4ff2d7ed201703189 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 11 Apr 2024 14:08:16 +0200
Subject: [PATCH 14/38] Disable smoke tests

---
 .github/workflows/macos.yml   | 134 +++++++++++++++++-----------------
 .github/workflows/ubuntu.yml  | 110 ++++++++++++++--------------
 .github/workflows/windows.yml | 114 ++++++++++++++---------------
 3 files changed, 179 insertions(+), 179 deletions(-)

diff --git a/.github/workflows/macos.yml b/.github/workflows/macos.yml
index 518acba325..37b89816a0 100644
--- a/.github/workflows/macos.yml
+++ b/.github/workflows/macos.yml
@@ -106,19 +106,19 @@ jobs:
       - 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@v3
-        with:
-          name: 'Smoke Test Kit Macos ${{matrix.variant}}'
-          path: smoke-test-kit/
-          retention-days: 5
+      # - 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@v3
+      #   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: |
@@ -149,57 +149,57 @@ jobs:
           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.18~tactician'
-          # - '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@v3
-        id: download
-        with:
-          name: 'Macos installer ${{matrix.variant}} x86_64'
-
-      - name: 'Download smoke test kit'
-        uses: actions/download-artifact@v3
-        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
+  # Macos_smoke:
+  #   name: Smoke test Macos
+  #   needs: Macos_platform
+  #   runs-on: macos-latest
+  #   strategy:
+  #     fail-fast: false
+  #     matrix:
+  #       variant:
+  #         - '8.18~tactician'
+  #         # - '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@v3
+  #       id: download
+  #       with:
+  #         name: 'Macos installer ${{matrix.variant}} x86_64'
+
+  #     - name: 'Download smoke test kit'
+  #       uses: actions/download-artifact@v3
+  #       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
index 2018abbac1..6f0a9318c9 100644
--- a/.github/workflows/ubuntu.yml
+++ b/.github/workflows/ubuntu.yml
@@ -29,7 +29,7 @@ on:
         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.18~2023.11
+        default: 8.18~tactician
       upload:
         description: 'Upload artifact to Snap Store? (true/false, default false)'
         default: false
@@ -40,7 +40,7 @@ on:
 env:
   PLATFORM: -extent=x -parallel=p -jobs=2 -large=i -compcert=y -unimath=n -set-switch=y
   COQREGTESTING: y
-  SNAP_PICK: 8.18~2023.11
+  SNAP_PICK: 8.18~tactician
 
 
 ###############################################################################
@@ -88,24 +88,24 @@ jobs:
         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@v3
-        with:
-          name: 'Smoke Test Kit ${{matrix.variant}}'
-          path: smoke-test-kit
-          retention-days: 5
+      # - 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@v3
+      #   with:
+      #     name: 'Smoke Test Kit ${{matrix.variant}}'
+      #     path: smoke-test-kit
+      #     retention-days: 5
 
   Ubuntu_snap:
     name: Snap package
@@ -159,38 +159,38 @@ jobs:
   # 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@v3
-        id: download-snap
-        with:
-          name: 'Snap package'
-
-      - name: 'Download smoke test kit'
-        uses: actions/download-artifact@v3
-        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
-          sudo snap alias coq-prover.sertop sertop
-
-      - name: 'Run Smoke Test Kit'
-        run: |
-          cd ${{steps.download-smoke.outputs.download-path}}
-          chmod a+x ./run-smoke-test.sh
-          ./run-smoke-test.sh
+  # 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@v3
+  #       id: download-snap
+  #       with:
+  #         name: 'Snap package'
+
+  #     - name: 'Download smoke test kit'
+  #       uses: actions/download-artifact@v3
+  #       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
+  #         sudo snap alias coq-prover.sertop sertop
+
+  #     - 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/windows.yml b/.github/workflows/windows.yml
index 7dd96b1d72..57e7e6da27 100644
--- a/.github/workflows/windows.yml
+++ b/.github/workflows/windows.yml
@@ -80,9 +80,9 @@ jobs:
         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/"
+      # - 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/"
 
       - name: 'Upload Artifact'
         uses: actions/upload-artifact@v3
@@ -91,57 +91,57 @@ jobs:
           path: C:\installer\*.exe
           retention-days: 5
 
-      - name: 'Upload smoke test kit'
-        uses: actions/upload-artifact@v3
-        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.18~tactician'
-          # - '8.19~2024.01+beta1'
-          # - '8.18~2023.11'
-          # - '8.18~mc2'
-          # - '8.17~2023.08'
-
-    steps:
-      - name: 'Download Artifact'
-        uses: actions/download-artifact@v3
-        id: download
-        with:
-          name: 'Windows installer ${{matrix.variant}} ${{matrix.architecture}}'
-
-      - name: 'Download smoke test kit'
-        uses: actions/download-artifact@v3
-        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
+      # - name: 'Upload smoke test kit'
+      #   uses: actions/upload-artifact@v3
+      #   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.18~tactician'
+  #         # - '8.19~2024.01+beta1'
+  #         # - '8.18~2023.11'
+  #         # - '8.18~mc2'
+  #         # - '8.17~2023.08'
+
+  #   steps:
+  #     - name: 'Download Artifact'
+  #       uses: actions/download-artifact@v3
+  #       id: download
+  #       with:
+  #         name: 'Windows installer ${{matrix.variant}} ${{matrix.architecture}}'
+
+  #     - name: 'Download smoke test kit'
+  #       uses: actions/download-artifact@v3
+  #       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

From a5c274d46b7a87cfa6594bb229ef9ff24a73983f Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 11 Apr 2024 16:22:01 +0200
Subject: [PATCH 15/38] Debug more

---
 shell_scripts/build.sh | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/shell_scripts/build.sh b/shell_scripts/build.sh
index e285e7b199..4a3d8f1c67 100644
--- a/shell_scripts/build.sh
+++ b/shell_scripts/build.sh
@@ -34,7 +34,11 @@ 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
 
-if ! $COQ_PLATFORM_TIME opam install --ignore-constraints-on="coq-tactician,dune,coq-core" dune.3.15.0 coq-tactician-dummy.1.0~beta2+8.17 coq-core.8.18.0 coq-tactician.1.0~beta2.1+8.18; then dump_opam_logs; fi
+if ! $COQ_PLATFORM_TIME opam pin dune 3.15.0; then dump_opam_logs; fi
+if ! $COQ_PLATFORM_TIME opam pin coq-tactician-dummy 1.0~beta2+8.17; then dump_opam_logs; fi
+if ! $COQ_PLATFORM_TIME opam pin coq-tactician 1.0~beta2.1+8.18; then dump_opam_logs; fi
+if ! $COQ_PLATFORM_TIME opam pin coq-core 8.18.0; then dump_opam_logs; fi
+if ! $COQ_PLATFORM_TIME opam install dune.3.15.0 coq-core.8.18.0 coq-tactician-dummy.1.0~beta2+8.17 coq-tactician.1.0~beta2.1+8.18; then dump_opam_logs; fi
 
 opam switch
 opam switch set ${COQ_PLATFORM_SWITCH_NAME}

From 7d00da258f883b8600d5cfa5bf7b8464ea32236b Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 11 Apr 2024 16:35:02 +0200
Subject: [PATCH 16/38] Debug

---
 shell_scripts/build.sh | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/shell_scripts/build.sh b/shell_scripts/build.sh
index 4a3d8f1c67..f866e202c8 100644
--- a/shell_scripts/build.sh
+++ b/shell_scripts/build.sh
@@ -34,10 +34,10 @@ 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
 
-if ! $COQ_PLATFORM_TIME opam pin dune 3.15.0; then dump_opam_logs; fi
-if ! $COQ_PLATFORM_TIME opam pin coq-tactician-dummy 1.0~beta2+8.17; then dump_opam_logs; fi
-if ! $COQ_PLATFORM_TIME opam pin coq-tactician 1.0~beta2.1+8.18; then dump_opam_logs; fi
-if ! $COQ_PLATFORM_TIME opam pin coq-core 8.18.0; then dump_opam_logs; fi
+if ! $COQ_PLATFORM_TIME opam pin -n dune 3.15.0; then dump_opam_logs; fi
+if ! $COQ_PLATFORM_TIME opam pin -n coq-tactician-dummy 1.0~beta2+8.17; then dump_opam_logs; fi
+if ! $COQ_PLATFORM_TIME opam pin -n coq-tactician 1.0~beta2.1+8.18; then dump_opam_logs; fi
+if ! $COQ_PLATFORM_TIME opam pin -n coq-core 8.18.0; then dump_opam_logs; fi
 if ! $COQ_PLATFORM_TIME opam install dune.3.15.0 coq-core.8.18.0 coq-tactician-dummy.1.0~beta2+8.17 coq-tactician.1.0~beta2.1+8.18; then dump_opam_logs; fi
 
 opam switch

From ed8da65054f0883135dddb81026d075543c27941 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 11 Apr 2024 16:50:58 +0200
Subject: [PATCH 17/38] Debug x

---
 shell_scripts/build.sh | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/shell_scripts/build.sh b/shell_scripts/build.sh
index f866e202c8..c046f331dc 100644
--- a/shell_scripts/build.sh
+++ b/shell_scripts/build.sh
@@ -38,7 +38,8 @@ if ! $COQ_PLATFORM_TIME opam pin -n dune 3.15.0; then dump_opam_logs; fi
 if ! $COQ_PLATFORM_TIME opam pin -n coq-tactician-dummy 1.0~beta2+8.17; then dump_opam_logs; fi
 if ! $COQ_PLATFORM_TIME opam pin -n coq-tactician 1.0~beta2.1+8.18; then dump_opam_logs; fi
 if ! $COQ_PLATFORM_TIME opam pin -n coq-core 8.18.0; then dump_opam_logs; fi
-if ! $COQ_PLATFORM_TIME opam install dune.3.15.0 coq-core.8.18.0 coq-tactician-dummy.1.0~beta2+8.17 coq-tactician.1.0~beta2.1+8.18; then dump_opam_logs; fi
+if ! $COQ_PLATFORM_TIME opam pin -n ocamlfind 1.9.5~relocatable; then dump_opam_logs; fi
+if ! $COQ_PLATFORM_TIME opam install dune.3.15.0 coq-core.8.18.0 coq-tactician-dummy.1.0~beta2+8.17 coq-tactician.1.0~beta2.1+8.18 ocamlfind.1.9.5~relocatable; then dump_opam_logs; fi
 
 opam switch
 opam switch set ${COQ_PLATFORM_SWITCH_NAME}

From 778d71232bea6790cb45c0e499ea00ce6464e6cc Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 11 Apr 2024 17:13:06 +0200
Subject: [PATCH 18/38] Full pick

---
 .github/workflows/macos.yml                | 2 +-
 .github/workflows/ubuntu.yml               | 6 +++---
 .github/workflows/windows.yml              | 2 +-
 package_picks/package-pick-8.18~2023.11.sh | 4 ++--
 4 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/macos.yml b/.github/workflows/macos.yml
index 37b89816a0..cdd9fd215d 100644
--- a/.github/workflows/macos.yml
+++ b/.github/workflows/macos.yml
@@ -54,7 +54,7 @@ jobs:
           # Keep this in sync with the Smoke test below
           - '8.18~tactician'
           # - '8.19~2024.01+beta1'
-          # - '8.18~2023.11'
+          - '8.18~2023.11'
           # - '8.18~mc2'
           # - '8.17~2023.08'
     steps:
diff --git a/.github/workflows/ubuntu.yml b/.github/workflows/ubuntu.yml
index 6f0a9318c9..198c3e08e8 100644
--- a/.github/workflows/ubuntu.yml
+++ b/.github/workflows/ubuntu.yml
@@ -29,7 +29,7 @@ on:
         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.18~tactician
+        default: 8.18~2023.11
       upload:
         description: 'Upload artifact to Snap Store? (true/false, default false)'
         default: false
@@ -40,7 +40,7 @@ on:
 env:
   PLATFORM: -extent=x -parallel=p -jobs=2 -large=i -compcert=y -unimath=n -set-switch=y
   COQREGTESTING: y
-  SNAP_PICK: 8.18~tactician
+  SNAP_PICK: 8.18~2023.11
 
 
 ###############################################################################
@@ -61,7 +61,7 @@ jobs:
           # This should contain all picks introduced in the current release + all original picks of all Coq versions
           - '8.18~tactician'
           # - '8.19~2024.01+beta1'
-          # - '8.18~2023.11'
+          - '8.18~2023.11'
           # - '8.18~mc2'
           # - '8.17~2023.08'
           # - '8.16~2022.09'
diff --git a/.github/workflows/windows.yml b/.github/workflows/windows.yml
index 57e7e6da27..64adf56337 100644
--- a/.github/workflows/windows.yml
+++ b/.github/workflows/windows.yml
@@ -55,7 +55,7 @@ jobs:
           # Keep this in sync with the Smoke test below
           - '8.18~tactician'
           # - '8.19~2024.01+beta1'
-          # - '8.18~2023.11'
+          - '8.18~2023.11'
           # - '8.18~mc2'
           # - '8.17~2023.08'
 
diff --git a/package_picks/package-pick-8.18~2023.11.sh b/package_picks/package-pick-8.18~2023.11.sh
index 8966f8c57f..cef7cc66be 100644
--- a/package_picks/package-pick-8.18~2023.11.sh
+++ b/package_picks/package-pick-8.18~2023.11.sh
@@ -50,8 +50,8 @@ 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"
+PACKAGES="${PACKAGES} dune.3.15.0"
+PACKAGES="${PACKAGES} dune-configurator.3.15.0"
 # The Coq compiler coqc and the Coq standard library
 PACKAGES="${PACKAGES} PIN.coq.8.18.0"
 

From ee3291be823e0371765c11e74fe34835a8c01742 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 11 Apr 2024 17:29:11 +0200
Subject: [PATCH 19/38] Pre-install z3

---
 shell_scripts/build.sh | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/shell_scripts/build.sh b/shell_scripts/build.sh
index c046f331dc..9a5956d34f 100644
--- a/shell_scripts/build.sh
+++ b/shell_scripts/build.sh
@@ -39,7 +39,8 @@ if ! $COQ_PLATFORM_TIME opam pin -n coq-tactician-dummy 1.0~beta2+8.17; then dum
 if ! $COQ_PLATFORM_TIME opam pin -n coq-tactician 1.0~beta2.1+8.18; then dump_opam_logs; fi
 if ! $COQ_PLATFORM_TIME opam pin -n coq-core 8.18.0; then dump_opam_logs; fi
 if ! $COQ_PLATFORM_TIME opam pin -n ocamlfind 1.9.5~relocatable; then dump_opam_logs; fi
-if ! $COQ_PLATFORM_TIME opam install dune.3.15.0 coq-core.8.18.0 coq-tactician-dummy.1.0~beta2+8.17 coq-tactician.1.0~beta2.1+8.18 ocamlfind.1.9.5~relocatable; then dump_opam_logs; fi
+if ! $COQ_PLATFORM_TIME opam pin -n z3 4.11.2; then dump_opam_logs; fi # Installing z3 later will cause Tactician to be recompiled
+if ! $COQ_PLATFORM_TIME opam install dune coq-core coq-tactician-dummy coq-tactician ocamlfind z3; then dump_opam_logs; fi
 
 opam switch
 opam switch set ${COQ_PLATFORM_SWITCH_NAME}

From 250ac408adf4390d321403d4ee374effe2fac3cf Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 11 Apr 2024 18:43:32 +0200
Subject: [PATCH 20/38] Don't install z3 in cygwin

---
 shell_scripts/build.sh | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/shell_scripts/build.sh b/shell_scripts/build.sh
index 9a5956d34f..8e9a6b7188 100644
--- a/shell_scripts/build.sh
+++ b/shell_scripts/build.sh
@@ -39,8 +39,13 @@ if ! $COQ_PLATFORM_TIME opam pin -n coq-tactician-dummy 1.0~beta2+8.17; then dum
 if ! $COQ_PLATFORM_TIME opam pin -n coq-tactician 1.0~beta2.1+8.18; then dump_opam_logs; fi
 if ! $COQ_PLATFORM_TIME opam pin -n coq-core 8.18.0; then dump_opam_logs; fi
 if ! $COQ_PLATFORM_TIME opam pin -n ocamlfind 1.9.5~relocatable; then dump_opam_logs; fi
-if ! $COQ_PLATFORM_TIME opam pin -n z3 4.11.2; then dump_opam_logs; fi # Installing z3 later will cause Tactician to be recompiled
-if ! $COQ_PLATFORM_TIME opam install dune coq-core coq-tactician-dummy coq-tactician ocamlfind z3; then dump_opam_logs; fi
+if ! $COQ_PLATFORM_TIME opam install dune coq-core coq-tactician-dummy coq-tactician ocamlfind; then dump_opam_logs; fi
+
+if [[ "$OSTYPE" != cygwin ]]
+then
+    if ! $COQ_PLATFORM_TIME opam pin -n z3 4.11.2; then dump_opam_logs; fi # Installing z3 later will cause Tactician to be recompiled
+    if ! $COQ_PLATFORM_TIME opam install z3; then dump_opam_logs; fi
+  fi
 
 opam switch
 opam switch set ${COQ_PLATFORM_SWITCH_NAME}

From e0ad3325cbf250ec2984eb9fc468fe966109aaca Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 11 Apr 2024 20:34:17 +0200
Subject: [PATCH 21/38] Dev version

---
 package_picks/package-pick-8.18~mc2.sh | 2 +-
 shell_scripts/build.sh                 | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/package_picks/package-pick-8.18~mc2.sh b/package_picks/package-pick-8.18~mc2.sh
index 9bdf9cbd85..55843d2e54 100644
--- a/package_picks/package-pick-8.18~mc2.sh
+++ b/package_picks/package-pick-8.18~mc2.sh
@@ -25,7 +25,7 @@ COQ_PLATFORM_COQ_BRANCH='v8.18'
 COQ_PLATFORM_COQ_TAG='8.18.0'
 
 # This controls if opam repositories for development packages are selected
-COQ_PLATFORM_USE_DEV_REPOSITORY='N'
+COQ_PLATFORM_USE_DEV_REPOSITORY='Y'
 
 # This extended descriptions is used for readme files
 COQ_PLATFORM_VERSION_DESCRIPTION='This version of Coq Platform 2023.11.0 includes Coq 8.18.0 from Sep 2023. '
diff --git a/shell_scripts/build.sh b/shell_scripts/build.sh
index 8e9a6b7188..8431402c3c 100644
--- a/shell_scripts/build.sh
+++ b/shell_scripts/build.sh
@@ -35,8 +35,8 @@ opam config set jobs $COQ_PLATFORM_JOBS
 ulimit -S -s 65520
 
 if ! $COQ_PLATFORM_TIME opam pin -n dune 3.15.0; then dump_opam_logs; fi
-if ! $COQ_PLATFORM_TIME opam pin -n coq-tactician-dummy 1.0~beta2+8.17; then dump_opam_logs; fi
-if ! $COQ_PLATFORM_TIME opam pin -n coq-tactician 1.0~beta2.1+8.18; then dump_opam_logs; fi
+if ! $COQ_PLATFORM_TIME opam pin -n coq-tactician-dummy 8.17.dev; then dump_opam_logs; fi
+if ! $COQ_PLATFORM_TIME opam pin -n coq-tactician 8.18.dev; then dump_opam_logs; fi
 if ! $COQ_PLATFORM_TIME opam pin -n coq-core 8.18.0; then dump_opam_logs; fi
 if ! $COQ_PLATFORM_TIME opam pin -n ocamlfind 1.9.5~relocatable; then dump_opam_logs; fi
 if ! $COQ_PLATFORM_TIME opam install dune coq-core coq-tactician-dummy coq-tactician ocamlfind; then dump_opam_logs; fi

From 0354734260c59be9de6332801fd816f572be4c7d Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 11 Apr 2024 20:44:26 +0200
Subject: [PATCH 22/38] Fix

---
 package_picks/package-pick-8.18~2023.11.sh | 2 +-
 package_picks/package-pick-8.18~mc2.sh     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/package_picks/package-pick-8.18~2023.11.sh b/package_picks/package-pick-8.18~2023.11.sh
index cef7cc66be..3a4ed95276 100644
--- a/package_picks/package-pick-8.18~2023.11.sh
+++ b/package_picks/package-pick-8.18~2023.11.sh
@@ -25,7 +25,7 @@ COQ_PLATFORM_COQ_BRANCH='v8.18'
 COQ_PLATFORM_COQ_TAG='8.18.0'
 
 # This controls if opam repositories for development packages are selected
-COQ_PLATFORM_USE_DEV_REPOSITORY='N'
+COQ_PLATFORM_USE_DEV_REPOSITORY='Y'
 
 # This extended descriptions is used for readme files
 COQ_PLATFORM_VERSION_DESCRIPTION='This version of Coq Platform 2023.11.0 includes Coq 8.18.0 from Sep 2023. '
diff --git a/package_picks/package-pick-8.18~mc2.sh b/package_picks/package-pick-8.18~mc2.sh
index 55843d2e54..9bdf9cbd85 100644
--- a/package_picks/package-pick-8.18~mc2.sh
+++ b/package_picks/package-pick-8.18~mc2.sh
@@ -25,7 +25,7 @@ COQ_PLATFORM_COQ_BRANCH='v8.18'
 COQ_PLATFORM_COQ_TAG='8.18.0'
 
 # This controls if opam repositories for development packages are selected
-COQ_PLATFORM_USE_DEV_REPOSITORY='Y'
+COQ_PLATFORM_USE_DEV_REPOSITORY='N'
 
 # This extended descriptions is used for readme files
 COQ_PLATFORM_VERSION_DESCRIPTION='This version of Coq Platform 2023.11.0 includes Coq 8.18.0 from Sep 2023. '

From 76dfd113660f76150012a3beeda351d3eab0e475 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 11 Apr 2024 21:39:36 +0200
Subject: [PATCH 23/38] Install z3 first

---
 shell_scripts/build.sh | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/shell_scripts/build.sh b/shell_scripts/build.sh
index 8431402c3c..da0deed0ff 100644
--- a/shell_scripts/build.sh
+++ b/shell_scripts/build.sh
@@ -34,6 +34,12 @@ 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
 
+if [[ "$OSTYPE" != cygwin ]]
+then
+    if ! $COQ_PLATFORM_TIME opam pin -n z3 4.11.2; then dump_opam_logs; fi # Installing z3 later will cause Tactician to be recompiled
+    if ! $COQ_PLATFORM_TIME opam install z3; then dump_opam_logs; fi
+fi
+
 if ! $COQ_PLATFORM_TIME opam pin -n dune 3.15.0; then dump_opam_logs; fi
 if ! $COQ_PLATFORM_TIME opam pin -n coq-tactician-dummy 8.17.dev; then dump_opam_logs; fi
 if ! $COQ_PLATFORM_TIME opam pin -n coq-tactician 8.18.dev; then dump_opam_logs; fi
@@ -41,12 +47,6 @@ if ! $COQ_PLATFORM_TIME opam pin -n coq-core 8.18.0; then dump_opam_logs; fi
 if ! $COQ_PLATFORM_TIME opam pin -n ocamlfind 1.9.5~relocatable; then dump_opam_logs; fi
 if ! $COQ_PLATFORM_TIME opam install dune coq-core coq-tactician-dummy coq-tactician ocamlfind; then dump_opam_logs; fi
 
-if [[ "$OSTYPE" != cygwin ]]
-then
-    if ! $COQ_PLATFORM_TIME opam pin -n z3 4.11.2; then dump_opam_logs; fi # Installing z3 later will cause Tactician to be recompiled
-    if ! $COQ_PLATFORM_TIME opam install z3; then dump_opam_logs; fi
-  fi
-
 opam switch
 opam switch set ${COQ_PLATFORM_SWITCH_NAME}
 opam switch

From 750a2b9232c5495d33278b636cb765298a450b15 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 18 Jul 2024 14:25:51 +0200
Subject: [PATCH 24/38] Run CI

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index f21496d339..56d519bb42 100644
--- a/README.md
+++ b/README.md
@@ -1,4 +1,4 @@
-# ATTENTION RELEASE IN PROGRESS
+# ATTENTION RELEASE IN PROGRESS 
 
 **We are currently preparing a release, which has the effect that some links already refer to the new tag, even though this does not exist as yet.**
 

From 9120673bb5e93911c6ec11ba06d06fb033017e86 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 18 Jul 2024 14:31:09 +0200
Subject: [PATCH 25/38] Run CI

---
 README.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/README.md b/README.md
index 56d519bb42..4db2e119be 100644
--- a/README.md
+++ b/README.md
@@ -1,5 +1,7 @@
 # ATTENTION RELEASE IN PROGRESS 
 
+bla
+
 **We are currently preparing a release, which has the effect that some links already refer to the new tag, even though this does not exist as yet.**
 
 **In case you experience dead links, please replace `2023.11.0` with `2023.03.0`.**

From 0e587d39cabce9bf4ea648255352388d743a93ee Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 18 Jul 2024 15:33:45 +0200
Subject: [PATCH 26/38] Do ocamlfind pin earlier

---
 shell_scripts/build.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/shell_scripts/build.sh b/shell_scripts/build.sh
index da0deed0ff..87c086930d 100644
--- a/shell_scripts/build.sh
+++ b/shell_scripts/build.sh
@@ -34,6 +34,7 @@ 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
 
+if ! $COQ_PLATFORM_TIME opam pin -n ocamlfind 1.9.5~relocatable; then dump_opam_logs; fi
 if [[ "$OSTYPE" != cygwin ]]
 then
     if ! $COQ_PLATFORM_TIME opam pin -n z3 4.11.2; then dump_opam_logs; fi # Installing z3 later will cause Tactician to be recompiled
@@ -44,7 +45,6 @@ if ! $COQ_PLATFORM_TIME opam pin -n dune 3.15.0; then dump_opam_logs; fi
 if ! $COQ_PLATFORM_TIME opam pin -n coq-tactician-dummy 8.17.dev; then dump_opam_logs; fi
 if ! $COQ_PLATFORM_TIME opam pin -n coq-tactician 8.18.dev; then dump_opam_logs; fi
 if ! $COQ_PLATFORM_TIME opam pin -n coq-core 8.18.0; then dump_opam_logs; fi
-if ! $COQ_PLATFORM_TIME opam pin -n ocamlfind 1.9.5~relocatable; then dump_opam_logs; fi
 if ! $COQ_PLATFORM_TIME opam install dune coq-core coq-tactician-dummy coq-tactician ocamlfind; then dump_opam_logs; fi
 
 opam switch

From fd4810fac98af37bad1ee848a7b6ab1ae384dfdb Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 18 Jul 2024 15:44:07 +0200
Subject: [PATCH 27/38] Fix

---
 shell_scripts/build.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/shell_scripts/build.sh b/shell_scripts/build.sh
index 87c086930d..cbe76dc205 100644
--- a/shell_scripts/build.sh
+++ b/shell_scripts/build.sh
@@ -41,7 +41,7 @@ then
     if ! $COQ_PLATFORM_TIME opam install z3; then dump_opam_logs; fi
 fi
 
-if ! $COQ_PLATFORM_TIME opam pin -n dune 3.15.0; then dump_opam_logs; fi
+if ! $COQ_PLATFORM_TIME opam pin -n dune 3.15.3; then dump_opam_logs; fi
 if ! $COQ_PLATFORM_TIME opam pin -n coq-tactician-dummy 8.17.dev; then dump_opam_logs; fi
 if ! $COQ_PLATFORM_TIME opam pin -n coq-tactician 8.18.dev; then dump_opam_logs; fi
 if ! $COQ_PLATFORM_TIME opam pin -n coq-core 8.18.0; then dump_opam_logs; fi

From 11eb265fb45ffdf41833f636ebf66c617fb899dd Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 18 Jul 2024 16:12:38 +0200
Subject: [PATCH 28/38] Downgrade opam-client for windows

---
 shell_scripts/build.sh | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/shell_scripts/build.sh b/shell_scripts/build.sh
index cbe76dc205..052a5f6216 100644
--- a/shell_scripts/build.sh
+++ b/shell_scripts/build.sh
@@ -35,6 +35,12 @@ opam config set jobs $COQ_PLATFORM_JOBS
 ulimit -S -s 65520
 
 if ! $COQ_PLATFORM_TIME opam pin -n ocamlfind 1.9.5~relocatable; then dump_opam_logs; fi
+
+if [[ "$OSTYPE" == cygwin ]]
+then
+    if ! $COQ_PLATFORM_TIME opam pin -n opam-client 2.1.0; then dump_opam_logs; fi
+fi
+
 if [[ "$OSTYPE" != cygwin ]]
 then
     if ! $COQ_PLATFORM_TIME opam pin -n z3 4.11.2; then dump_opam_logs; fi # Installing z3 later will cause Tactician to be recompiled

From 35f3e047bfd3e27dbfb7cd5e58b5d61d3a00ab89 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 18 Jul 2024 16:51:11 +0200
Subject: [PATCH 29/38] Note

---
 shell_scripts/build.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/shell_scripts/build.sh b/shell_scripts/build.sh
index 052a5f6216..01df32f420 100644
--- a/shell_scripts/build.sh
+++ b/shell_scripts/build.sh
@@ -38,7 +38,7 @@ if ! $COQ_PLATFORM_TIME opam pin -n ocamlfind 1.9.5~relocatable; then dump_opam_
 
 if [[ "$OSTYPE" == cygwin ]]
 then
-    if ! $COQ_PLATFORM_TIME opam pin -n opam-client 2.1.0; then dump_opam_logs; fi
+    if ! $COQ_PLATFORM_TIME opam pin -n opam-client 2.1.0; then dump_opam_logs; fi # opam-clinet 2.2.0 doesn't want to compile on Windows
 fi
 
 if [[ "$OSTYPE" != cygwin ]]

From 839b5dfeb31423f3b4fa9241287c3c7aebc82617 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Fri, 19 Jul 2024 01:06:42 +0200
Subject: [PATCH 30/38] CI

---
 README.md | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/README.md b/README.md
index 4db2e119be..f21496d339 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,4 @@
-# ATTENTION RELEASE IN PROGRESS 
-
-bla
+# ATTENTION RELEASE IN PROGRESS
 
 **We are currently preparing a release, which has the effect that some links already refer to the new tag, even though this does not exist as yet.**
 

From c56440dc310f7e4ebbe3556291d508dbdd3b0ac5 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Fri, 19 Jul 2024 04:00:25 +0200
Subject: [PATCH 31/38] Cleanup

---
 .github/workflows/macos.yml                  | 132 +++++++++----------
 .github/workflows/ubuntu.yml                 | 107 ++++++++-------
 .github/workflows/windows.yml                | 111 ++++++++--------
 package_picks/package-pick-8.18~tactician.sh |  56 --------
 4 files changed, 173 insertions(+), 233 deletions(-)
 delete mode 100644 package_picks/package-pick-8.18~tactician.sh

diff --git a/.github/workflows/macos.yml b/.github/workflows/macos.yml
index d7401dd3e7..fd324bc771 100644
--- a/.github/workflows/macos.yml
+++ b/.github/workflows/macos.yml
@@ -52,7 +52,6 @@ jobs:
       matrix:
         variant:
           # Keep this in sync with the Smoke test below
-          - '8.18~tactician'
           # - '8.19~2024.01+beta1'
           - '8.18~2023.11'
           # - '8.18~mc2'
@@ -120,19 +119,19 @@ jobs:
       - 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: 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: '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: |
@@ -163,57 +162,56 @@ jobs:
           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.18~tactician'
-  #         # - '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
+  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
index 88c12efef3..395599052b 100644
--- a/.github/workflows/ubuntu.yml
+++ b/.github/workflows/ubuntu.yml
@@ -59,7 +59,6 @@ jobs:
       matrix:
         variant:
           # This should contain all picks introduced in the current release + all original picks of all Coq versions
-          - '8.18~tactician'
           # - '8.19~2024.01+beta1'
           - '8.18~2023.11'
           # - '8.18~mc2'
@@ -88,24 +87,24 @@ jobs:
         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
+      - 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
 
   Ubuntu_snap:
     name: Snap package
@@ -159,38 +158,38 @@ jobs:
   # 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@v4
-      #   id: download-snap
-      #   with:
-      #     name: 'Snap package'
-
-      # - name: 'Download smoke test kit'
-      #   uses: actions/download-artifact@v4
-      #   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
-  #         sudo snap alias coq-prover.sertop sertop
-
-  #     - name: 'Run Smoke Test Kit'
-  #       run: |
-  #         cd ${{steps.download-smoke.outputs.download-path}}
-  #         chmod a+x ./run-smoke-test.sh
-  #         ./run-smoke-test.sh
+  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@v4
+        id: download-snap
+        with:
+          name: 'Snap package'
+
+      - name: 'Download smoke test kit'
+        uses: actions/download-artifact@v4
+        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
+          sudo snap alias coq-prover.sertop sertop
+
+      - 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/windows.yml b/.github/workflows/windows.yml
index 2c4ab22546..456906620b 100644
--- a/.github/workflows/windows.yml
+++ b/.github/workflows/windows.yml
@@ -52,7 +52,6 @@ jobs:
           - '64'
         variant:
           # Keep this in sync with the Smoke test below
-          - '8.18~tactician'
           # - '8.19~2024.01+beta1'
           - '8.18~2023.11'
           # - '8.18~mc2'
@@ -79,9 +78,9 @@ jobs:
         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/"
+      - 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/"
 
       - name: 'Upload Artifact'
         uses: actions/upload-artifact@v4
@@ -90,55 +89,55 @@ jobs:
           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
+      - 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.18~tactician.sh b/package_picks/package-pick-8.18~tactician.sh
deleted file mode 100644
index 5b4d969fb9..0000000000
--- a/package_picks/package-pick-8.18~tactician.sh
+++ /dev/null
@@ -1,56 +0,0 @@
-#!/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.18.0 (released Sep 2023) with Tactician"
-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.18~tactician'
-
-# The corresponding Coq development branch and tag
-COQ_PLATFORM_COQ_BRANCH='v8.18'
-COQ_PLATFORM_COQ_TAG='8.18.0'
-
-# 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 Coq Platform 2023.11.0 includes Coq 8.18.0 from Sep 2023 and Tactician.'
-
-# 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"  # TODO port patch to 1.9.6
-# The Coq compiler coqc and the Coq standard library
-PACKAGES="${PACKAGES} PIN.coq.8.18.0"
-
-########## IDE PACKAGES ##########
-
-PACKAGES="${PACKAGES} coqide.8.18.0"

From 3bdeb303004c93414ffecb7cc432e6db68b4fb16 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Wed, 24 Jul 2024 12:39:26 +0200
Subject: [PATCH 32/38] CI


From 9e0190cc66a9819e058fac1553054193da4f9656 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Wed, 24 Jul 2024 21:28:36 +0200
Subject: [PATCH 33/38] CI


From 57d14e747ee854c6ed6884e24ca8532b8b46f06b Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 25 Jul 2024 08:24:11 +0200
Subject: [PATCH 34/38] CI


From 5abba6efaa4bd1510147403de81b220801e74404 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 25 Jul 2024 17:19:48 +0200
Subject: [PATCH 35/38] CI


From daa9ee6c87ad9f5784bc26a42ca89d4a90678eab Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 25 Jul 2024 22:15:14 +0200
Subject: [PATCH 36/38] CI


From 941efe2ca1d572f6fafb41af4561b0cc4c8b07eb Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 25 Jul 2024 22:36:25 +0200
Subject: [PATCH 37/38] CI


From 0b70d9beae6f00d977d17d5c48a7515de216dc31 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek <lasse@blaauwbroek.eu>
Date: Thu, 25 Jul 2024 23:06:04 +0200
Subject: [PATCH 38/38] CI