From af836d157744e105cab52e4fa126d95f5abe0124 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Mon, 16 Jan 2023 10:25:45 +0100
Subject: [PATCH 01/22] add ci

---
 .github/workflows/main.yml | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 .github/workflows/main.yml

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
new file mode 100644
index 00000000..e9a64f51
--- /dev/null
+++ b/.github/workflows/main.yml
@@ -0,0 +1,29 @@
+on:
+  pull_request:
+    types: [opened, synchronize, edited, reopened]
+  push:
+  workflow_dispatch:
+jobs:
+  build:
+    strategy:
+      fail-fast: false
+      matrix:
+        ocaml-version: [4.02.3] #3.07+2, 3.08.4, 3.09.3, 3.10.2, 3.11.2, 3.12.1, 4.00.1, 4.01.0, 4.02.3, 4.03.0, 4.04.2, 4.05.0, 4.06.1, 4.07.1, 4.08.1, 4.09.1, 4.10.2, 4.11.2, 4.12.1, 4.13.1, 4.14.1]
+        camlp5-version: [6.17] #6.04  6.06  6.07  6.11  6.12  6.13  6.14  6.15  6.16 6.17  7.00  7.01  7.03  7.05  7.06  7.06.10-g84ce6cc4 7.08  7.09  7.10  7.11  7.12  7.13  7.14  8.00~alpha01 8.00~alpha02  8.00~alpha03  8.00~alpha04  8.00~alpha05 8.00~alpha06  8.00  8.00.01  8.00.02  8.00.03  8.00.04]
+    runs-on: ubuntu-latest
+    steps:
+      - name: check out hol-light repo ...
+        uses: actions/checkout@v2
+      - name: recovering cached opam files ...
+        uses: actions/cache@v2
+        with:
+          path: ~/.opam
+          key: ${{ runner.os }}-ocaml-${{ matrix.ocaml-version }}
+      - name: setting up opam ...
+        uses: avsm/setup-ocaml@v1
+        with:
+          ocaml-version: ${{ matrix.ocaml-version }}
+      - name: install camlp5 ...
+        run: opam install camlp5.${{ matrix.camlp5-version }}
+      - name: run tests ...
+        run: echo "#use hol.ml" | ocaml -I `camlp5 -where` camlp5o.cma'

From 55a37037bf0fd0deb18042d1d1434cc263144eb5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Mon, 16 Jan 2023 10:31:31 +0100
Subject: [PATCH 02/22] ci: install num and ocamlfind

---
 .github/workflows/main.yml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index e9a64f51..b047cb38 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -23,6 +23,10 @@ jobs:
         uses: avsm/setup-ocaml@v1
         with:
           ocaml-version: ${{ matrix.ocaml-version }}
+      - name: install num ...
+        run: opam install num
+      - name: install ocamlfind ...
+        run: opam install ocamlfind
       - name: install camlp5 ...
         run: opam install camlp5.${{ matrix.camlp5-version }}
       - name: run tests ...

From c7b7d975bbd7ccc03772ba973aec8f2a51cf8917 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Mon, 16 Jan 2023 10:40:42 +0100
Subject: [PATCH 03/22] fix ci script

---
 .github/workflows/main.yml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index b047cb38..f35d1705 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -19,7 +19,7 @@ jobs:
         with:
           path: ~/.opam
           key: ${{ runner.os }}-ocaml-${{ matrix.ocaml-version }}
-      - name: setting up opam ...
+      - name: set up opam ...
         uses: avsm/setup-ocaml@v1
         with:
           ocaml-version: ${{ matrix.ocaml-version }}
@@ -29,5 +29,7 @@ jobs:
         run: opam install ocamlfind
       - name: install camlp5 ...
         run: opam install camlp5.${{ matrix.camlp5-version }}
-      - name: run tests ...
-        run: echo "#use hol.ml" | ocaml -I `camlp5 -where` camlp5o.cma'
+      - name: setup hol-light ...
+        run: make
+      - name: run test ...
+        run: echo "#use \"hol.ml\";;" | ocaml -I `camlp5 -where` camlp5o.cma

From 7f20ba090a78b3548d82d1da2e293ae7af160ebc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Mon, 16 Jan 2023 10:47:12 +0100
Subject: [PATCH 04/22] fix ci script

---
 .github/workflows/main.yml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index f35d1705..07a3df78 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -12,9 +12,9 @@ jobs:
         camlp5-version: [6.17] #6.04  6.06  6.07  6.11  6.12  6.13  6.14  6.15  6.16 6.17  7.00  7.01  7.03  7.05  7.06  7.06.10-g84ce6cc4 7.08  7.09  7.10  7.11  7.12  7.13  7.14  8.00~alpha01 8.00~alpha02  8.00~alpha03  8.00~alpha04  8.00~alpha05 8.00~alpha06  8.00  8.00.01  8.00.02  8.00.03  8.00.04]
     runs-on: ubuntu-latest
     steps:
-      - name: check out hol-light repo ...
+      - name: check out hol-light ...
         uses: actions/checkout@v2
-      - name: recovering cached opam files ...
+      - name: set up cache ...
         uses: actions/cache@v2
         with:
           path: ~/.opam
@@ -30,6 +30,8 @@ jobs:
       - name: install camlp5 ...
         run: opam install camlp5.${{ matrix.camlp5-version }}
       - name: setup hol-light ...
-        run: make
+        run: |
+          eval $(opam env)
+          make
       - name: run test ...
         run: echo "#use \"hol.ml\";;" | ocaml -I `camlp5 -where` camlp5o.cma

From 47461ab9ead90f4bb34e7da29304068fa685362e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Mon, 16 Jan 2023 10:54:54 +0100
Subject: [PATCH 05/22] fix ci script

---
 .github/workflows/main.yml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 07a3df78..33635760 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -34,4 +34,6 @@ jobs:
           eval $(opam env)
           make
       - name: run test ...
-        run: echo "#use \"hol.ml\";;" | ocaml -I `camlp5 -where` camlp5o.cma
+        run: |
+          eval $(opam env)
+          echo "#use \"hol.ml\";;" | ocaml -I `camlp5 -where` camlp5o.cma

From fd9d68d2f5ae1935fd7507c6c5547b47f337cf49 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Mon, 16 Jan 2023 11:30:31 +0100
Subject: [PATCH 06/22] test all versions of ocaml and camlp5

---
 .github/workflows/main.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 33635760..3bc59cf1 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -8,8 +8,8 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        ocaml-version: [4.02.3] #3.07+2, 3.08.4, 3.09.3, 3.10.2, 3.11.2, 3.12.1, 4.00.1, 4.01.0, 4.02.3, 4.03.0, 4.04.2, 4.05.0, 4.06.1, 4.07.1, 4.08.1, 4.09.1, 4.10.2, 4.11.2, 4.12.1, 4.13.1, 4.14.1]
-        camlp5-version: [6.17] #6.04  6.06  6.07  6.11  6.12  6.13  6.14  6.15  6.16 6.17  7.00  7.01  7.03  7.05  7.06  7.06.10-g84ce6cc4 7.08  7.09  7.10  7.11  7.12  7.13  7.14  8.00~alpha01 8.00~alpha02  8.00~alpha03  8.00~alpha04  8.00~alpha05 8.00~alpha06  8.00  8.00.01  8.00.02  8.00.03  8.00.04]
+        ocaml-version: [3.07+2, 3.08.4, 3.09.3, 3.10.2, 3.11.2, 3.12.1, 4.00.1, 4.01.0, 4.02.3, 4.03.0, 4.04.2, 4.05.0, 4.06.1, 4.07.1, 4.08.1, 4.09.1, 4.10.2, 4.11.2, 4.12.1, 4.13.1, 4.14.1]
+        camlp5-version: [6.04  6.06  6.07  6.11  6.12  6.13  6.14  6.15  6.16 6.17  7.00  7.01  7.03  7.05  7.06  7.06.10-g84ce6cc4 7.08  7.09  7.10  7.11  7.12  7.13  7.14  8.00~alpha01 8.00~alpha02  8.00~alpha03  8.00~alpha04  8.00~alpha05 8.00~alpha06  8.00  8.00.01  8.00.02  8.00.03  8.00.04]
     runs-on: ubuntu-latest
     steps:
       - name: check out hol-light ...

From 81c5945108eceaebae107dd85a499510397b521a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Mon, 16 Jan 2023 11:34:59 +0100
Subject: [PATCH 07/22] fix ci script

---
 .github/workflows/main.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 3bc59cf1..2767d0cd 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -9,7 +9,7 @@ jobs:
       fail-fast: false
       matrix:
         ocaml-version: [3.07+2, 3.08.4, 3.09.3, 3.10.2, 3.11.2, 3.12.1, 4.00.1, 4.01.0, 4.02.3, 4.03.0, 4.04.2, 4.05.0, 4.06.1, 4.07.1, 4.08.1, 4.09.1, 4.10.2, 4.11.2, 4.12.1, 4.13.1, 4.14.1]
