| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-12-19 | fix 2 background compilation bugs for a dependency in state ready | Hendrik Tews | |
| 2020-12-19 | add auto compile test to trigger two bugs for dependees in state ready | Hendrik Tews | |
| See also the committed test.el. The test is not completely robust, it needs to be improved in the future. | |||
| 2020-12-19 | add test for recompilation with changes | Hendrik Tews | |
| 2020-12-19 | add tests for parallel background compilation | Hendrik Tews | |
| 2020-12-06 | refactor: Simplify ci/init-tests.el | Erik Martin-Dorel | |
| 2020-12-06 | fix: 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-29 | refactor: Remove unneeded coq-should-response | Erik Martin-Dorel | |
| 2020-05-29 | Minor changes | Anaclet | |
| 2020-05-29 | Fix the test 081 | Anaclet | |
| 2020-05-29 | Add tests and flags system | Anaclet | |
| 2020-05-29 | test: Add regression test (currently failing) | Erik Martin-Dorel | |
| 2020-05-26 | fix: test files should not provide features | Erik Martin-Dorel | |
| Close #493 | |||
| 2020-05-04 | docs: Add a comment in ci/test_wholefile.v | Erik Martin-Dorel | |
| * see also https://github.com/ProofGeneral/PG/issues/485 | |||
| 2020-05-04 | add test | Cyril Anaclet | |
| 2020-05-04 | refactor: Rename test file | Erik Martin-Dorel | |
| 2020-05-04 | test: Remove "Proof." workaround | Erik Martin-Dorel | |
| 2020-05-04 | docs: Add docstrings in tests | Erik Martin-Dorel | |
| 2020-05-04 | refactor: Remove unneeded auxiliary functions & Use "coq-" prefix | Erik Martin-Dorel | |
| 2020-05-04 | fix: Tweak comments and workaround ProofGeneral/PG#485 | Erik Martin-Dorel | |
| 2020-05-04 | test: Add tests and some fix | Cyril Anaclet | |
| 2020-05-01 | test: Slightly increase 'ert-batch-backtrace-right-margin | Erik Martin-Dorel | |
| 2020-04-30 | [WIP] add 2 tests | Cyril Anaclet | |
| 2020-04-29 | fix: ERT tests OK in batch & interactive mode at once | Erik Martin-Dorel | |
| 2020-04-29 | fix: coq-tests.el and related files | Erik 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-29 | fix(test.sh): $_dir naming | Erik Martin-Dorel | |
| 2020-04-29 | Add 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-29 | Add a test | Cyril Anaclet | |
| 2020-04-17 | feat: Update test.yml to trigger integration tests | Erik Martin-Dorel | |
| * Fix test.sh so it can be run from the parent dir | |||
| 2020-04-17 | feat: Add first version of coq-tests.el | Erik 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-17 | chore: Add shell script to automate the tests | Erik Martin-Dorel | |
| * Inspired by https://github.com/pfitaxel/learn-ocaml.el/blob/master/test.sh (under license MIT) | |||
| 2020-04-16 | chore: Add init-tests.el | Erik Martin-Dorel | |
| * Taken from https://github.com/pfitaxel/learn-ocaml.el/blob/master/tests/init-tests.el (under license MIT) | |||
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |