Add Tactician to the platform

.github/workflows/macos.yml

@@ -15,6 +15,7 @@ on:
       - 2021.02
       - 2021.09
       - main
+      - tactician
   pull_request:
     branches:
       - '**'
@@ -51,10 +52,10 @@ jobs:
       matrix:
         variant:
           # Keep this in sync with the Smoke test below
-          - '8.19~2024.01+beta1'
+          # - '8.19~2024.01+beta1'
           - '8.18~2023.11'
-          - '8.18~mc2'
-          - '8.17~2023.08'
+          # - '8.18~mc2'
+          # - '8.17~2023.08'
     steps:
       - name: Git checkout
         uses: actions/checkout@v4
@@ -169,10 +170,10 @@ jobs:
       fail-fast: false
       matrix:
         variant:
-          - '8.19~2024.01+beta1'
+          # - '8.19~2024.01+beta1'
           - '8.18~2023.11'
-          - '8.18~mc2'
-          - '8.17~2023.08'
+          # - '8.18~mc2'
+          # - '8.17~2023.08'
 
     steps:
       - name: Install bash

.github/workflows/ubuntu.yml

@@ -15,6 +15,7 @@ on:
       - 2021.02
       - 2021.09
       - main
+      - tactician
   pull_request:
     branches:
       - '**'
@@ -58,16 +59,16 @@ 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.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~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

.github/workflows/windows.yml

@@ -13,6 +13,7 @@ on:
   push:
     branches:
       - main
+      - tactician
   pull_request:
     branches:
       - '**'
@@ -51,10 +52,10 @@ jobs:
           - '64'
         variant:
           # Keep this in sync with the Smoke test below
-          - '8.19~2024.01+beta1'
+          # - '8.19~2024.01+beta1'
           - '8.18~2023.11'
-          - '8.18~mc2'
-          - '8.17~2023.08'
+          # - '8.18~mc2'
+          # - '8.17~2023.08'
 
     steps:
       - name: Set git to use LF

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. '

shell_scripts/build.sh

@@ -34,11 +34,38 @@ 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 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 ]]
+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.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
+if ! $COQ_PLATFORM_TIME opam install dune coq-core coq-tactician-dummy coq-tactician ocamlfind; then dump_opam_logs; fi
+
+opam switch
+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
+
 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.*)