-        camlp5-version: [6.04  6.06  6.07  6.11  6.12  6.13  6.14  6.15  6.16 6.17  7.00  7.01  7.03  7.05  7.06  7.06.10-g84ce6cc4 7.08  7.09  7.10  7.11  7.12  7.13  7.14  8.00~alpha01 8.00~alpha02  8.00~alpha03  8.00~alpha04  8.00~alpha05 8.00~alpha06  8.00  8.00.01  8.00.02  8.00.03  8.00.04]
+        camlp5-version: [6.04, 6.06, 6.07, 6.11, 6.12, 6.13, 6.14, 6.15, 6.16 6.17, 7.00, 7.01, 7.03, 7.05, 7.06, 7.06.10-g84ce6cc4 7.08, 7.09, 7.10, 7.11, 7.12, 7.13, 7.14, 8.00~alpha01 8.00~alpha02, 8.00~alpha03, 8.00~alpha04, 8.00~alpha05 8.00~alpha06, 8.00, 8.00.01, 8.00.02, 8.00.03, 8.00.04]
     runs-on: ubuntu-latest
     steps:
       - name: check out hol-light ...

From f11ac0d1ad846a555620801d7f692de4e10c10b2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Mon, 16 Jan 2023 11:38:45 +0100
Subject: [PATCH 08/22] do not test alpha version of camlp5

---
 .github/workflows/main.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 2767d0cd..35269ad2 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -9,7 +9,7 @@ jobs:
       fail-fast: false
       matrix:
         ocaml-version: [3.07+2, 3.08.4, 3.09.3, 3.10.2, 3.11.2, 3.12.1, 4.00.1, 4.01.0, 4.02.3, 4.03.0, 4.04.2, 4.05.0, 4.06.1, 4.07.1, 4.08.1, 4.09.1, 4.10.2, 4.11.2, 4.12.1, 4.13.1, 4.14.1]
-        camlp5-version: [6.04, 6.06, 6.07, 6.11, 6.12, 6.13, 6.14, 6.15, 6.16 6.17, 7.00, 7.01, 7.03, 7.05, 7.06, 7.06.10-g84ce6cc4 7.08, 7.09, 7.10, 7.11, 7.12, 7.13, 7.14, 8.00~alpha01 8.00~alpha02, 8.00~alpha03, 8.00~alpha04, 8.00~alpha05 8.00~alpha06, 8.00, 8.00.01, 8.00.02, 8.00.03, 8.00.04]
+        camlp5-version: [6.04, 6.06, 6.07, 6.11, 6.12, 6.13, 6.14, 6.15, 6.16 6.17, 7.00, 7.01, 7.03, 7.05, 7.06, 7.06.10-g84ce6cc4 7.08, 7.09, 7.10, 7.11, 7.12, 7.13, 7.14, 8.00, 8.00.01, 8.00.02, 8.00.03, 8.00.04] # 8.00~alpha01 8.00~alpha02, 8.00~alpha03, 8.00~alpha04, 8.00~alpha05 8.00~alpha06
     runs-on: ubuntu-latest
     steps:
       - name: check out hol-light ...

From e6407685f14c0291241bb347590a80299cf35023 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Mon, 16 Jan 2023 11:44:54 +0100
Subject: [PATCH 09/22] reduce matrix size

---
 .github/workflows/main.yml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 35269ad2..b7e77a01 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -7,9 +7,9 @@ jobs:
   build:
     strategy:
       fail-fast: false
-      matrix:
-        ocaml-version: [3.07+2, 3.08.4, 3.09.3, 3.10.2, 3.11.2, 3.12.1, 4.00.1, 4.01.0, 4.02.3, 4.03.0, 4.04.2, 4.05.0, 4.06.1, 4.07.1, 4.08.1, 4.09.1, 4.10.2, 4.11.2, 4.12.1, 4.13.1, 4.14.1]
-        camlp5-version: [6.04, 6.06, 6.07, 6.11, 6.12, 6.13, 6.14, 6.15, 6.16 6.17, 7.00, 7.01, 7.03, 7.05, 7.06, 7.06.10-g84ce6cc4 7.08, 7.09, 7.10, 7.11, 7.12, 7.13, 7.14, 8.00, 8.00.01, 8.00.02, 8.00.03, 8.00.04] # 8.00~alpha01 8.00~alpha02, 8.00~alpha03, 8.00~alpha04, 8.00~alpha05 8.00~alpha06
+      matrix: # limited to 256 jobs
+        ocaml-version: [4.02.3, 4.03.0, 4.04.2, 4.05.0, 4.06.1, 4.07.1, 4.08.1, 4.09.1, 4.10.2, 4.11.2, 4.12.1, 4.13.1, 4.14.1] # 13 versions # 3.07+2, 3.08.4, 3.09.3, 3.10.2, 3.11.2, 3.12.1, 4.00.1, 4.01.0
+        camlp5-version: [6.12, 6.13, 6.14, 6.15, 6.16, 6.17, 7.00, 7.01, 7.03, 7.05, 7.06.10-g84ce6cc4, 7.08, 7.09, 7.10, 7.11, 7.12, 7.13, 7.14, 8.00.04] # 19 versions # 6.04, 6.06, 6.07, 6.11, 7.06, 8.00~alpha01 8.00~alpha02, 8.00~alpha03, 8.00~alpha04, 8.00~alpha05 8.00~alpha06, 8.00, 8.00.01, 8.00.02, 8.00.03
     runs-on: ubuntu-latest
     steps:
       - name: check out hol-light ...

From 6b25cdbb8b8baf849dd52f03052c55c31115acaa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Wed, 1 Feb 2023 22:06:26 +0100
Subject: [PATCH 10/22] test camlp5.8.00.03

---
 .github/workflows/main.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index b7e77a01..3afee4c5 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -9,7 +9,7 @@ jobs:
       fail-fast: false
       matrix: # limited to 256 jobs
         ocaml-version: [4.02.3, 4.03.0, 4.04.2, 4.05.0, 4.06.1, 4.07.1, 4.08.1, 4.09.1, 4.10.2, 4.11.2, 4.12.1, 4.13.1, 4.14.1] # 13 versions # 3.07+2, 3.08.4, 3.09.3, 3.10.2, 3.11.2, 3.12.1, 4.00.1, 4.01.0
-        camlp5-version: [6.12, 6.13, 6.14, 6.15, 6.16, 6.17, 7.00, 7.01, 7.03, 7.05, 7.06.10-g84ce6cc4, 7.08, 7.09, 7.10, 7.11, 7.12, 7.13, 7.14, 8.00.04] # 19 versions # 6.04, 6.06, 6.07, 6.11, 7.06, 8.00~alpha01 8.00~alpha02, 8.00~alpha03, 8.00~alpha04, 8.00~alpha05 8.00~alpha06, 8.00, 8.00.01, 8.00.02, 8.00.03
+        camlp5-version: [6.12, 6.13, 6.14, 6.15, 6.16, 6.17, 7.00, 7.01, 7.03, 7.05, 7.06.10-g84ce6cc4, 7.08, 7.09, 7.10, 7.11, 7.12, 7.13, 7.14, 8.00.03] # 19 versions # 6.04, 6.06, 6.07, 6.11, 7.06, 8.00~alpha01 8.00~alpha02, 8.00~alpha03, 8.00~alpha04, 8.00~alpha05 8.00~alpha06, 8.00, 8.00.01, 8.00.02, 8.00.04
     runs-on: ubuntu-latest
     steps:
       - name: check out hol-light ...

From 6a74af1109b59df373f0bcd15c04ceab94db4b69 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Fri, 3 Feb 2023 12:58:46 +0100
Subject: [PATCH 11/22] wip

---
 .github/workflows/main.yml | 10 ++++------
 ci.ml                      |  4 ++++
 2 files changed, 8 insertions(+), 6 deletions(-)
 create mode 100644 ci.ml

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 3afee4c5..4ca46c15 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -14,11 +14,9 @@ jobs:
     steps:
       - name: check out hol-light ...
         uses: actions/checkout@v2
-      - name: set up cache ...
-        uses: actions/cache@v2
-        with:
-          path: ~/.opam
-          key: ${{ runner.os }}-ocaml-${{ matrix.ocaml-version }}
+    # necessary for ocaml 4.14.1 and camlp5.8.00.03
+      - name: install libipc-system-simple-perl and libstring-shellquote ...
+        run: sudo apt-get install -y libipc-system-simple-perl libstring-shellquote
       - name: set up opam ...
         uses: avsm/setup-ocaml@v1
         with:
@@ -36,4 +34,4 @@ jobs:
       - name: run test ...
         run: |
           eval $(opam env)
-          echo "#use \"hol.ml\";;" | ocaml -I `camlp5 -where` camlp5o.cma
+          cat ci.ml | ocaml
diff --git a/ci.ml b/ci.ml
new file mode 100644
index 00000000..d614530e
--- /dev/null
+++ b/ci.ml
@@ -0,0 +1,4 @@
+#use "topfind";;
+#require "camlp5";;
+#load "camlp5o.cma";;
+#use "hol.ml";;

From f6ab5d1bf7c25bfda91adcc9f000897531ba9862 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Fri, 3 Feb 2023 13:34:20 +0100
Subject: [PATCH 12/22] wip

---
 .github/workflows/main.yml | 20 ++++++--------------
 1 file changed, 6 insertions(+), 14 deletions(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 4ca46c15..68aaa39e 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -14,24 +14,16 @@ jobs:
     steps:
       - name: check out hol-light ...
         uses: actions/checkout@v2
-    # necessary for ocaml 4.14.1 and camlp5.8.00.03
-      - name: install libipc-system-simple-perl and libstring-shellquote ...
-        run: sudo apt-get install -y libipc-system-simple-perl libstring-shellquote
       - name: set up opam ...
-        uses: avsm/setup-ocaml@v1
+        uses: avsm/setup-ocaml@v2
         with:
           ocaml-version: ${{ matrix.ocaml-version }}
-      - name: install num ...
-        run: opam install num
-      - name: install ocamlfind ...
-        run: opam install ocamlfind
-      - name: install camlp5 ...
-        run: opam install camlp5.${{ matrix.camlp5-version }}
-      - name: setup hol-light ...
+      - name: install hol-light dependencies ...
         run: |
-          eval $(opam env)
-          make
-      - name: run test ...
+          sudo apt-get install -y libipc-system-simple-perl libstring-shellquote # necessary for ocaml 4.14.1 and camlp5.8.00.03
+          opam install num ocamlfind camlp5.${{ matrix.camlp5-version }}
+      - name: check hol.ml ...
         run: |
           eval $(opam env)
+          make
           cat ci.ml | ocaml

From c583c18574d39a5e792620aeafa1226cd094f3fa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Fri, 3 Feb 2023 14:00:43 +0100
Subject: [PATCH 13/22] wip

---
 .github/workflows/main.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 68aaa39e..17c97f6b 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -13,11 +13,11 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: check out hol-light ...
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
       - name: set up opam ...
         uses: avsm/setup-ocaml@v2
         with:
-          ocaml-version: ${{ matrix.ocaml-version }}
+          ocaml-compiler: ${{ matrix.ocaml-version }}
       - name: install hol-light dependencies ...
         run: |
           sudo apt-get install -y libipc-system-simple-perl libstring-shellquote # necessary for ocaml 4.14.1 and camlp5.8.00.03

From 4465734c2b93cf5784693950d6432c44e7d485c9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Wed, 8 Feb 2023 08:32:18 +0100
Subject: [PATCH 14/22] fix dep name

---
 .github/workflows/main.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 17c97f6b..eeef22b1 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -20,7 +20,7 @@ jobs:
           ocaml-compiler: ${{ matrix.ocaml-version }}
       - name: install hol-light dependencies ...
         run: |
-          sudo apt-get install -y libipc-system-simple-perl libstring-shellquote # necessary for ocaml 4.14.1 and camlp5.8.00.03
+          sudo apt-get install -y libipc-system-simple-perl libstring-shellquote-perl # necessary for ocaml 4.14.1 and camlp5.8.00.03
           opam install num ocamlfind camlp5.${{ matrix.camlp5-version }}
       - name: check hol.ml ...
         run: |

From 6775e45c6a910aa6619d87d92c828e18ca0c8707 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Wed, 8 Feb 2023 19:09:52 +0100
Subject: [PATCH 15/22] test camlp5.8.00.04

---
 .github/workflows/main.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index eeef22b1..64d71e1b 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -9,7 +9,7 @@ jobs:
       fail-fast: false
       matrix: # limited to 256 jobs
         ocaml-version: [4.02.3, 4.03.0, 4.04.2, 4.05.0, 4.06.1, 4.07.1, 4.08.1, 4.09.1, 4.10.2, 4.11.2, 4.12.1, 4.13.1, 4.14.1] # 13 versions # 3.07+2, 3.08.4, 3.09.3, 3.10.2, 3.11.2, 3.12.1, 4.00.1, 4.01.0
-        camlp5-version: [6.12, 6.13, 6.14, 6.15, 6.16, 6.17, 7.00, 7.01, 7.03, 7.05, 7.06.10-g84ce6cc4, 7.08, 7.09, 7.10, 7.11, 7.12, 7.13, 7.14, 8.00.03] # 19 versions # 6.04, 6.06, 6.07, 6.11, 7.06, 8.00~alpha01 8.00~alpha02, 8.00~alpha03, 8.00~alpha04, 8.00~alpha05 8.00~alpha06, 8.00, 8.00.01, 8.00.02, 8.00.04
+        camlp5-version: [8.00.04] #[6.12, 6.13, 6.14, 6.15, 6.16, 6.17, 7.00, 7.01, 7.03, 7.05, 7.06.10-g84ce6cc4, 7.08, 7.09, 7.10, 7.11, 7.12, 7.13, 7.14, 8.00.04] # 19 versions # 6.04, 6.06, 6.07, 6.11, 7.06, 8.00~alpha01 8.00~alpha02, 8.00~alpha03, 8.00~alpha04, 8.00~alpha05 8.00~alpha06, 8.00, 8.00.01, 8.00.02, 8.00.03
     runs-on: ubuntu-latest
     steps:
       - name: check out hol-light ...

From 0885c0344ae8780c7cffec73dc12611601760db0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Wed, 8 Feb 2023 19:39:24 +0100
Subject: [PATCH 16/22] start using a yml file for each camlp5 version

---
 .github/workflows/camlp5-deps.txt             | 34 +++++++++++++++++++
 .../{main.yml => camlp5.8.00.02.yml}          |  4 +--
 .github/workflows/camlp5.8.00.03.yml          | 29 ++++++++++++++++
 .github/workflows/camlp5.8.00.04.yml          | 29 ++++++++++++++++
 .github/workflows/get-camlp5-deps.sh          |  7 ++++
 5 files changed, 101 insertions(+), 2 deletions(-)
 create mode 100644 .github/workflows/camlp5-deps.txt
 rename .github/workflows/{main.yml => camlp5.8.00.02.yml} (65%)
 create mode 100644 .github/workflows/camlp5.8.00.03.yml
 create mode 100644 .github/workflows/camlp5.8.00.04.yml
 create mode 100755 .github/workflows/get-camlp5-deps.sh

diff --git a/.github/workflows/camlp5-deps.txt b/.github/workflows/camlp5-deps.txt
new file mode 100644
index 00000000..e41492c9
--- /dev/null
+++ b/.github/workflows/camlp5-deps.txt
@@ -0,0 +1,34 @@
+camlp5.6.04 depends      "ocaml" {= "3.12.1"}
+camlp5.6.06 depends      "ocaml" {<= "4.00.0"}
+camlp5.6.07 depends      "ocaml" {< "4.01.0"}
+camlp5.6.11 depends      "ocaml" {< "4.02.0"}
+camlp5.6.12 depends      "ocaml" {< "4.02.2"}
+camlp5.6.13 depends      "ocaml" {< "4.02.3"}
+camlp5.6.14 depends      "ocaml" {< "4.02.4"}
+camlp5.6.15 depends      "ocaml" {>= "4.02.0" & <= "4.03.0"}
+camlp5.6.16 depends      "ocaml" {>= "1.07" & <= "4.03.0"}
+camlp5.6.17 depends      "ocaml" {>= "1.07" & <= "4.04.1"}
+camlp5.7.00 depends      "ocaml" {>= "4.02" & <= "4.06"}
+camlp5.7.01 depends      "ocaml" {>= "4.02" & <= "4.05.0"}
+camlp5.7.03 depends      "ocaml" {>= "4.02" & < "4.06.1"}
+camlp5.7.05 depends      "ocaml" {>= "4.02" & < "4.06.3"}
+camlp5.7.06 depends      "ocaml" {>= "4.02" & <= "4.07.0"}
+camlp5.7.06.10-g84ce6cc4 depends      "ocaml" {>= "4.02" & <= "4.07.1"}
+camlp5.7.08 depends      "ocaml" {>= "4.02" & <= "4.08.0"}
+camlp5.7.09 depends      "ocaml" {>= "4.08" & < "4.10.0" & != "4.09.1"}
+camlp5.7.10 depends      "ocaml" {>= "4.02" & < "4.10.0" & != "4.09.1"}
+camlp5.7.11 depends      "ocaml" {>= "4.02" & <= "4.10.0"}
+camlp5.7.12 depends      "ocaml" {>= "4.02" & <= "4.11.0" & != "4.10.2"}
+camlp5.7.13 depends      "ocaml" {>= "4.02" & <= "4.11.1" & != "4.10.2"}
+camlp5.7.14 depends      "ocaml" {>= "4.02" & < "4.13.0"} "conf-perl"
+camlp5.8.00~alpha01 depends      "ocaml" {>= "4.02" & <= "4.11.0" & != "4.10.1" & != "4.10.2"}
+camlp5.8.00~alpha02 depends      "ocaml" {>= "4.02" & <= "4.11.0" & != "4.10.1" & != "4.10.2"}
+camlp5.8.00~alpha03 depends      "ocaml" {>= "4.02" & <= "4.11.0" & != "4.10.2"}
+camlp5.8.00~alpha04 depends      "ocaml" {>= "4.02" & < "4.12.0"}
+camlp5.8.00~alpha05 depends      "ocaml" {>= "4.02" & < "4.12.0"}
+camlp5.8.00~alpha06 depends      "ocaml" {>= "4.02" & < "4.12.0"}
+camlp5.8.00 depends      "ocaml" {>= "4.02" & < "4.13.0"}
+camlp5.8.00.01 depends      "ocaml" {>= "4.02" & < "4.13.0"}
+camlp5.8.00.02 depends      "ocaml" {>= "4.02" & < "4.14.0"}
+camlp5.8.00.03 depends      "ocaml" {>= "4.05" & < "4.15.0"}
+camlp5.8.00.04 depends      "ocaml" {>= "4.05" & < "5.01.0"}
diff --git a/.github/workflows/main.yml b/.github/workflows/camlp5.8.00.02.yml
similarity index 65%
rename from .github/workflows/main.yml
rename to .github/workflows/camlp5.8.00.02.yml
index 64d71e1b..47da79e7 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/camlp5.8.00.02.yml
@@ -8,8 +8,8 @@ jobs:
     strategy:
       fail-fast: false
       matrix: # limited to 256 jobs
-        ocaml-version: [4.02.3, 4.03.0, 4.04.2, 4.05.0, 4.06.1, 4.07.1, 4.08.1, 4.09.1, 4.10.2, 4.11.2, 4.12.1, 4.13.1, 4.14.1] # 13 versions # 3.07+2, 3.08.4, 3.09.3, 3.10.2, 3.11.2, 3.12.1, 4.00.1, 4.01.0
-        camlp5-version: [8.00.04] #[6.12, 6.13, 6.14, 6.15, 6.16, 6.17, 7.00, 7.01, 7.03, 7.05, 7.06.10-g84ce6cc4, 7.08, 7.09, 7.10, 7.11, 7.12, 7.13, 7.14, 8.00.04] # 19 versions # 6.04, 6.06, 6.07, 6.11, 7.06, 8.00~alpha01 8.00~alpha02, 8.00~alpha03, 8.00~alpha04, 8.00~alpha05 8.00~alpha06, 8.00, 8.00.01, 8.00.02, 8.00.03
+        ocaml-version: [4.02.3, 4.03.0, 4.04.2, 4.05.0, 4.06.1, 4.07.1, 4.08.1, 4.09.1, 4.10.2, 4.11.2, 4.12.1, 4.13.1] # 12 versions
+        camlp5-version: [8.00.02]
     runs-on: ubuntu-latest
     steps:
       - name: check out hol-light ...
diff --git a/.github/workflows/camlp5.8.00.03.yml b/.github/workflows/camlp5.8.00.03.yml
new file mode 100644
index 00000000..8789d143
--- /dev/null
+++ b/.github/workflows/camlp5.8.00.03.yml
@@ -0,0 +1,29 @@
+on:
+  pull_request:
+    types: [opened, synchronize, edited, reopened]
+  push:
+  workflow_dispatch:
+jobs:
+  build:
+    strategy:
+      fail-fast: false
+      matrix: # limited to 256 jobs
+        ocaml-version: [4.05.0, 4.06.1, 4.07.1, 4.08.1, 4.09.1, 4.10.2, 4.11.2, 4.12.1, 4.13.1, 4.14.1] # 10 versions
+        camlp5-version: [8.00.03]
+    runs-on: ubuntu-latest
+    steps:
+      - name: check out hol-light ...
+        uses: actions/checkout@v3
+      - name: set up opam ...
+        uses: avsm/setup-ocaml@v2
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-version }}
+      - name: install hol-light dependencies ...
+        run: |
+          sudo apt-get install -y libipc-system-simple-perl libstring-shellquote-perl # necessary for ocaml 4.14.1 and camlp5.8.00.03
+          opam install num ocamlfind camlp5.${{ matrix.camlp5-version }}
+      - name: check hol.ml ...
+        run: |
+          eval $(opam env)
+          make
+          cat ci.ml | ocaml
diff --git a/.github/workflows/camlp5.8.00.04.yml b/.github/workflows/camlp5.8.00.04.yml
new file mode 100644
index 00000000..fac0eea0
--- /dev/null
+++ b/.github/workflows/camlp5.8.00.04.yml
@@ -0,0 +1,29 @@
+on:
+  pull_request:
+    types: [opened, synchronize, edited, reopened]
+  push:
+  workflow_dispatch:
+jobs:
+  build:
+    strategy:
+      fail-fast: false
+      matrix: # limited to 256 jobs
+        ocaml-version: [4.05.0, 4.06.1, 4.07.1, 4.08.1, 4.09.1, 4.10.2, 4.11.2, 4.12.1, 4.13.1, 4.14.1] # 10 versions
+        camlp5-version: [8.00.04]
+    runs-on: ubuntu-latest
+    steps:
+      - name: check out hol-light ...
+        uses: actions/checkout@v3
+      - name: set up opam ...
+        uses: avsm/setup-ocaml@v2
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-version }}
+      - name: install hol-light dependencies ...
+        run: |
+          sudo apt-get install -y libipc-system-simple-perl libstring-shellquote-perl # necessary for ocaml 4.14.1 and camlp5.8.00.03
+          opam install num ocamlfind camlp5.${{ matrix.camlp5-version }}
+      - name: check hol.ml ...
+        run: |
+          eval $(opam env)
+          make
+          cat ci.ml | ocaml
diff --git a/.github/workflows/get-camlp5-deps.sh b/.github/workflows/get-camlp5-deps.sh
new file mode 100755
index 00000000..f53ffd24
--- /dev/null
+++ b/.github/workflows/get-camlp5-deps.sh
@@ -0,0 +1,7 @@
+#!/bin/sh
+
+for v in 6.04  6.06  6.07  6.11  6.12  6.13  6.14  6.15  6.16 6.17  7.00  7.01  7.03  7.05  7.06  7.06.10-g84ce6cc4 7.08  7.09  7.10  7.11  7.12  7.13  7.14  8.00~alpha01 8.00~alpha02  8.00~alpha03  8.00~alpha04  8.00~alpha05 8.00~alpha06  8.00  8.00.01  8.00.02  8.00.03  8.00.04
+do
+    echo -n "camlp5.$v "
+    opam info camlp5.$v | grep depends
+done

