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..f347a1cf --- /dev/null +++ b/.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 | diff --git a/.github/workflows/test-ocaml-camlp5-pairs/camlp5-deps.txt b/.github/workflows/test-ocaml-camlp5-pairs/camlp5-deps.txt new file mode 100644 index 00000000..8943509d --- /dev/null +++ b/.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"} diff --git a/.github/workflows/test-ocaml-camlp5-pairs/camlp5.8.00.02.yml b/.github/workflows/test-ocaml-camlp5-pairs/camlp5.8.00.02.yml new file mode 100644 index 00000000..bb129f67 --- /dev/null +++ b/.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 diff --git a/.github/workflows/test-ocaml-camlp5-pairs/camlp5.8.00.03.yml b/.github/workflows/test-ocaml-camlp5-pairs/camlp5.8.00.03.yml new file mode 100644 index 00000000..36084815 --- /dev/null +++ b/.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 diff --git a/.github/workflows/test-ocaml-camlp5-pairs/camlp5.8.00.04.yml b/.github/workflows/test-ocaml-camlp5-pairs/camlp5.8.00.04.yml new file mode 100644 index 00000000..8f1a28e2 --- /dev/null +++ b/.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 diff --git a/.github/workflows/test-ocaml-camlp5-pairs/camlp5.8.00.05.yml b/.github/workflows/test-ocaml-camlp5-pairs/camlp5.8.00.05.yml new file mode 100644 index 00000000..73c8c0ae --- /dev/null +++ b/.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 diff --git a/.github/workflows/test-ocaml-camlp5-pairs/camlp5.8.01.00.yml b/.github/workflows/test-ocaml-camlp5-pairs/camlp5.8.01.00.yml new file mode 100644 index 00000000..5666ecd1 --- /dev/null +++ b/.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 diff --git a/.github/workflows/test-ocaml-camlp5-pairs/camlp5.8.02.00.yml b/.github/workflows/test-ocaml-camlp5-pairs/camlp5.8.02.00.yml new file mode 100644 index 00000000..97e253b0 --- /dev/null +++ b/.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 diff --git a/.github/workflows/test-ocaml-camlp5-pairs/camlp5.8.02.01.yml b/.github/workflows/test-ocaml-camlp5-pairs/camlp5.8.02.01.yml new file mode 100644 index 00000000..5fbf4833 --- /dev/null +++ b/.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 diff --git a/.github/workflows/test-ocaml-camlp5-pairs/get-camlp5-deps.sh b/.github/workflows/test-ocaml-camlp5-pairs/get-camlp5-deps.sh new file mode 100755 index 00000000..1364f766 --- /dev/null +++ b/.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 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";;