aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:47:01 +0000