From 0ba94d0134b930f4ee00b4741fcd430879f86bb0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Wed, 15 Feb 2023 15:56:54 +0100
Subject: [PATCH 17/22] test camlp5.8.00.05

---
 .github/workflows/camlp5-deps.txt    | 67 ++++++++++++++--------------
 .github/workflows/camlp5.8.00.02.yml |  2 +-
 .github/workflows/camlp5.8.00.03.yml |  2 +-
 .github/workflows/camlp5.8.00.04.yml |  2 +-
 .github/workflows/camlp5.8.00.05.yml | 29 ++++++++++++
 .github/workflows/get-camlp5-deps.sh |  2 +-
 6 files changed, 67 insertions(+), 37 deletions(-)
 create mode 100644 .github/workflows/camlp5.8.00.05.yml

diff --git a/.github/workflows/camlp5-deps.txt b/.github/workflows/camlp5-deps.txt
index e41492c9..13c1be96 100644
--- a/.github/workflows/camlp5-deps.txt
+++ b/.github/workflows/camlp5-deps.txt
@@ -1,34 +1,35 @@
-camlp5.6.04 depends      "ocaml" {= "3.12.1"}
-camlp5.6.06 depends      "ocaml" {<= "4.00.0"}
-camlp5.6.07 depends      "ocaml" {< "4.01.0"}
-camlp5.6.11 depends      "ocaml" {< "4.02.0"}
-camlp5.6.12 depends      "ocaml" {< "4.02.2"}
-camlp5.6.13 depends      "ocaml" {< "4.02.3"}
-camlp5.6.14 depends      "ocaml" {< "4.02.4"}
-camlp5.6.15 depends      "ocaml" {>= "4.02.0" & <= "4.03.0"}
-camlp5.6.16 depends      "ocaml" {>= "1.07" & <= "4.03.0"}
-camlp5.6.17 depends      "ocaml" {>= "1.07" & <= "4.04.1"}
-camlp5.7.00 depends      "ocaml" {>= "4.02" & <= "4.06"}
-camlp5.7.01 depends      "ocaml" {>= "4.02" & <= "4.05.0"}
-camlp5.7.03 depends      "ocaml" {>= "4.02" & < "4.06.1"}
-camlp5.7.05 depends      "ocaml" {>= "4.02" & < "4.06.3"}
-camlp5.7.06 depends      "ocaml" {>= "4.02" & <= "4.07.0"}
-camlp5.7.06.10-g84ce6cc4 depends      "ocaml" {>= "4.02" & <= "4.07.1"}
-camlp5.7.08 depends      "ocaml" {>= "4.02" & <= "4.08.0"}
-camlp5.7.09 depends      "ocaml" {>= "4.08" & < "4.10.0" & != "4.09.1"}
-camlp5.7.10 depends      "ocaml" {>= "4.02" & < "4.10.0" & != "4.09.1"}
-camlp5.7.11 depends      "ocaml" {>= "4.02" & <= "4.10.0"}
-camlp5.7.12 depends      "ocaml" {>= "4.02" & <= "4.11.0" & != "4.10.2"}
-camlp5.7.13 depends      "ocaml" {>= "4.02" & <= "4.11.1" & != "4.10.2"}
-camlp5.7.14 depends      "ocaml" {>= "4.02" & < "4.13.0"} "conf-perl"
-camlp5.8.00~alpha01 depends      "ocaml" {>= "4.02" & <= "4.11.0" & != "4.10.1" & != "4.10.2"}
-camlp5.8.00~alpha02 depends      "ocaml" {>= "4.02" & <= "4.11.0" & != "4.10.1" & != "4.10.2"}
-camlp5.8.00~alpha03 depends      "ocaml" {>= "4.02" & <= "4.11.0" & != "4.10.2"}
-camlp5.8.00~alpha04 depends      "ocaml" {>= "4.02" & < "4.12.0"}
-camlp5.8.00~alpha05 depends      "ocaml" {>= "4.02" & < "4.12.0"}
-camlp5.8.00~alpha06 depends      "ocaml" {>= "4.02" & < "4.12.0"}
-camlp5.8.00 depends      "ocaml" {>= "4.02" & < "4.13.0"}
-camlp5.8.00.01 depends      "ocaml" {>= "4.02" & < "4.13.0"}
-camlp5.8.00.02 depends      "ocaml" {>= "4.02" & < "4.14.0"}
-camlp5.8.00.03 depends      "ocaml" {>= "4.05" & < "4.15.0"}
+camlp5.8.00.05 depends      "ocaml" {>= "4.10" & < "5.01.0"}
 camlp5.8.00.04 depends      "ocaml" {>= "4.05" & < "5.01.0"}
