LPTP/.github/workflows/ci.yml at main · FredMesnard/LPTP · 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
name: CI

on:
  push:
  pull_request:
  workflow_dispatch:

jobs:
  proofs:
    name: proofs (${{ matrix.prolog }})
    runs-on: ubuntu-latest
    strategy:
      fail-fast: false
      matrix:
        prolog: [swi, gprolog]
    steps:
      - uses: actions/checkout@v7

      - name: Install SWI-Prolog
        if: matrix.prolog == 'swi'
        run: |
          sudo apt-get update
          sudo apt-get install -y --no-install-recommends swi-prolog-nox

      - name: Install GNU Prolog
        if: matrix.prolog == 'gprolog'
        run: |
          sudo apt-get update
          sudo apt-get install -y --no-install-recommends gprolog

      - name: Check the whole proof corpus
        run: etc/run-tests.sh ${{ matrix.prolog }}

      # src/system.pl and some .thm files are version-controlled yet rewritten
      # by a run, so the script puts them back. This is what says it worked.
      - name: The run must leave the working tree untouched
        run: |
          if [ -n "$(git status --porcelain)" ]; then
            echo "the check run left the working tree dirty:"
            git status --porcelain
            git diff
            exit 1
          fi

      - name: Upload generated proofs
        if: always()
        uses: actions/upload-artifact@v7
        with:
          name: tmp-${{ matrix.prolog }}
          path: tmp/
          if-no-files-found: ignore

  emacs:
    name: emacs mode
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v7

      - name: Install Emacs
        run: |
          sudo apt-get update
          sudo apt-get install -y --no-install-recommends emacs-nox

      - name: Byte-compile and exercise lptp-mode
        run: |
          emacs --batch --eval '
            (progn
              (unless (byte-compile-file "etc/lptp-mode.el")
                (error "byte-compilation of etc/lptp-mode.el failed"))
              (load (expand-file-name "etc/lptp-mode.el"))
              (find-file "lib/list/list.pr")
              (lptp-mode)
              (unless (eq major-mode (quote lptp-mode))
                (error "lptp-mode did not activate"))
              ;; Guards against faces that Emacs has since removed.
              (font-lock-mode 1)
              (font-lock-ensure)
              (message "lptp-mode: ok"))'