hol-light-dev/.github/workflows/main.yml at f1493131f3672e3f85493ba6b0183a46f4e3b548 · jargh/hol-light-dev · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
name: CI

on:
  # Allows you to run this workflow manually from the Actions tab
  workflow_dispatch:

  # check PRs
  pull_request:
    branches:
      - master

  # check pushes
  push:
    branches:
      - master

jobs:
  test1:
    runs-on: ubuntu-22.04
    name: OCaml 4.06, Camlp5 7.10

    steps:
      - name: Install dependency
        run: |
          sudo apt update && sudo apt install -y opam
          opam init --disable-sandboxing --compiler=4.06.0
          opam repository add archive git+https://github.com/ocaml/opam-repository-archive
          opam pin -y add camlp5 7.10
          opam install -y num ledit camlp-streams ocamlfind

      - name: Checkout this repo
        uses: actions/checkout@v6
        with:
          path: hol-light

      - name: Run
        run: |
          set -xe
          cd hol-light
          eval $(opam env)
          make
          (echo 'loadt "update_database.ml";;') | ./hol.sh 2>&1 | tee log.txt
          grep "Error" log.txt && exit 1
          grep "Camlp5 parsing version" log.txt

  test2:
    runs-on: ubuntu-22.04
    name: OCaml 4.14, Camlp5 8.03 (make switch)

    steps:
      - name: Install dependency
        run: |
          sudo apt update && sudo apt install -y opam xdot
          opam init --disable-sandboxing

      - name: Checkout this repo
        uses: actions/checkout@v6
        with:
          path: hol-light

      - name: Run
        run: |
          set -xe
          cd hol-light
          make switch
          eval $(opam env)
          make
          (echo 'loadt "update_database.ml";;') | ./hol.sh 2>&1 | tee log.txt
          grep "Error" log.txt && exit 1
          grep "Camlp5 parsing version (HOL-Light)" log.txt
          cd ..

      - name: Run (HOLLIGHT_USE_MODULE=1)
        run: |
          set -xe
          cd hol-light
          eval $(opam env)
          make clean
          export HOLLIGHT_USE_MODULE=1
          make
          ./hol.sh 2>&1 | tee log.txt
          grep "Error" log.txt && exit 1
          grep "Camlp5 parsing version (HOL-Light)" log.txt
          ./unit_tests.byte
          ./unit_tests.native

  test3:
    runs-on: ubuntu-22.04
    name: OCaml 5.4, Camlp5 8.04 (make switch-5)

    steps:
      - name: Install dependency
        run: |
          sudo apt update && sudo apt install -y opam xdot
          opam init --disable-sandboxing

      - name: Checkout this repo
        uses: actions/checkout@v6
        with:
          path: hol-light

      - name: Run
        run: |
          set -xe
          cd hol-light
          make switch-5
          eval $(opam env)
          make
          (echo 'loadt "update_database.ml";;') | ./hol.sh 2>&1 | tee log.txt
          grep "Error" log.txt && exit 1
          grep "Camlp5 parsing version (HOL-Light)" log.txt
          cd ..

      - name: Run (HOLLIGHT_USE_MODULE=1)
        run: |
          set -xe
          cd hol-light
          eval $(opam env)
          make clean
          export HOLLIGHT_USE_MODULE=1
          make
          (echo 'loadt "update_database.ml";;') | ./hol.sh 2>&1 | tee log.txt
          grep "Error" log.txt && exit 1
          grep "Camlp5 parsing version (HOL-Light)" log.txt
          ./unit_tests.byte
          ./unit_tests.native