+camlp5.8.00.03 depends      "ocaml" {>= "4.05" & < "4.15.0"}
+camlp5.8.00.02 depends      "ocaml" {>= "4.02" & < "4.14.0"}
+camlp5.8.00.01 depends      "ocaml" {>= "4.02" & < "4.13.0"}
+camlp5.8.00 depends      "ocaml" {>= "4.02" & < "4.13.0"}
+camlp5.8.00~alpha06 depends      "ocaml" {>= "4.02" & < "4.12.0"}
+camlp5.8.00~alpha05 depends      "ocaml" {>= "4.02" & < "4.12.0"}
+camlp5.8.00~alpha04 depends      "ocaml" {>= "4.02" & < "4.12.0"}
+camlp5.8.00~alpha03 depends      "ocaml" {>= "4.02" & <= "4.11.0" & != "4.10.2"}
+camlp5.8.00~alpha02 depends      "ocaml" {>= "4.02" & <= "4.11.0" & != "4.10.1" & != "4.10.2"}
+camlp5.8.00~alpha01 depends      "ocaml" {>= "4.02" & <= "4.11.0" & != "4.10.1" & != "4.10.2"}
+camlp5.7.14 depends      "ocaml" {>= "4.02" & < "4.13.0"} "conf-perl"
+camlp5.7.13 depends      "ocaml" {>= "4.02" & <= "4.11.1" & != "4.10.2"}
+camlp5.7.12 depends      "ocaml" {>= "4.02" & <= "4.11.0" & != "4.10.2"}
+camlp5.7.11 depends      "ocaml" {>= "4.02" & <= "4.10.0"}
+camlp5.7.10 depends      "ocaml" {>= "4.02" & < "4.10.0" & != "4.09.1"}
+camlp5.7.09 depends      "ocaml" {>= "4.08" & < "4.10.0" & != "4.09.1"}
+camlp5.7.08 depends      "ocaml" {>= "4.02" & <= "4.08.0"}
+camlp5.7.06.10-g84ce6cc4 depends      "ocaml" {>= "4.02" & <= "4.07.1"}
+camlp5.7.06 depends      "ocaml" {>= "4.02" & <= "4.07.0"}
+camlp5.7.05 depends      "ocaml" {>= "4.02" & < "4.06.3"}
+camlp5.7.03 depends      "ocaml" {>= "4.02" & < "4.06.1"}
+camlp5.7.01 depends      "ocaml" {>= "4.02" & <= "4.05.0"}
+camlp5.7.00 depends      "ocaml" {>= "4.02" & <= "4.06"}
+camlp5.6.17 depends      "ocaml" {>= "1.07" & <= "4.04.1"}
+camlp5.6.16 depends      "ocaml" {>= "1.07" & <= "4.03.0"}
+camlp5.6.15 depends      "ocaml" {>= "4.02.0" & <= "4.03.0"}
+camlp5.6.14 depends      "ocaml" {< "4.02.4"}
+camlp5.6.13 depends      "ocaml" {< "4.02.3"}
+camlp5.6.12 depends      "ocaml" {< "4.02.2"}
+camlp5.6.11 depends      "ocaml" {< "4.02.0"}
+camlp5.6.07 depends      "ocaml" {< "4.01.0"}
+camlp5.6.06 depends      "ocaml" {<= "4.00.0"}
+camlp5.6.04 depends      "ocaml" {= "3.12.1"}
diff --git a/.github/workflows/camlp5.8.00.02.yml b/.github/workflows/camlp5.8.00.02.yml
index 47da79e7..bb129f67 100644
--- a/.github/workflows/camlp5.8.00.02.yml
+++ b/.github/workflows/camlp5.8.00.02.yml
@@ -20,7 +20,7 @@ jobs:
           ocaml-compiler: ${{ matrix.ocaml-version }}
       - name: install hol-light dependencies ...
         run: |
-          sudo apt-get install -y libipc-system-simple-perl libstring-shellquote-perl # necessary for ocaml 4.14.1 and camlp5.8.00.03
+          sudo apt-get install -y libipc-system-simple-perl libstring-shellquote-perl
           opam install num ocamlfind camlp5.${{ matrix.camlp5-version }}
       - name: check hol.ml ...
         run: |
diff --git a/.github/workflows/camlp5.8.00.03.yml b/.github/workflows/camlp5.8.00.03.yml
index 8789d143..36084815 100644
--- a/.github/workflows/camlp5.8.00.03.yml
+++ b/.github/workflows/camlp5.8.00.03.yml
@@ -20,7 +20,7 @@ jobs:
           ocaml-compiler: ${{ matrix.ocaml-version }}
       - name: install hol-light dependencies ...
         run: |
-          sudo apt-get install -y libipc-system-simple-perl libstring-shellquote-perl # necessary for ocaml 4.14.1 and camlp5.8.00.03
+          sudo apt-get install -y libipc-system-simple-perl libstring-shellquote-perl
           opam install num ocamlfind camlp5.${{ matrix.camlp5-version }}
       - name: check hol.ml ...
         run: |
diff --git a/.github/workflows/camlp5.8.00.04.yml b/.github/workflows/camlp5.8.00.04.yml
index fac0eea0..4d3940db 100644
--- a/.github/workflows/camlp5.8.00.04.yml
+++ b/.github/workflows/camlp5.8.00.04.yml
@@ -20,7 +20,7 @@ jobs:
           ocaml-compiler: ${{ matrix.ocaml-version }}
       - name: install hol-light dependencies ...
         run: |
-          sudo apt-get install -y libipc-system-simple-perl libstring-shellquote-perl # necessary for ocaml 4.14.1 and camlp5.8.00.03
+          sudo apt-get install -y libipc-system-simple-perl libstring-shellquote-perl
           opam install num ocamlfind camlp5.${{ matrix.camlp5-version }}
       - name: check hol.ml ...
         run: |
diff --git a/.github/workflows/camlp5.8.00.05.yml b/.github/workflows/camlp5.8.00.05.yml
new file mode 100644
index 00000000..686688f7
--- /dev/null
+++ b/.github/workflows/camlp5.8.00.05.yml
@@ -0,0 +1,29 @@
+on:
+  pull_request:
+    types: [opened, synchronize, edited, reopened]
+  push:
+  workflow_dispatch:
+jobs:
+  build:
+    strategy:
+      fail-fast: false
+      matrix: # limited to 256 jobs
+        ocaml-version: [4.10.2, 4.11.2, 4.12.1, 4.13.1, 4.14.1] # 5 versions
+        camlp5-version: [8.00.05]
+    runs-on: ubuntu-latest
+    steps:
+      - name: check out hol-light ...
+        uses: actions/checkout@v3
+      - name: set up opam ...
+        uses: avsm/setup-ocaml@v2
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-version }}
+      - name: install hol-light dependencies ...
+        run: |
+          sudo apt-get install -y libipc-system-simple-perl libstring-shellquote-perl
+          opam install num ocamlfind camlp5.${{ matrix.camlp5-version }}
+      - name: check hol.ml ...
+        run: |
+          eval $(opam env)
+          make
+          cat ci.ml | ocaml
diff --git a/.github/workflows/get-camlp5-deps.sh b/.github/workflows/get-camlp5-deps.sh
index f53ffd24..2c548c6d 100755
--- a/.github/workflows/get-camlp5-deps.sh
+++ b/.github/workflows/get-camlp5-deps.sh
@@ -1,6 +1,6 @@
 #!/bin/sh
 
-for v in 6.04  6.06  6.07  6.11  6.12  6.13  6.14  6.15  6.16 6.17  7.00  7.01  7.03  7.05  7.06  7.06.10-g84ce6cc4 7.08  7.09  7.10  7.11  7.12  7.13  7.14  8.00~alpha01 8.00~alpha02  8.00~alpha03  8.00~alpha04  8.00~alpha05 8.00~alpha06  8.00  8.00.01  8.00.02  8.00.03  8.00.04
+for v in 8.00.05 8.00.04 8.00.03 8.00.02 8.00.01 8.00 8.00~alpha06 8.00~alpha05 8.00~alpha04 8.00~alpha03 8.00~alpha02 8.00~alpha01 7.14 7.13 7.12 7.11 7.10 7.09 7.08 7.06.10-g84ce6cc4 7.06 7.05 7.03 7.01 7.00 6.17 6.16 6.15 6.14 6.13 6.12 6.11 6.07 6.06 6.04
 do
     echo -n "camlp5.$v "
     opam info camlp5.$v | grep depends

