aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-05-04Merge pull request #486 from ProofGeneral/coq-tests-for-masterErik Martin-Dorel
Coq tests for master
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-04Fixing #485, bug on proof without "Proof".Pierre Courtieu
Due to a re-search that should fail silently.
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-04Fixing #485, bug on proof without "Proof".Pierre Courtieu
Due to a re-search that should fail silently.
2020-05-04refactor: Remove unneeded auxiliary functions & Use "coq-" prefixErik Martin-Dorel
2020-05-04fix: ert.jsonErik Martin-Dorel
* The zone between "Test ... condition:" & "FAILED ..." can have more than 1 line!
2020-05-04fix: Tweak comments and workaround ProofGeneral/PG#485Erik Martin-Dorel
2020-05-04test: Add tests and some fixCyril Anaclet
2020-05-01fix: add some "sudo chown coq:coq" commandErik Martin-Dorel
* This should solve the "(buffer-read-only #<buffer test1.v>)" error, probably due to permission issues.
2020-05-01test: Add ert-problem-matcher for CI workflowErik Martin-Dorel
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-29ci: Build all branches for nowErik Martin-Dorel
TODO: revert this commit before creating a Pull Request
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-27[CI] fail-fast:=falseErik Martin-Dorel
href: https://help.github.com/en/actions/reference/workflow-syntax-for-github-actions#jobsjob_idstrategyfail-fast
2020-04-27[CI] Use coq-community/docker-coq-action@v1Erik Martin-Dorel
2020-04-22[CI] Use erikmd/docker-coq-action@masterErik Martin-Dorel
2020-04-21Merge pull request #483 from ProofGeneral/use-github-actionsErik Martin-Dorel
Use GitHub actions
2020-04-21docs(README.md): Update CI badgeErik Martin-Dorel
2020-04-21[CI] Tweak max-parallel specErik Martin-Dorel
2020-04-21[CI] Fix on/(push,pull_request) specErik Martin-Dorel
2020-04-21s/4.07-flambda/minimal/Erik Martin-Dorel
2020-04-21fix: Install emacs in the Docker containerErik Martin-Dorel
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)
2020-04-16feat: Add GitHub-action workflowErik Martin-Dorel
2020-04-16feat: Remove Travis CI configurationErik Martin-Dorel
2020-04-16Fix hide/show proof.Pierre Courtieu
Bug described by @MdeLv at: https://github.com/coq/coq/issues/12088#issuecomment-613266520
2020-04-15Fix a bug in detection of "Proof." when "proof using" insertionPierre Courtieu
2020-04-15Fixed disabled proof using menu.Pierre Courtieu
2020-04-15add CHANGES entry for vosHendrik Tews
2020-04-15update documentation for vos compilationHendrik Tews
2020-04-15menu entry for coq-compile-vosHendrik Tews
2020-04-15coq-par-compile: support -vos for coq >= 8.11 and default setting changeHendrik Tews
This commit adds support for the new -vos compilation. For coq >= 8.11 only -vos can be used, depending on the config option coq-compile-vos. For coq < 8.11 only -quick/-vio is used, depending on option coq-compile-quick, as before. For a smooth upgrade path, if coq-compile-vos has not been configured, the users intention on whether to use -vos or not for coq >= 8.11 is derived from coq-compile-quick. Some defaults have been changed: - parallel background compilation is the default now in case coq-compile-before-require is enabled. - for coq < 8.11, quick/vio compilation with delayed vio-to-vo conversion is now the default
2020-04-15Span menu entry for proof using annotation + doc.Pierre Courtieu
2020-04-10docs: Update CHANGES after issue #479 and PR #480Erik Martin-Dorel
* Make (coq-insert-intros) conditionnaly insert `move=>` or `intros`
2020-04-10Merge branch 'master' of https://github.com/ProofGeneral/PGPierre Courtieu
2020-04-10Fixed proof using annotation mechanism.Pierre Courtieu
I ended up using (in a slight devious way) the lemma dependency mechanism of PG: the dependency information stored in the span is only the ones suggested by coq: only the one that should appear in theproof using annotation (and only when coq felt the need to suggest them.
2020-04-10Merge pull request #480 from CyrilAnac/masterErik Martin-Dorel
feat(coq-insert-intros): Conditionally insert `move=>` or `intros`
2020-04-10Close #479cyrilzak31
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:46:36 +0000