aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2020-06-04New hook for early prompt/output analyzis.Pierre Courtieu
proof-state-change-pre-hook happens earlier than proof-state-change-hook, i.e. before proof-done-advancing. This should be used to register information in the currently processed span before proof-done-advancing classifies it. Historically PG design was to gather these information during proof-done-advancing (or in its hook called at the end) by just looking at the command statement. But it is often useful to look at the output (messages and/or prompt) to gather more accurate information. Some of this information may be needed DURING proof-done-advancing. Hence this early hook.
2020-05-29Merge pull request #490 from ProofGeneral/feature/487Erik Martin-Dorel
Improve PG support of Show Proof (Diffs): Display the proof terms stepwise in the *response* buffer. Close #487
2020-05-29refactor: Remove unneeded coq-should-responseErik Martin-Dorel
2020-05-29Minor changesAnaclet
2020-05-29Fix the test 081Anaclet
2020-05-29Add tests and flags systemAnaclet
2020-05-29fix: backtrack for "Show Proof" disabledAnaclet
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-07 16:42:59 +0000