From 46ae2827de42e857a49869e3ba6c76a7b23a1ea4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Sun, 12 Mar 2023 10:08:46 +0100
Subject: [PATCH 18/22] test ocaml 5.0.0

---
 .github/workflows/camlp5.8.00.04.yml | 2 +-
 .github/workflows/camlp5.8.00.05.yml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/camlp5.8.00.04.yml b/.github/workflows/camlp5.8.00.04.yml
index 4d3940db..8f1a28e2 100644
--- a/.github/workflows/camlp5.8.00.04.yml
+++ b/.github/workflows/camlp5.8.00.04.yml
@@ -8,7 +8,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix: # limited to 256 jobs
-        ocaml-version: [4.05.0, 4.06.1, 4.07.1, 4.08.1, 4.09.1, 4.10.2, 4.11.2, 4.12.1, 4.13.1, 4.14.1] # 10 versions
+        ocaml-version: [4.05.0, 4.06.1, 4.07.1, 4.08.1, 4.09.1, 4.10.2, 4.11.2, 4.12.1, 4.13.1, 4.14.1, 5.0.0] # 11 versions
         camlp5-version: [8.00.04]
     runs-on: ubuntu-latest
     steps:
diff --git a/.github/workflows/camlp5.8.00.05.yml b/.github/workflows/camlp5.8.00.05.yml
index 686688f7..73c8c0ae 100644
--- a/.github/workflows/camlp5.8.00.05.yml
+++ b/.github/workflows/camlp5.8.00.05.yml
@@ -8,7 +8,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix: # limited to 256 jobs
-        ocaml-version: [4.10.2, 4.11.2, 4.12.1, 4.13.1, 4.14.1] # 5 versions
+        ocaml-version: [4.10.2, 4.11.2, 4.12.1, 4.13.1, 4.14.1, 5.0.0] # 6 versions
         camlp5-version: [8.00.05]
     runs-on: ubuntu-latest
     steps:

From 94e85b6443e6624d72c41b0dccc9d6340d4e75f5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Wed, 22 Nov 2023 08:23:50 +0100
Subject: [PATCH 19/22] test new versions of camlp5

---
 .github/workflows/camlp5-deps.txt    |  3 +++
 .github/workflows/camlp5.8.01.00.yml | 29 ++++++++++++++++++++++++++++
 .github/workflows/camlp5.8.02.00.yml | 29 ++++++++++++++++++++++++++++
 .github/workflows/camlp5.8.02.01.yml | 29 ++++++++++++++++++++++++++++
 .github/workflows/get-camlp5-deps.sh |  2 +-
 5 files changed, 91 insertions(+), 1 deletion(-)
 create mode 100644 .github/workflows/camlp5.8.01.00.yml
 create mode 100644 .github/workflows/camlp5.8.02.00.yml
 create mode 100644 .github/workflows/camlp5.8.02.01.yml

diff --git a/.github/workflows/camlp5-deps.txt b/.github/workflows/camlp5-deps.txt
index 13c1be96..8943509d 100644
--- a/.github/workflows/camlp5-deps.txt
+++ b/.github/workflows/camlp5-deps.txt
@@ -1,3 +1,6 @@
+camlp5.8.02.01 depends      "ocaml" {>= "4.10" & < "5.02.0"}
+camlp5.8.02.00 depends      "ocaml" {>= "4.10" & < "5.02.0"}
+camlp5.8.01.00 depends      "ocaml" {>= "4.10" & < "5.01.0"}
 camlp5.8.00.05 depends      "ocaml" {>= "4.10" & < "5.01.0"}
 camlp5.8.00.04 depends      "ocaml" {>= "4.05" & < "5.01.0"}
 camlp5.8.00.03 depends      "ocaml" {>= "4.05" & < "4.15.0"}
diff --git a/.github/workflows/camlp5.8.01.00.yml b/.github/workflows/camlp5.8.01.00.yml
new file mode 100644
index 00000000..5666ecd1
--- /dev/null
+++ b/.github/workflows/camlp5.8.01.00.yml
@@ -0,0 +1,29 @@
+on:
+  pull_request:
+    types: [opened, synchronize, edited, reopened]
+  push:
+  workflow_dispatch:
+jobs:
+  build:
+    strategy:
+      fail-fast: false
+      matrix: # limited to 256 jobs
+        ocaml-version: [4.10.2, 4.11.2, 4.12.1, 4.13.1, 4.14.1, 5.0.0] # 6 versions
+        camlp5-version: [8.01.00]
+    runs-on: ubuntu-latest
+    steps:
+      - name: check out hol-light ...
+        uses: actions/checkout@v3
+      - name: set up opam ...
+        uses: avsm/setup-ocaml@v2
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-version }}
+      - name: install hol-light dependencies ...
+        run: |
+          sudo apt-get install -y libipc-system-simple-perl libstring-shellquote-perl
+          opam install num ocamlfind camlp5.${{ matrix.camlp5-version }}
+      - name: check hol.ml ...
+        run: |
+          eval $(opam env)
+          make
+          cat ci.ml | ocaml
diff --git a/.github/workflows/camlp5.8.02.00.yml b/.github/workflows/camlp5.8.02.00.yml
new file mode 100644
index 00000000..97e253b0
--- /dev/null
+++ b/.github/workflows/camlp5.8.02.00.yml
@@ -0,0 +1,29 @@
+on:
+  pull_request:
+    types: [opened, synchronize, edited, reopened]
+  push:
+  workflow_dispatch:
+jobs:
+  build:
+    strategy:
+      fail-fast: false
+      matrix: # limited to 256 jobs
+        ocaml-version: [4.10.2, 4.11.2, 4.12.1, 4.13.1, 4.14.1, 5.0.0, 5.1.0] # 7 versions
+        camlp5-version: [8.02.00]
+    runs-on: ubuntu-latest
+    steps:
+      - name: check out hol-light ...
+        uses: actions/checkout@v3
+      - name: set up opam ...
+        uses: avsm/setup-ocaml@v2
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-version }}
+      - name: install hol-light dependencies ...
+        run: |
+          sudo apt-get install -y libipc-system-simple-perl libstring-shellquote-perl
+          opam install num ocamlfind camlp5.${{ matrix.camlp5-version }}
+      - name: check hol.ml ...
+        run: |
+          eval $(opam env)
+          make
+          cat ci.ml | ocaml
diff --git a/.github/workflows/camlp5.8.02.01.yml b/.github/workflows/camlp5.8.02.01.yml
new file mode 100644
index 00000000..fc482ebe
--- /dev/null
+++ b/.github/workflows/camlp5.8.02.01.yml
@@ -0,0 +1,29 @@
+on:
+  pull_request:
+    types: [opened, synchronize, edited, reopened]
+  push:
+  workflow_dispatch:
+jobs:
+  build:
+    strategy:
+      fail-fast: false
+      matrix: # limited to 256 jobs
+        ocaml-version: [4.10.2, 4.11.2, 4.12.1, 4.13.1, 4.14.1, 5.0.0, 5.1.0] # 7 versions
+        camlp5-version: [8.02.01]
+    runs-on: ubuntu-latest
+    steps:
+      - name: check out hol-light ...
+        uses: actions/checkout@v3
+      - name: set up opam ...
+        uses: avsm/setup-ocaml@v2
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-version }}
+      - name: install hol-light dependencies ...
+        run: |
+          sudo apt-get install -y libipc-system-simple-perl libstring-shellquote-perl
+          opam install num ocamlfind camlp5.${{ matrix.camlp5-version }}
+      - name: check hol.ml ...
+        run: |
+          eval $(opam env)
+          make
+          cat ci.ml | ocaml
diff --git a/.github/workflows/get-camlp5-deps.sh b/.github/workflows/get-camlp5-deps.sh
index 2c548c6d..1364f766 100755
--- a/.github/workflows/get-camlp5-deps.sh
+++ b/.github/workflows/get-camlp5-deps.sh
@@ -1,6 +1,6 @@
 #!/bin/sh
 
-for v in 8.00.05 8.00.04 8.00.03 8.00.02 8.00.01 8.00 8.00~alpha06 8.00~alpha05 8.00~alpha04 8.00~alpha03 8.00~alpha02 8.00~alpha01 7.14 7.13 7.12 7.11 7.10 7.09 7.08 7.06.10-g84ce6cc4 7.06 7.05 7.03 7.01 7.00 6.17 6.16 6.15 6.14 6.13 6.12 6.11 6.07 6.06 6.04
+for v in 8.02.01 8.02.00 8.01.00 8.00.05 8.00.04 8.00.03 8.00.02 8.00.01 8.00 8.00~alpha06 8.00~alpha05 8.00~alpha04 8.00~alpha03 8.00~alpha02 8.00~alpha01 7.14 7.13 7.12 7.11 7.10 7.09 7.08 7.06.10-g84ce6cc4 7.06 7.05 7.03 7.01 7.00 6.17 6.16 6.15 6.14 6.13 6.12 6.11 6.07 6.06 6.04
 do
     echo -n "camlp5.$v "
     opam info camlp5.$v | grep depends

