Working ocaml-camlp5 pairs

.github/workflows/test-ocaml-camlp5-pairs/README.md

@@ -0,0 +1,43 @@
+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.0.0  | 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 |

.github/workflows/test-ocaml-camlp5-pairs/camlp5-deps.txt

@@ -0,0 +1,38 @@
+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"}
+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"}

.github/workflows/test-ocaml-camlp5-pairs/camlp5.8.00.02.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.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 ...
+        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

.github/workflows/test-ocaml-camlp5-pairs/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
+          opam install num ocamlfind camlp5.${{ matrix.camlp5-version }}
+      - name: check hol.ml ...
+        run: |
+          eval $(opam env)
+          make
+          cat ci.ml | ocaml

.github/workflows/test-ocaml-camlp5-pairs/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, 5.0.0] # 11 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
+          opam install num ocamlfind camlp5.${{ matrix.camlp5-version }}
+      - name: check hol.ml ...
+        run: |
+          eval $(opam env)
+          make
+          cat ci.ml | ocaml

.github/workflows/test-ocaml-camlp5-pairs/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.0.0] # 6 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

.github/workflows/test-ocaml-camlp5-pairs/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

.github/workflows/test-ocaml-camlp5-pairs/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

.github/workflows/test-ocaml-camlp5-pairs/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.1] # 7 versions
+        camlp5-version: [8.02.01]
+    runs-on: ubuntu-latest
+    steps:
+      - name: check out hol-light ...
+        uses: actions/checkout@v4
+      - 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 zarith ocamlfind camlp5.${{ matrix.camlp5-version }}
+      - name: check hol.ml ...
+        run: |
+          eval $(opam env)
+          make
+          cat ci.ml | ocaml

.github/workflows/test-ocaml-camlp5-pairs/get-camlp5-deps.sh

@@ -0,0 +1,7 @@
+#!/bin/sh
+
+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
+done

ci.ml

@@ -0,0 +1,4 @@
+#use "topfind";;
+#require "camlp5";;
+#load "camlp5o.cma";;
+#use "hol.ml";;