aboutsummaryrefslogtreecommitdiff
path: root/ci
AgeCommit message (Collapse)Author
2021-04-16fix omit proofs test for emacs <= 25Hendrik Tews
Work around the wrong order returned by `overlays-at' in Emacs <= 25.
2021-04-16add test for omit proofs featureHendrik Tews
2021-02-22protect uses of coq-callcoqHendrik Tews
Uses of coq-callcoq need to correctly handle nil as result for the case that coq-callcoq fails. Additionally, add a regression test. Fixes #551
2021-01-10add Coq compile test for a delayed requireHendrik Tews
2020-12-19ensure vo compilation for tests, increase parallelism, more config outputHendrik Tews
2020-12-19reimplement functions not present in earlier emacs versionsHendrik Tews
2020-12-19include compile tests in CI elisp compilationHendrik Tews
2020-12-19fix 2 background compilation bugs for a dependency in state readyHendrik Tews
2020-12-19add auto compile test to trigger two bugs for dependees in state readyHendrik Tews
See also the committed test.el. The test is not completely robust, it needs to be improved in the future.
2020-12-19add test for recompilation with changesHendrik Tews
2020-12-19add tests for parallel background compilationHendrik Tews
2020-12-06refactor: Simplify ci/init-tests.elErik Martin-Dorel
2020-12-06fix: Workaround DebBug 34341 (fixed in Emacs 26.3, 27.1)Erik Martin-Dorel
* This patch should hopefully fix ProofGeneral CI tests. href: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=34341 href: https://github.com/coq/coq/issues/12088#issuecomment-613522676
2020-05-29refactor: Remove unneeded coq-should-responseErik Martin-Dorel
2020-05-29Minor changesAnaclet
2020-05-29Fix the test 081Anaclet
2020-05-29Add tests and flags systemAnaclet
2020-05-29test: Add regression test (currently failing)Erik Martin-Dorel
2020-05-26fix: test files should not provide featuresErik Martin-Dorel
Close #493
2020-05-04docs: Add a comment in ci/test_wholefile.vErik Martin-Dorel
* see also https://github.com/ProofGeneral/PG/issues/485
2020-05-04add testCyril Anaclet
2020-05-04refactor: Rename test fileErik Martin-Dorel
2020-05-04test: Remove "Proof." workaroundErik Martin-Dorel
2020-05-04docs: Add docstrings in testsErik Martin-Dorel
2020-05-04refactor: Remove unneeded auxiliary functions & Use "coq-" prefixErik Martin-Dorel
2020-05-04fix: Tweak comments and workaround ProofGeneral/PG#485Erik Martin-Dorel
2020-05-04test: Add tests and some fixCyril Anaclet
2020-05-01test: Slightly increase 'ert-batch-backtrace-right-marginErik Martin-Dorel
2020-04-30[WIP] add 2 testsCyril Anaclet
2020-04-29fix: ERT tests OK in batch & interactive mode at onceErik Martin-Dorel
2020-04-29fix: coq-tests.el and related filesErik Martin-Dorel
* The "./test1.v" relative filename triggered an issue => use (coq-test-full-path "test1.v") * The (coq-test-cmd "...") was not optimal for coq-test-print => use (progn (coq-test-goto-before "(*some-unique-identifier*)") (proof-goto-point) (proof-shell-wait)) * The (string-trim "...") function was not defined in batch mode => use (require 'subr-x) & Remove forgotten "(setq temp" snippet.
2020-04-29fix(test.sh): $_dir namingErik Martin-Dorel
2020-04-29Add ERT tests (WIP)Cyril Anaclet
Co-authored-by: Cyril Anaclet <cyril.anaclet@gmail.com> Co-authored-by: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
2020-04-29Add a testCyril Anaclet
2020-04-17feat: Update test.yml to trigger integration testsErik Martin-Dorel
* Fix test.sh so it can be run from the parent dir
2020-04-17feat: Add first version of coq-tests.elErik Martin-Dorel
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
2020-04-17chore: Add shell script to automate the testsErik Martin-Dorel
* Inspired by https://github.com/pfitaxel/learn-ocaml.el/blob/master/test.sh (under license MIT)
2020-04-16chore: Add init-tests.elErik Martin-Dorel
* Taken from https://github.com/pfitaxel/learn-ocaml.el/blob/master/tests/init-tests.el (under license MIT)