From 15ff3029b39c94c6354aeeb44692498a549fcea7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Wed, 22 Nov 2023 09:07:35 +0100
Subject: [PATCH 20/22] add README

---
 .github/workflows/README.md | 39 +++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)
 create mode 100644 .github/workflows/README.md

diff --git a/.github/workflows/README.md b/.github/workflows/README.md
new file mode 100644
index 00000000..43d07727
--- /dev/null
+++ b/.github/workflows/README.md
@@ -0,0 +1,39 @@
+Please do not merge this PR but keep it open: the purpose of this PR is just to check working ocaml-camlp5 pairs when it is updated. 
+
+This PR adds some github action scripts to inventory the pairs ocaml-camlp5 for which hol-light works.
+
+For each camlp5 version, we add a yml script testing the ocaml versions meaningful for this camlp5 version.
+
+Remarks:
+- we only test "hol.ml"
+- we sometimes need to install the following packages: libipc-system-simple-perl, libstring-shellquote-perl
+- github accepts up to 256 jobs maximum
+
+Working pairs found:
+| ocaml | camlp5 |
+| --- | --- |
+| 4.02.3 | 6.14, 6.15, 6.16, 6.17, 7.01, 7.03, 7.05, 7.06.10-g84ce6cc4, 7.08, 7.1 |
+| 4.03.0 | 6.15, 6.16, 6.17, 7.01, 7.03, 7.05, 7.06.10-g84ce6cc4, 7.08, 7.1 |
+| 4.04.2 | 7.01, 7.03, 7.05, 7.06.10-g84ce6cc4, 7.08, 7.1 |
+| 4.05.0 | 7.01, 7.03, 7.05, 7.06.10-g84ce6cc4, 7.08, 7.1 |
+| 4.06.1 | 7.05, 7.06.10-g84ce6cc4, 7.08, 7.11, 7.12, 7.13, 7.14 |
+| 4.07.1 | 7.06.10-g84ce6cc4, 7.08, 7.11, 7.12, 7.13, 7.14 |
+| 4.08.1 | 7.09, 7.11, 7.12, 7.13, 7.14, 8.00.03, 8.00.04 |
+| 4.09.1 | 7.11, 7.12, 7.13, 7.14, 8.00.03, 8.00.04 |
+| 4.10.2 | 7.14, 8.00.03, 8.00.04, 8.00.05, 8.02.00, 8.02.01 |
+| 4.11.2 | 7.14, 8.00.03, 8.00.04, 8.00.05, 8.02.00, 8.02.01 |
+| 4.12.1 | 7.14, 8.00.03, 8.00.04, 8.00.05, 8.02.00, 8.02.01 |
+| 4.13.1 | 8.00.03, 8.00.04, 8.00.05, 8.02.00, 8.02.01 |
+| 4.14.1 | 8.00.03, 8.00.04, 8.00.05, 8.02.00, 8.02.01 |
+
+Detailed results can be found in:
+| camlp5 | results |
+| --- | --- |
+| 8.02.01 | https://github.com/fblanqui/hol-light/actions/runs/6954163356 |
+| 8.02.00 | https://github.com/fblanqui/hol-light/actions/runs/6954163355 |
+| 8.01.00 | https://github.com/fblanqui/hol-light/actions/runs/6954163352 |
+| 8.00.05 | https://github.com/fblanqui/hol-light/actions/runs/4185147934 |
+| 8.00.04 | https://github.com/fblanqui/hol-light/actions/runs/4127325386 |
+| 8.00.03 | https://github.com/fblanqui/hol-light/actions/runs/4127325387 |
+| 8.00.02 | https://github.com/fblanqui/hol-light/actions/runs/4127325397 |
+| other | https://github.com/fblanqui/hol-light/actions/runs/3929583606 |

From 4ac7d3cd11b0739f6bb875bbdb8d74e17809a229 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Tue, 16 Apr 2024 22:08:12 +0200
Subject: [PATCH 21/22] update table with ocaml 5.1.1

---
 .github/workflows/README.md                   | 39 -----------------
 .../test-ocaml-camlp5-pairs/README.md         | 42 +++++++++++++++++++
 .../camlp5-deps.txt                           |  0
 .../camlp5.8.00.02.yml                        |  0
 .../camlp5.8.00.03.yml                        |  0
 .../camlp5.8.00.04.yml                        |  0
 .../camlp5.8.00.05.yml                        |  0
 .../camlp5.8.01.00.yml                        |  0
 .../camlp5.8.02.00.yml                        |  0
 .../camlp5.8.02.01.yml                        |  6 +--
 .../get-camlp5-deps.sh                        |  0
 11 files changed, 45 insertions(+), 42 deletions(-)
 delete mode 100644 .github/workflows/README.md
 create mode 100644 .github/workflows/test-ocaml-camlp5-pairs/README.md
 rename .github/workflows/{ => test-ocaml-camlp5-pairs}/camlp5-deps.txt (100%)
 rename .github/workflows/{ => test-ocaml-camlp5-pairs}/camlp5.8.00.02.yml (100%)
 rename .github/workflows/{ => test-ocaml-camlp5-pairs}/camlp5.8.00.03.yml (100%)
 rename .github/workflows/{ => test-ocaml-camlp5-pairs}/camlp5.8.00.04.yml (100%)
 rename .github/workflows/{ => test-ocaml-camlp5-pairs}/camlp5.8.00.05.yml (100%)
 rename .github/workflows/{ => test-ocaml-camlp5-pairs}/camlp5.8.01.00.yml (100%)
 rename .github/workflows/{ => test-ocaml-camlp5-pairs}/camlp5.8.02.00.yml (100%)
 rename .github/workflows/{ => test-ocaml-camlp5-pairs}/camlp5.8.02.01.yml (84%)
 rename .github/workflows/{ => test-ocaml-camlp5-pairs}/get-camlp5-deps.sh (100%)

