From e8681a08bbbe19e440ee7c013814229e51195b3e Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Thu, 16 Apr 2020 17:06:27 +0200 Subject: feat: Remove Travis CI configuration --- .travis.yml | 24 ------------------------ Makefile.travis | 30 ------------------------------ 2 files changed, 54 deletions(-) delete mode 100644 .travis.yml delete mode 100644 Makefile.travis 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: -- cgit v1.2.3 From b04949d2c36a1e19c9eb748dd9c342523edf08e5 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Thu, 16 Apr 2020 17:07:08 +0200 Subject: feat: Add GitHub-action workflow --- .github/workflows/test.yml | 40 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 .github/workflows/test.yml diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml new file mode 100644 index 00000000..0cc6027a --- /dev/null +++ b/.github/workflows/test.yml @@ -0,0 +1,40 @@ +name: CI + +on: + push: + branches: + - '**' + pull_request: + branches: + - master + - hybrid + +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: 5 + + steps: + - uses: actions/checkout@v2 + + - uses: purcell/setup-emacs@master + with: + version: ${{ matrix.emacs_version }} + + - run: emacs --version + - run: make -- cgit v1.2.3 From 234d9761212b3e70d538de9704a6bcd29ea684c8 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Thu, 16 Apr 2020 17:34:41 +0200 Subject: chore: Add init-tests.el * Taken from https://github.com/pfitaxel/learn-ocaml.el/blob/master/tests/init-tests.el (under license MIT) --- ci/init-tests.el | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 ci/init-tests.el 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 -- cgit v1.2.3 From 76943f911134863596eb5ca150f7b9c8051eac72 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Thu, 16 Apr 2020 18:02:43 +0200 Subject: chore: Add shell script to automate the tests * Inspired by https://github.com/pfitaxel/learn-ocaml.el/blob/master/test.sh (under license MIT) --- ci/test.sh | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100755 ci/test.sh diff --git a/ci/test.sh b/ci/test.sh new file mode 100755 index 00000000..e9e0b472 --- /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 -l init-tests.el --eval "$form" -l proof-general.el -f ert-run-tests-batch-and-exit -- cgit v1.2.3 From 4849bb7d8c01770e60ff306994e3ef1e7d4a54f1 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Thu, 16 Apr 2020 18:25:05 +0200 Subject: feat: Add first version of coq-tests.el TODO: Expand it using - https://github.com/rejeep/ert-async.el - and/or https://www.gnu.org/software/emacs/manual/html_node/ert/index.html --- ci/coq-tests.el | 139 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ ci/test.sh | 2 +- 2 files changed, 140 insertions(+), 1 deletion(-) create mode 100644 ci/coq-tests.el 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 +;; +;; (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" # nil ("-emacs")) +;; scomint-exec(# "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 # too small for splitting") +;; signal(error ("Window # too small for splitting")) +;; error("Window %s too small for splitting" #) +;; split-window(nil nil) +;; split-window-vertically() +;; proof-safe-split-window-vertically() +;; proof-select-three-b(nil # # 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 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/test.sh b/ci/test.sh index e9e0b472..661f8f7a 100755 --- a/ci/test.sh +++ b/ci/test.sh @@ -35,4 +35,4 @@ 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 -l init-tests.el --eval "$form" -l proof-general.el -f ert-run-tests-batch-and-exit +assert emacs --batch -l ert -l init-tests.el --eval "$form" -l proof-general.el -l coq-tests.el -f ert-run-tests-batch-and-exit -- cgit v1.2.3 From 41d1750be0c45b51eb4e91ba4832c50a20e5fc2d Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Fri, 17 Apr 2020 08:25:13 +0200 Subject: feat: Update test.yml to trigger integration tests * Fix test.sh so it can be run from the parent dir --- .github/workflows/test.yml | 41 +++++++++++++++++++++++++++++++++++++++++ ci/test.sh | 2 +- 2 files changed, 42 insertions(+), 1 deletion(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 0cc6027a..e695f435 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -38,3 +38,44 @@ jobs: - 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: + - 4.07-flambda + # 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: 5 + + steps: + - uses: actions/checkout@v2 + + - uses: purcell/setup-emacs@master + with: + version: ${{ matrix.emacs_version }} + + - 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 Run tests + ./ci/test.sh + endGroup diff --git a/ci/test.sh b/ci/test.sh index 661f8f7a..b29d5af7 100755 --- a/ci/test.sh +++ b/ci/test.sh @@ -35,4 +35,4 @@ 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 -l init-tests.el --eval "$form" -l proof-general.el -l coq-tests.el -f ert-run-tests-batch-and-exit +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 -- cgit v1.2.3 From 57f671eecb186f827ef14c4e3fc8a4debb99435c Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Fri, 17 Apr 2020 08:49:51 +0200 Subject: fix: Install emacs in the Docker container --- .github/workflows/test.yml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index e695f435..45274d89 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -44,11 +44,11 @@ jobs: strategy: matrix: - emacs_version: + # emacs_version: # the emacs version in Ubuntu 18.04 LTS - - 25.2 + # - 25.2 # the emacs version in Debian Buster - - 26.1 + # - 26.1 # the emacs version in Debian Sid # - 26.3 coq_version: @@ -62,10 +62,6 @@ jobs: steps: - uses: actions/checkout@v2 - - uses: purcell/setup-emacs@master - with: - version: ${{ matrix.emacs_version }} - - uses: erikmd/docker-coq-action@alpha id: docker-coq-action with: @@ -76,6 +72,10 @@ jobs: 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 -- cgit v1.2.3 From e92d151dcbe12e5294d710755a2c9e1b38794be7 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Tue, 21 Apr 2020 15:25:40 +0200 Subject: s/4.07-flambda/minimal/ --- .github/workflows/test.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 45274d89..5821b748 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -54,7 +54,7 @@ jobs: coq_version: - 8.11 ocaml_version: - - 4.07-flambda + - 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: 5 -- cgit v1.2.3 From 7131fc5d2f8bea9f6a1f3c3823b9236fcfd4687b Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Tue, 21 Apr 2020 21:49:52 +0200 Subject: [CI] Fix on/(push,pull_request) spec --- .github/workflows/test.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 5821b748..7196d3d8 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -2,12 +2,12 @@ name: CI on: push: - branches: - - '**' - pull_request: branches: - master - hybrid + pull_request: + branches: + - '**' jobs: build: -- cgit v1.2.3 From 3ce80c44f2d95fa7d2d6547129511fb1b6beca84 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Tue, 21 Apr 2020 21:52:29 +0200 Subject: [CI] Tweak max-parallel spec --- .github/workflows/test.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 7196d3d8..4b4bf8ec 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -27,7 +27,7 @@ jobs: - 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: 5 + max-parallel: 4 steps: - uses: actions/checkout@v2 @@ -57,7 +57,7 @@ jobs: - 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: 5 + max-parallel: 6 steps: - uses: actions/checkout@v2 -- cgit v1.2.3 From 2346bbafa9dcefe5ed344e758c399e1507817b43 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Tue, 21 Apr 2020 22:01:43 +0200 Subject: docs(README.md): Update CI badge --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- cgit v1.2.3