Merge pull request #483 from ProofGeneral/use-github-actions

Use GitHub actions

7 files changed, 293 insertions, 55 deletions

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
new file mode 100644
index 00000000..4b4bf8ec
--- /dev/null
+++ b/.github/workflows/test.yml
@@ -0,0 +1,81 @@
+name: CI
+
+on:
+  push:
+    branches:
+      - master
+      - hybrid
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    strategy:
+      matrix:
+        emacs_version:
+          - 24.3
+          - 24.4
+          - 24.5
+          - 25.1
+          - 25.2
+          - 25.3
+          - 26.1
+          - 26.2
+          - 26.3
+      # at most 20 concurrent jobs per free account
+      # cf. https://help.github.com/en/actions/reference/workflow-syntax-for-github-actions#usage-limit
+      max-parallel: 4
+
+    steps:
+    - uses: actions/checkout@v2
+
+    - uses: purcell/setup-emacs@master
+      with:
+        version: ${{ matrix.emacs_version }}
+
+    - run: emacs --version
+    - run: make
+
+  test:
+    runs-on: ubuntu-latest
+
+    strategy:
+      matrix:
+        # emacs_version:
+          # the emacs version in Ubuntu 18.04 LTS
+          # - 25.2
+          # the emacs version in Debian Buster
+          # - 26.1
+          # the emacs version in Debian Sid
+          # - 26.3
+        coq_version:
+          - 8.11
+        ocaml_version:
+          - minimal
+      # at most 20 concurrent jobs per free account
+      # cf. https://help.github.com/en/actions/reference/workflow-syntax-for-github-actions#usage-limit
+      max-parallel: 6
+
+    steps:
+    - uses: actions/checkout@v2
+
+    - uses: erikmd/docker-coq-action@alpha
+      id: docker-coq-action
+      with:
+        opam_file: 'dummy.opam'
+        coq_version: ${{ matrix.coq_version }}
+        ocaml_version: ${{ matrix.ocaml_version }}
+        custom_script: |
+          startGroup Print opam config
+            opam config list; opam repo list; opam list
+          endGroup
+          startGroup Install emacs
+            sudo apt-get update -y -q
+            sudo DEBIAN_FRONTEND=noninteractive apt-get install -y -q --no-install-recommends emacs
+          endGroup
+          startGroup Run tests
+            ./ci/test.sh
+          endGroup
diff --git a/.travis.yml b/.travis.yml
deleted file mode 100644
index 6f70e507..00000000
--- a/.travis.yml
+++ /dev/null
@@ -1,24 +0,0 @@
-language: emacs-lisp
-sudo: true
-
-env:
-  - EMACS_TARGET=emacs-24.3
-  - EMACS_TARGET=emacs-24.4
-  - EMACS_TARGET=emacs-24.5
-  - EMACS_TARGET=emacs-25.1
-  - EMACS_TARGET=emacs-25.2
-  - EMACS_TARGET=emacs-25.3
-
-before_install:
-  - make -f Makefile.travis before_install
-
-install:
-  - make -f Makefile.travis install
-
-script:
-  - emacs --version
-  - make -f Makefile.travis script
-
-notifications:
-  slack:
-    secure: "Cul0iDgsNZgDYCyuHE7a2D1XCWzbFMBi/3J9MIfddWwChL5EEEv/A1EI+VVjXwzWLyvyeJLv7V8PmPUKMuACjlcQcTKcb1q/1WV3k6Y5kR5Z29HktCNTF27KX/e/6bNeKMVvjC0EERRxIi9GAwCOOokapCxS5FjjPnVubGf99FNfRFXePh9FeRg3I7XcSNCjKicZgNGczME1vPxERbpcFnMXPD5+vPhjKjJWQJUNpZUnonRRqfbNmSCwu/oy0Uby3lJhmcLm2Fc7UggD/IYcFbefbLgzmImVmra1qzRH9ZLF5fVS59npd+o2iowL27SQCYxGtqMc6gX85h9evzwgL2KFMXCV6om1r5pwBOBnEPgkiNKqCig9R5Ij+nHbkEkZqPBwEcXqeQyVsXUEV5yiU5qwDZXe2z1dlqhPa8tRpxRNk0IUdVVYeOsOS+AhbkUDkbYMlOY+yMiY5J4P94AhhDmYzuLTuSNi3ZGdPNCJcx0JSTLALITT5NJp1QljaOO5Xq/8UHTRlVdfFKijfpLfaCT6VloigXw8kTbxhm5Kpf5aZqFC/3uCg+4D6CuBI/IiWNADJcLMocJqS/Rp6kUA+VqAMMWfpyWySihDHSuw0WXeDVZL/ZhynVagIV+0/VcqYzQKXDzCEOaD0lJp3ypeKfjBAz18N6s7LH/yBFHfJck="
diff --git a/Makefile.travis b/Makefile.travis
deleted file mode 100644
index 1aa04dc0..00000000
--- a/Makefile.travis
+++ /dev/null
@@ -1,30 +0,0 @@
-VERSIONS = 24.3 24.4 24.5 25.1 25.2 25.3
-STABLE_TARGETS = $(addprefix prepare-emacs-,$(VERSIONS))
-
-.PHONY: prepare-emacs-24 prepare-emacs-git $(STABLE_TARGETS) \
-        prepare-emacs before_install install script
-
-$(STABLE_TARGETS):
-	curl -o /tmp/$(EMACS_TARGET).tar.gz "https://ftp.gnu.org/gnu/emacs/$(EMACS_TARGET).tar.gz"
-	mkdir /tmp/emacs-tmp
-	tar xzf /tmp/$(EMACS_TARGET).tar.gz -C /tmp/emacs-tmp
-	mv /tmp/emacs-tmp/* "/tmp/emacs" || (ls /tmp/*; exit 1)
-
-prepare-emacs-git:
-	git clone --depth=1 'git://git.savannah.gnu.org/emacs.git' --branch emacs-25 /tmp/emacs
-	cd /tmp/emacs && ./autogen.sh
-
-prepare-emacs: prepare-$(EMACS_TARGET)
-	echo 0 | sudo tee /proc/sys/kernel/randomize_va_space
-	cd /tmp/emacs && ./configure --prefix="$(HOME)" --without-all --with-x-toolkit=no --without-x --with-xml2 && make -j2 install
-
-before_install: prepare-emacs
-
-install:
-
-script:
-	make
-
-# Local Variables:
-# indent-tabs-mode: t
-# End:
diff --git a/README.md b/README.md
index 95c73b43..909eddd2 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,6 @@
 # Proof General — Organize your proofs! 
 
-[![Build Status](https://travis-ci.org/ProofGeneral/PG.svg?branch=master)](https://travis-ci.org/ProofGeneral/PG)
+[![CI](https://github.com/ProofGeneral/PG/workflows/CI/badge.svg?branch=master)](https://github.com/ProofGeneral/PG/actions?query=workflow%3ACI)
 [![MELPA](http://melpa.org/packages/proof-general-badge.svg)](https://melpa.org/#/proof-general)
 
 ## Overview
diff --git a/ci/coq-tests.el b/ci/coq-tests.el
new file mode 100644
index 00000000..057f918e
--- /dev/null
+++ b/ci/coq-tests.el
@@ -0,0 +1,139 @@
+;;; coq-tests.el --- integration tests -*- lexical-binding: t; -*-
+
+;;; Commentary:
+;;
+
+;;;  Eval this to run the tests interactively <C-x C-e>
+;;
+;; (call-interactively #'ert-run-tests-interactively)
+
+(setq debug-on-error t) ; open the debugger on error -- may be commented-out
+
+(require 'ert-async)
+;(setq ert-async-timeout 2)
+
+;;; Code:
+
+; Exemple de code Lisp qui lance des commandes au prouveur en arrière-plan
+; (defun has-error ()
+;   "True if error in Proof"
+;   (eq 'error proof-shell-last-output-kind))
+; 
+; (defun test-process-invisible-split ()
+;   (proof-shell-invisible-command "split."
+;    'waitforit
+;     #'proof-done-invisible
+;     'no-error-display 'no-response-display 'no-goals-display))
+; 
+; (defun test-process-invisible-tactics-then-reset-and-insert ()
+;   (interactive)
+;   (let ((reset-cmd ; store backtracking info before proof search
+;            (format "Backtrack %s %s %s . "
+;                    (int-to-string coq-last-but-one-statenum)
+;                    (int-to-string coq-last-but-one-proofnum)
+;                    0)))
+;          ;; Toy example of proof search
+;          (while (not (has-error))
+;                 (message "Trying split.")
+;                 (test-process-invisible-split))
+;          ;; Reset to the previous state
+;          (proof-shell-invisible-command reset-cmd 'waitforit #'proof-done-invisible)
+;          ;; Insert (and re-process) the found script
+;          (proof-insert-sendback-command "split.\nsplit.\nsplit.\nQed.")))
+; 
+; (test-process-invisible-tactics-then-reset-and-insert)
+
+(defconst coq-test-file-prefix "coq_test_")
+
+(defun coq-test-init ()
+  "Ensure `coq' is loaded."
+  (unless (featurep 'coq)
+    (add-to-list 'load-path
+		 (locate-dominating-file buffer-file-name "proof-general.el"))
+    (load "proof-general")
+    (proofgeneral "coq")))
+
+(defun coq-test-exit ()
+  "Exit the Coq process."
+  (proof-shell-exit t))
+
+;; AVOID THE FOLLOWING ERROR:
+;; Starting:  -emacs
+;; Debugger entered--Lisp error: (wrong-type-argument stringp nil)
+;;   file-name-directory(nil)
+;;   scomint-exec-1("coq" #<buffer *coq*> nil ("-emacs"))
+;;   scomint-exec(#<buffer *coq*> "coq" nil nil ("-emacs"))
+;;   scomint-make-in-buffer("coq" nil nil nil "-emacs")
+;;   apply(scomint-make-in-buffer "coq" nil nil nil "-emacs")
+;;   scomint-make("coq" nil nil "-emacs")
+;;   apply(scomint-make ("coq" nil nil "-emacs"))
+;;   proof-shell-start()
+;;   proof-shell-ready-prover()
+(defmacro coq-test-on-file (&rest body)
+  "Eval BODY like `progn' after opening a temporary Coq file."
+  ;; For more info: https://mullikine.github.io/posts/macro-tutorial/
+  `(let ((file (concat (make-temp-file coq-test-file-prefix) ".v")))
+     (message "Opening file %s ..." file)
+     (save-excursion          
+       (let ((buffer (find-file file))
+             (res (progn ,@body)))
+         (progn (kill-buffer buffer)
+                (ignore-errors (delete-file file))
+                res)))))
+; (pp (macroexpand '(coq-test-on-file (message "OK"))))
+; (coq-test-on-file (message (buffer-file-name)) (message "OK") 42)
+
+;; DEFINITION OF MOCKS, SEE `coq-mock' BELOW
+;; Another solution would consist in using el-mock, mentioned in:
+;; https://www.gnu.org/software/emacs/manual/html_mono/ert.html#Mocks-and-Stubs
+(defun mock-proof-display-three-b (&rest rest)
+  (message (concat "Skipping proof-display-three-b on input: "
+                   (pp-to-string rest)))
+  ; Result:
+  nil)
+
+;; AVOID THE FOLLOWING ERROR:
+;; Hit M-x proof-layout-windows to reset layout
+;; Debugger entered--Lisp error: (error "Window #<window 6 on *goals*> too small for splitting")
+;;   signal(error ("Window #<window 6 on *goals*> too small for splitting"))
+;;   error("Window %s too small for splitting" #<window 6 on *goals*>)
+;;   split-window(nil nil)
+;;   split-window-vertically()
+;;   proof-safe-split-window-vertically()
+;;   proof-select-three-b(nil #<buffer *goals*> #<buffer *response*> smart)
+;;   proof-display-three-b(smart)
+;;   proof-layout-windows()
+;;   proof-multiple-frames-enable()
+;;   proof-shell-start()
+;;   proof-shell-ready-prover()
+(defun coq-mock (f)
+  (require 'pg-response) ; load the feature defining proof-display-three-b first
+   (cl-letf (;((symbol-function 'foo) #'mock-foo)
+             ((symbol-function 'proof-display-three-b) #'mock-proof-display-three-b))
+     (funcall f)))
+;; Run <C-x C-e> on:
+;; (coq-mock #'main)
+
+(defun coq-test-cmd (cmd)
+  (coq-test-on-file
+    (coq-test-init)
+    (proof-shell-invisible-command
+     cmd
+     'waitforit
+     #'proof-done-invisible
+     'no-error-display 'no-response-display 'no-goals-display)))
+
+(defun coq-test-001 ()
+  ;; TODO: retrieve the test status, maybe by changing the function above
+  (coq-test-cmd "Print nat."))
+;; TODO: Use https://github.com/rejeep/ert-async.el
+;; and/or ERT https://www.gnu.org/software/emacs/manual/html_node/ert/index.html
+
+(defun coq-test-main ()
+  (coq-mock #'coq-test-001))
+
+;(ignore-errors (coq-test-exit))
+(coq-test-main)
+
+(provide 'coq-tests)
+;;; learn-ocaml-tests.el ends here
diff --git a/ci/init-tests.el b/ci/init-tests.el
new file mode 100644
index 00000000..565df976
--- /dev/null
+++ b/ci/init-tests.el
@@ -0,0 +1,34 @@
+;;; init-tests.el --- tests init file -*- coding: utf-8; lexical-binding: t; -*-
+
+;;; Commentary:
+;;
+;; Load this file to setup MELPA and tests-related packages.
+;;
+
+;;; Code:
+
+;; Setup MELPA
+(require 'package)
+(let* ((no-ssl (and (memq system-type '(windows-nt ms-dos))
+                    (not (gnutls-available-p))))
+       (proto (if no-ssl "http" "https")))
+  (add-to-list 'package-archives
+               (cons "melpa" (concat proto "://melpa.org/packages/")) t))
+(package-initialize)
+
+;; Optionally: bootstrap use-package for declarative package specs
+;(unless (package-installed-p 'use-package)
+;(package-refresh-contents)
+;(package-install 'use-package))
+;(eval-when-compile
+;  (require 'use-package))
+
+;; Bootstrap ert-async
+(unless (package-installed-p 'ert-async)
+  (package-refresh-contents)
+  (package-install 'ert-async))
+(eval-when-compile
+  (require 'ert-async))
+
+(provide 'init-tests)
+;;; init-tests.el ends here
diff --git a/ci/test.sh b/ci/test.sh
new file mode 100755
index 00000000..b29d5af7
--- /dev/null
+++ b/ci/test.sh
@@ -0,0 +1,38 @@
+#!/bin/bash
+
+# Print $1 in green
+green () {
+    echo -e "\e[32m$1\e[0m"
+}
+
+# Print $1 in red
+red () {
+    echo -e "\e[31m$1\e[0m"
+}
+
+assert () {
+    if [ $# -lt 1 ]; then
+        red "ERROR, assert expects some args (the code to run)"
+        exit 1
+    fi
+    /bin/bash -exc '"$@"' bash "$@"
+    ret=$?
+    if [ "$ret" -ne 0 ]; then
+        red "FAILURE, this shell command returned exit status $ret:
+\$ $(printf "'%s' " "$@")\n"
+        exit $ret
+    fi
+    echo
+}
+
+###############################################################################
+
+assert emacs --version
+
+srcdir=$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && cd .. && pwd )
+rootdir=$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )
+
+# form="(message \"OK\")"
+form="(progn (add-to-list 'load-path \"$rootdir\") (add-to-list 'load-path \"$srcdir\"))"
+
+assert emacs --batch -l ert --eval "$form" -l init-tests.el -l proof-general.el -l coq-tests.el -f ert-run-tests-batch-and-exit