diff --git a/.github/workflows/README.md b/.github/workflows/README.md
deleted file mode 100644
index 43d07727..00000000
--- a/.github/workflows/README.md
+++ /dev/null
@@ -1,39 +0,0 @@
-Please do not merge this PR but keep it open: the purpose of this PR is just to check working ocaml-camlp5 pairs when it is updated. 
-
-This PR adds some github action scripts to inventory the pairs ocaml-camlp5 for which hol-light works.
-
-For each camlp5 version, we add a yml script testing the ocaml versions meaningful for this camlp5 version.
-
-Remarks:
-- we only test "hol.ml"
-- we sometimes need to install the following packages: libipc-system-simple-perl, libstring-shellquote-perl
-- github accepts up to 256 jobs maximum
-
-Working pairs found:
-| ocaml | camlp5 |
-| --- | --- |
-| 4.02.3 | 6.14, 6.15, 6.16, 6.17, 7.01, 7.03, 7.05, 7.06.10-g84ce6cc4, 7.08, 7.1 |
-| 4.03.0 | 6.15, 6.16, 6.17, 7.01, 7.03, 7.05, 7.06.10-g84ce6cc4, 7.08, 7.1 |
-| 4.04.2 | 7.01, 7.03, 7.05, 7.06.10-g84ce6cc4, 7.08, 7.1 |
-| 4.05.0 | 7.01, 7.03, 7.05, 7.06.10-g84ce6cc4, 7.08, 7.1 |
-| 4.06.1 | 7.05, 7.06.10-g84ce6cc4, 7.08, 7.11, 7.12, 7.13, 7.14 |
-| 4.07.1 | 7.06.10-g84ce6cc4, 7.08, 7.11, 7.12, 7.13, 7.14 |
-| 4.08.1 | 7.09, 7.11, 7.12, 7.13, 7.14, 8.00.03, 8.00.04 |
-| 4.09.1 | 7.11, 7.12, 7.13, 7.14, 8.00.03, 8.00.04 |
-| 4.10.2 | 7.14, 8.00.03, 8.00.04, 8.00.05, 8.02.00, 8.02.01 |
-| 4.11.2 | 7.14, 8.00.03, 8.00.04, 8.00.05, 8.02.00, 8.02.01 |
-| 4.12.1 | 7.14, 8.00.03, 8.00.04, 8.00.05, 8.02.00, 8.02.01 |
-| 4.13.1 | 8.00.03, 8.00.04, 8.00.05, 8.02.00, 8.02.01 |
-| 4.14.1 | 8.00.03, 8.00.04, 8.00.05, 8.02.00, 8.02.01 |
-
-Detailed results can be found in:
-| camlp5 | results |
-| --- | --- |
-| 8.02.01 | https://github.com/fblanqui/hol-light/actions/runs/6954163356 |
-| 8.02.00 | https://github.com/fblanqui/hol-light/actions/runs/6954163355 |
-| 8.01.00 | https://github.com/fblanqui/hol-light/actions/runs/6954163352 |
-| 8.00.05 | https://github.com/fblanqui/hol-light/actions/runs/4185147934 |
-| 8.00.04 | https://github.com/fblanqui/hol-light/actions/runs/4127325386 |
-| 8.00.03 | https://github.com/fblanqui/hol-light/actions/runs/4127325387 |
-| 8.00.02 | https://github.com/fblanqui/hol-light/actions/runs/4127325397 |
-| other | https://github.com/fblanqui/hol-light/actions/runs/3929583606 |
diff --git a/.github/workflows/test-ocaml-camlp5-pairs/README.md b/.github/workflows/test-ocaml-camlp5-pairs/README.md
new file mode 100644
index 00000000..df2238ca
--- /dev/null
+++ b/.github/workflows/test-ocaml-camlp5-pairs/README.md
@@ -0,0 +1,42 @@
+Please do not merge this PR but keep it open: its purpose is to provide data on working ocaml-camlp5 pairs.
+
+It contains some github action scripts to inventory the pairs ocaml-camlp5 for which hol-light works.
+
+For each camlp5 version, there is a yml script testing the ocaml versions meaningful for this camlp5 version.
+
+Remarks:
+- we only test "hol.ml"
+- we sometimes need to install the following packages: libipc-system-simple-perl, libstring-shellquote-perl
+- github accepts up to 256 jobs maximum
+
+Working pairs found (this may not be exhaustive):
+
+| ocaml  | camlp5                                                                 |
+|--------|------------------------------------------------------------------------|
+| 4.02.3 | 6.14, 6.15, 6.16, 6.17, 7.01, 7.03, 7.05, 7.06.10-g84ce6cc4, 7.08, 7.1 |
+| 4.03.0 | 6.15, 6.16, 6.17, 7.01, 7.03, 7.05, 7.06.10-g84ce6cc4, 7.08, 7.1       |
+| 4.04.2 | 7.01, 7.03, 7.05, 7.06.10-g84ce6cc4, 7.08, 7.1                         |
+| 4.05.0 | 7.01, 7.03, 7.05, 7.06.10-g84ce6cc4, 7.08, 7.1                         |
+| 4.06.1 | 7.05, 7.06.10-g84ce6cc4, 7.08, 7.11, 7.12, 7.13, 7.14                  |
+| 4.07.1 | 7.06.10-g84ce6cc4, 7.08, 7.11, 7.12, 7.13, 7.14                        |
+| 4.08.1 | 7.09, 7.11, 7.12, 7.13, 7.14, 8.00.03, 8.00.04                         |
+| 4.09.1 | 7.11, 7.12, 7.13, 7.14, 8.00.03, 8.00.04                               |
+| 4.10.2 | 7.14, 8.00.03, 8.00.04, 8.00.05, 8.02.00, 8.02.01                      |
+| 4.11.2 | 7.14, 8.00.03, 8.00.04, 8.00.05, 8.02.00, 8.02.01                      |
+| 4.12.1 | 7.14, 8.00.03, 8.00.04, 8.00.05, 8.02.00, 8.02.01                      |
+| 4.13.1 | 8.00.03, 8.00.04, 8.00.05, 8.02.00, 8.02.01                            |
+| 4.14.1 | 8.00.03, 8.00.04, 8.00.05, 8.02.00, 8.02.01                            |
+| 5.1.1  | 8.02.01                                                                |
+
+Detailed results can be found in:
+
+| camlp5  | results                                                       |
+|---------|---------------------------------------------------------------|
+| 8.02.01 | https://github.com/fblanqui/hol-light/actions/runs/8710772959 |
+| 8.02.00 | https://github.com/fblanqui/hol-light/actions/runs/6954163355 |
+| 8.01.00 | https://github.com/fblanqui/hol-light/actions/runs/6954163352 |
+| 8.00.05 | https://github.com/fblanqui/hol-light/actions/runs/4185147934 |
+| 8.00.04 | https://github.com/fblanqui/hol-light/actions/runs/4127325386 |
+| 8.00.03 | https://github.com/fblanqui/hol-light/actions/runs/4127325387 |
+| 8.00.02 | https://github.com/fblanqui/hol-light/actions/runs/4127325397 |
+| other   | https://github.com/fblanqui/hol-light/actions/runs/3929583606 |
diff --git a/.github/workflows/camlp5-deps.txt b/.github/workflows/test-ocaml-camlp5-pairs/camlp5-deps.txt
similarity index 100%
rename from .github/workflows/camlp5-deps.txt
rename to .github/workflows/test-ocaml-camlp5-pairs/camlp5-deps.txt
diff --git a/.github/workflows/camlp5.8.00.02.yml b/.github/workflows/test-ocaml-camlp5-pairs/camlp5.8.00.02.yml
similarity index 100%
rename from .github/workflows/camlp5.8.00.02.yml
rename to .github/workflows/test-ocaml-camlp5-pairs/camlp5.8.00.02.yml
diff --git a/.github/workflows/camlp5.8.00.03.yml b/.github/workflows/test-ocaml-camlp5-pairs/camlp5.8.00.03.yml
similarity index 100%
rename from .github/workflows/camlp5.8.00.03.yml
rename to .github/workflows/test-ocaml-camlp5-pairs/camlp5.8.00.03.yml
diff --git a/.github/workflows/camlp5.8.00.04.yml b/.github/workflows/test-ocaml-camlp5-pairs/camlp5.8.00.04.yml
similarity index 100%
rename from .github/workflows/camlp5.8.00.04.yml
rename to .github/workflows/test-ocaml-camlp5-pairs/camlp5.8.00.04.yml
diff --git a/.github/workflows/camlp5.8.00.05.yml b/.github/workflows/test-ocaml-camlp5-pairs/camlp5.8.00.05.yml
similarity index 100%
rename from .github/workflows/camlp5.8.00.05.yml
rename to .github/workflows/test-ocaml-camlp5-pairs/camlp5.8.00.05.yml
diff --git a/.github/workflows/camlp5.8.01.00.yml b/.github/workflows/test-ocaml-camlp5-pairs/camlp5.8.01.00.yml
similarity index 100%
rename from .github/workflows/camlp5.8.01.00.yml
rename to .github/workflows/test-ocaml-camlp5-pairs/camlp5.8.01.00.yml
diff --git a/.github/workflows/camlp5.8.02.00.yml b/.github/workflows/test-ocaml-camlp5-pairs/camlp5.8.02.00.yml
similarity index 100%
rename from .github/workflows/camlp5.8.02.00.yml
rename to .github/workflows/test-ocaml-camlp5-pairs/camlp5.8.02.00.yml
diff --git a/.github/workflows/camlp5.8.02.01.yml b/.github/workflows/test-ocaml-camlp5-pairs/camlp5.8.02.01.yml
similarity index 84%
rename from .github/workflows/camlp5.8.02.01.yml
rename to .github/workflows/test-ocaml-camlp5-pairs/camlp5.8.02.01.yml
index fc482ebe..5fbf4833 100644
--- a/.github/workflows/camlp5.8.02.01.yml
+++ b/.github/workflows/test-ocaml-camlp5-pairs/camlp5.8.02.01.yml
@@ -8,12 +8,12 @@ jobs:
     strategy:
       fail-fast: false
       matrix: # limited to 256 jobs
-        ocaml-version: [4.10.2, 4.11.2, 4.12.1, 4.13.1, 4.14.1, 5.0.0, 5.1.0] # 7 versions
+        ocaml-version: [4.10.2, 4.11.2, 4.12.1, 4.13.1, 4.14.1, 5.0.0, 5.1.1] # 7 versions
         camlp5-version: [8.02.01]
     runs-on: ubuntu-latest
     steps:
       - name: check out hol-light ...
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
       - name: set up opam ...
         uses: avsm/setup-ocaml@v2
         with:
@@ -21,7 +21,7 @@ jobs:
       - name: install hol-light dependencies ...
         run: |
           sudo apt-get install -y libipc-system-simple-perl libstring-shellquote-perl
-          opam install num ocamlfind camlp5.${{ matrix.camlp5-version }}
+          opam install num zarith ocamlfind camlp5.${{ matrix.camlp5-version }}
       - name: check hol.ml ...
         run: |
           eval $(opam env)
diff --git a/.github/workflows/get-camlp5-deps.sh b/.github/workflows/test-ocaml-camlp5-pairs/get-camlp5-deps.sh
similarity index 100%
rename from .github/workflows/get-camlp5-deps.sh
rename to .github/workflows/test-ocaml-camlp5-pairs/get-camlp5-deps.sh

From 01f2f0e73935401de35c96300d7247e8ccde548f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Tue, 16 Apr 2024 22:13:49 +0200
Subject: [PATCH 22/22] add ocaml 5.0.0

---
 .github/workflows/test-ocaml-camlp5-pairs/README.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/test-ocaml-camlp5-pairs/README.md b/.github/workflows/test-ocaml-camlp5-pairs/README.md
index df2238ca..f347a1cf 100644
--- a/.github/workflows/test-ocaml-camlp5-pairs/README.md
+++ b/.github/workflows/test-ocaml-camlp5-pairs/README.md
@@ -26,6 +26,7 @@ Working pairs found (this may not be exhaustive):
 | 4.12.1 | 7.14, 8.00.03, 8.00.04, 8.00.05, 8.02.00, 8.02.01                      |
 | 4.13.1 | 8.00.03, 8.00.04, 8.00.05, 8.02.00, 8.02.01                            |
 | 4.14.1 | 8.00.03, 8.00.04, 8.00.05, 8.02.00, 8.02.01                            |
+| 5.0.0  | 8.02.01                                                                |
 | 5.1.1  | 8.02.01                                                                |
 
 Detailed results can be found in: