diff options
| -rw-r--r-- | .github/workflows/test.yml | 81 | ||||
| -rw-r--r-- | .travis.yml | 24 | ||||
| -rw-r--r-- | Makefile.travis | 30 | ||||
| -rw-r--r-- | README.md | 2 | ||||
| -rw-r--r-- | ci/coq-tests.el | 139 | ||||
| -rw-r--r-- | ci/init-tests.el | 34 | ||||
| -rwxr-xr-x | ci/test.sh | 38 |
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: @@ -1,6 +1,6 @@ # Proof General — Organize your proofs! -[](https://travis-ci.org/ProofGeneral/PG) +[](https://github.com/ProofGeneral/PG/actions?query=workflow%3ACI) [](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 |