aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-02-25test: Add Emacs 27.1 & Remove Emacs 24.3, 24.4 CI testsErik Martin-Dorel
* Document (in README.md) the proposed policy: supporting Emacsen from the versions packaged in Debian Stable / Ubuntu LTS until their EOS.
2021-02-13Update README.mdJulin S
Fix a tiny typo
2021-02-13update magical documentation in manual for vok featureHendrik Tews
2021-02-13update changes and documentation for vok featureHendrik Tews
2021-02-13improve/fix code documentation for vok processingHendrik Tews
2021-02-13add second stage -vok for Coq >= 8.11Hendrik Tews
New value vos-and-vok for coq-compile-vos customization option, existing value vos stands now for vos-no-vok. The implementation uses the existing vio2vo infrastructure with symbols vok and vio2vo. Documentation is still missing.
2021-02-13generalize vio2vo symbol names for vok compilationHendrik Tews
In functions, variables and symbols vio2vo is replaced with second-stage to accommodate for vok compilation. For backward compatibility, the options coq-compile-vio2vo-delay and coq-max-background-vio2vo-percentage are kept. They provide default values for their renamed counterparts, if they have been set manually or through the customization system. Documentation has only been marked but not updated yet.
2021-02-13new github action for make magicHendrik Tews
This action checks that - make -C doc magic works - the manual is currently up-to-date The second check fails when somebody changes variable or function documentation of something that appears in one of the manuals without updating the manuals at the same time. Further, it fails when emacs changes such that the function `texi-docstring-magic' produces different output.
2021-01-31update manuals with make magicHendrik Tews
2021-01-31fix typos and unicode single quotations in doc stringsHendrik Tews
Backported those typos that were fixed only in the manual texi sources and not in the doc strings, from which the text was imported. Convert a few symbols quoted with curved unicode single quotations to ascii, such that make magic recognizes them.
2021-01-31report arguments for closures with make magicHendrik Tews
Switching to lexical scope and emacs using closure (instead of lambda) broke argument printing with make magic.
2021-01-31fix make magic problem with emacs 26 and olderHendrik Tews
Set text quoting style to get doc strings without unicode single quotation marks to keep the regular expressions in texi-docstring-magic working.
2021-01-31fix another make magic problem from 2018Hendrik Tews
In 7389d43893569ff0e1eff892254901876fc8225e proof-ready-for-assistant was moved to proof-script.el, breaking make magic in a complicated chain. The auto load for proof-ready-for-assistant caused proof-script.el to be loaded before proof-assistant was set, causing proof-eval-when-ready-for-assistant, to put stuff into proof-ready-for-assistant-hook. proof-ready-for-assistant loads pg-custom.el by require, therefore, for the first proof assistant in the loop in docstring-magic everything was defined when executing the hooks at the end of proof-ready-for-assistant. The second assistant caused errors than. Fixes #542
2021-01-31fix make magic problem from 2018Hendrik Tews
this problem was introduced in a921439a4eb5b0d96182748e779c78e2f6a41a5f
2021-01-31fix make magic problem from 2017Hendrik Tews
After 574b09 92e3cb4b7a4ad88400b9a5ab0198a96ca5, make magic fails with a recursive require chain. No requires were changed in that commit, it's unclear to me, why there is no recursive require chain with (eval-when (compile).
2021-01-15Preventive support of "goal instead of "subgoal" in coq messages.Pierre Courtieu
Coq team is currently considering changing all messages containing "subgoal[s]" into "goal[s]". This commit allows for both. I make this change as early as possible, even if this chage may not land in coq's master, so that we support this as early as possible. I don't see how this could break anything but again the earliest the best.
2021-01-10add Coq compile test for a delayed requireHendrik Tews
2020-12-26make-temp-file without text argument for emacs 25Hendrik Tews
fixes #534
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-19enable coq background compilation tests in github CIHendrik Tews
extend the github workflow to additionally run the tests in ci/compile-tests
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-19fix keep-going when dependency exists but failedHendrik Tews
2020-12-19redesign of parallel background compilation without clonesHendrik Tews
- no clones any more, existing jobs are directly linked - the whole require command is processed by coqdep to determine the required files, this fixes #352 - the require commands are a separate kind of jobs, because they do not need to get compiled - queue items are only stored in require jobs and file jobs can not have a queue dependency, this simplifies the logic
2020-12-10Merge pull request #527 from rgrinberg/fix-byte-compClément Pit-Claudel
Fix byte compilation in Doom Emacs
2020-12-07Merge pull request #526 from hendriktews/version-break-525hendriktews
fix coq-callcoq for emacs 27
2020-12-07protect coq-callcoq against escaping signalsHendrik Tews
This hopefully fixes compilation without coqtop and especially the github tests.
2020-12-07fix coq-callcoq for emacs 27Hendrik Tews
Use process-file and omit find-file-name-handler, because process-file takes care of file handlers already. Fixes #525
2020-12-06Merge pull request #530 from ProofGeneral/fix-ciErik Martin-Dorel
Workaround & Document debbug 34341 (fixed in Emacs 26.3, 27.1)
2020-12-06docs: Update README.md accordingly & Mention the URL of the debbugErik Martin-Dorel
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-12-01Fix byte compilationRudi Grinberg
load-file-name is not set to pg's source when compiling from doom-emacs https://github.com/hlissner/doom-emacs/issues/2788 Signed-off-by: Rudi Grinberg <me@rgrinberg.com>
2020-11-19coq: Add highlighting for Hint ModeClément Pit-Claudel
2020-10-16Fix #514 + support for named goal selector.Pierre Courtieu
It was hard to separate this too fixes (same regexps).
2020-10-16Fix #518: "Proof using" mode corrupts "Proof with tac".Pierre Courtieu
2020-10-14Merge pull request #517 from Lysxia/hl-computeClément Pit-Claudel
Highlight Compute
2020-10-14Highlight ComputeLi-yao Xia
2020-09-11fix(coq/coq.el): spelling of "whether" (#512)dymil
2020-09-11fix(CHANGES): spelling of "whether" (#511)dymil
2020-09-11Update PhoX link and add https (#510)dymil
2020-06-23Merge pull request #503 from hendriktews/issue-499-ancestor-appendErik Martin-Dorel
coq-par-compile: use hash for ancestors
2020-06-20Merge pull request #501 from haselwarter/proof-shell-string-match-safeErik Martin-Dorel
Use `proof-shell-string-match-safe` to avoid failing on `nil` regexp
2020-06-19coq-par-compile: use hash for ancestorsHendrik Tews
The hash avoids an exponentially growing number of duplicates in the ancestor collection. Fixes #499
2020-06-18Use `proof-shell-string-match-safe` to avoid failing on `nil` regexpPhilipp G. Haselwarter
Fixes a regression introduced in 22681a3caf2c8f45700585ea74dffbf48bb2ac19. In particular, the Coq module seems to be the only one currently setting `proof-show-proof-diffs-regexp`, causing an error for EasyCrypt.
2020-06-15Add coloration for Ltac2 commandsCyril Anaclet
Close #489
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 00:04:26 +0000