aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-05-29fix: backtrack wrong type argumentAnaclet
2020-05-29fix: Do "Show Proof…" (with "?Goal") as soon as the proof is startedErik Martin-Dorel
2020-05-29test: Add regression test (currently failing)Erik Martin-Dorel
2020-05-29Apply reviews of @erikmdCyril Anaclet
2020-05-29WIP for #487Cyril Anaclet
2020-05-29Fix name clash & rephrase some stringsErik Martin-Dorel
2020-05-29All case for Show and regex variableCyril Anaclet
2020-05-29First try for feature #487Cyril Anaclet
2020-05-28Merge pull request #496Erik Martin-Dorel
fix: test files should not provide features Fix #493 further
2020-05-28Added a few coq commands.Pierre Courtieu
2020-05-28fix: test files should not provide featuresErik Martin-Dorel
href: https://github.com/ProofGeneral/PG/issues/493#issuecomment-634493988
2020-05-28Fix default value for proof-shell-last-cmd-left-goals-p.Pierre Courtieu
This variable was still not used anywhere, but will soon.
2020-05-27Add proof-shell-last-cmd-left-goals-p.Pierre Courtieu
Prover specific analyzis of the last prompt/output to determine if there are open goals left.
2020-05-26[CI] Also run integration tests with Coq 8.9.1 and 8.10.2Erik Martin-Dorel
href: https://github.com/coq-community/docker-coq/wiki#supported-tags
2020-05-26fix: test files should not provide featuresErik Martin-Dorel
Close #493
2020-05-06Merge pull request #488 from Flupp/doc-info-menu-fixErik Martin-Dorel
doc/ProofGeneral.texi: fix makeinfo
2020-05-06test: Add CI step to build the docErik Martin-Dorel
* Only build the info manual. * Otherwise we would get the following issue: $ texi2pdf PG-adapting.texi You don't have a working TeX binary (tex) installed anywhere in your PATH, and texi2dvi cannot proceed without one. If you want to use this script, you'll need to install TeX (if you don't have it) or change your PATH or TEX environment variable (if you do). See the --help output for more details. For information about obtaining TeX, please see http://tug.org/texlive, Makefile.doc:50: recipe for target 'PG-adapting.pdf' failed or do a web search for TeX and your operating system or distro. On Debian you can install a working TeX system with apt-get install texlive
2020-05-06doc/ProofGeneral.texi: fix makeinfoToni Dietze
Fixes the following error: node `Coq Proof General' lacks menu item for `Proof using annotations' despite being its Up target
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 12:12:15 +0000