aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2020-04-09Unplugging previous commit (proof using insertion.Pierre Courtieu
It needs more tweaking when a bloc is asserted at once.
2020-04-09Merge branch 'master' of https://github.com/ProofGeneral/PGPierre Courtieu
2020-04-09Automatic "Proof using" insertion.Pierre Courtieu
When "Suggest Proof Using" is set in coq, coq suggests "Proof using" annotations. We insert these annotation (by default after asking the user).
2020-04-02Rephrase ProofGeneral.texi following PR #476 that fixed #475Erik Martin-Dorel
Note that currently, there is no keybinding associated to the electric terminator.
2020-04-02Merge pull request #476 from dunnl/issue-475Erik Martin-Dorel
Fix documentation about Coq electric terminator Related: #160
2020-04-02Correct documentationLawrence Dunn
2020-04-02Merge pull request #474 from tchajed/add-ltac2-syntaxErik Martin-Dorel
Add support for core Ltac2 syntax
2020-04-02Add support for core Ltac2 syntaxTej Chajed
- Ltac2 definitions, types, and notation - Ltac2 queries - ltac1:(...) and ltac2:(...) antiquotations Closes #473.
2020-04-01SearchAbout is deprecated since 8.5; use Search insteadClément Pit-Claudel
2020-04-01Change "" into nil in argument to appendClément Pit-Claudel
2020-03-26Cleaning previous commit, following @cpitclaudel advices.Pierre Courtieu
2020-03-26Fix #472. Removed -topfile when file name incorrect.Pierre Courtieu
For the record: - "-topfile" option is good so that coqtop understands the name of the current module - but some people want to script coq files with incorrect names without ever comiling them. So we don't add "-topfile" option when it would make coqtop fail. A warning is issued.
2020-03-13Fix 464: proof-autoloads not found by EmacsPierre Courtieu
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 12:42:34 +0000