Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / ProofGeneral/PG issues and pull requests

#810 - CI: add Coq 9.0+rc1

Pull Request - State: open - Opened by hendriktews 23 days ago

#809 - deficiencies when changing processed comments

Issue - State: open - Opened by hendriktews 24 days ago - 1 comment

#808 - CI: new tests for changing and undoing processed comments

Pull Request - State: closed - Opened by hendriktews 25 days ago

#807 - CI: replace Coq 8.20.0 with Coq 8.20.1

Pull Request - State: closed - Opened by hendriktews 28 days ago

#806 - `Print Tables` treated as error

Issue - State: open - Opened by SkySkimmer about 1 month ago - 2 comments

#805 - Subgoal bullet auto completition

Issue - State: open - Opened by yaitskov about 2 months ago

#804 - highlight Guarded command (since Coq 8.16)

Pull Request - State: closed - Opened by yaitskov 3 months ago
Labels: kind: enhancement

#803 - Task: improve/harden the pg-protected-undo function

Issue - State: open - Opened by erikmd 3 months ago - 1 comment

#802 - coq/generic: display empty strings in diagnostic messages

Pull Request - State: closed - Opened by hendriktews 3 months ago

#801 - Library compilation failed

Issue - State: open - Opened by usr345 3 months ago - 11 comments

#800 - undo does not retract when undoing a comment created by comment-dwim

Issue - State: open - Opened by hendriktews 3 months ago - 16 comments

#799 - test that Coq background compilation is not affected by local variables

Pull Request - State: closed - Opened by hendriktews 3 months ago - 1 comment

#798 - Unknown error in process filter

Issue - State: closed - Opened by ElifUskuplu 4 months ago - 16 comments

#797 - (Some) vok compilation seems to ignore `coq-compiler`

Issue - State: closed - Opened by LukeXuan 4 months ago - 7 comments

#794 - PG gets confused by comment in _CoqProject file that involves "-arg"

Issue - State: open - Opened by RalfJung 5 months ago - 1 comment

#793 - proof-shell: Don't ask about killing the proof assistant on exit

Pull Request - State: open - Opened by hendriktews 5 months ago - 3 comments

#792 - CI: add Ubuntu 24 release; delete unused containers

Pull Request - State: closed - Opened by hendriktews 5 months ago

#791 - improve hints on splash; fix quick options saving

Pull Request - State: open - Opened by hendriktews 5 months ago - 4 comments

#789 - Fix #757 indentation of "\in"

Pull Request - State: open - Opened by Matafou 5 months ago - 11 comments
Labels: kind: fix, part: indentation

#788 - Fixing the debug mode (for recent coq verions).

Pull Request - State: open - Opened by Matafou 5 months ago

#787 - CI: add Coq 8.20

Pull Request - State: closed - Opened by hendriktews 6 months ago

#786 - Warnings with emacs 29.3

Issue - State: closed - Opened by fblanqui 6 months ago - 2 comments

#785 - Coq: make printing parentheses flag accessible

Pull Request - State: closed - Opened by hendriktews 6 months ago - 16 comments

#784 - Change _CoqProject separator settings

Pull Request - State: closed - Opened by Columbus240 7 months ago - 2 comments

#783 - EasyCrypt: add `ecall` keyword

Pull Request - State: closed - Opened by ruipedro16 7 months ago

#782 - Fix #781 PG does not position to error.

Pull Request - State: closed - Opened by Matafou 8 months ago - 11 comments
Labels: pg: proof-shell, priority: high, kind: fix

#781 - PG does not position to error

Issue - State: closed - Opened by Matafou 8 months ago - 8 comments
Labels: kind: bug, pg: proof-shell, priority: high

#780 - Fixes #779 regression cannot step Fail correctly.

Pull Request - State: closed - Opened by Matafou 8 months ago - 2 comments

#779 - REGRESSION: ProofGeneral cannot step over Fail correctly

Issue - State: closed - Opened by hendriktews 8 months ago - 10 comments

#778 - CI: add Coq 8.20+rc1

Pull Request - State: closed - Opened by hendriktews 8 months ago

#777 - CI: update to Coq 8.19.2 and Emacs 29.4

Pull Request - State: closed - Opened by hendriktews 8 months ago

#776 - Update Makefile

Pull Request - State: closed - Opened by jgarte 8 months ago

#775 - File mode specification error: (void-variable coq-cmd-force-next-proof-kept)

Issue - State: closed - Opened by DaKnig 8 months ago - 15 comments

#774 - fix(coq.el): (setq proof-shell-strip-crs-from-input nil)

Pull Request - State: closed - Opened by erikmd 8 months ago - 2 comments
Labels: kind: fix

#773 - bug: newlines misparsed as space in string litterals

Issue - State: closed - Opened by erikmd 8 months ago - 10 comments
Labels: kind: bug, pg: proof-shell

#772 - also omit proofs with bullets and braces

Pull Request - State: closed - Opened by hendriktews 8 months ago - 5 comments
Labels: kind: enhancement, kind: test

#771 - Incompatibility with `package-quickstart`

Issue - State: open - Opened by monnier 9 months ago - 7 comments
Labels: kind: bug, kind: fix

#770 - Why retracting before restarting coqtop?

Issue - State: open - Opened by Matafou 9 months ago - 3 comments

#769 - Proof General gets into a state where it doesn't know what + is.

Issue - State: open - Opened by walck 9 months ago - 11 comments

#768 - Reduce splash time to 1s.

Pull Request - State: closed - Opened by Matafou 10 months ago - 6 comments
Labels: kind: enhancement

#767 - DONT MERGE - test strange CI behavior

Pull Request - State: closed - Opened by hendriktews 10 months ago - 1 comment

#766 - CI: update CI config to include Emacs 29.3

Pull Request - State: closed - Opened by hendriktews 10 months ago

#764 - UI and kernel out of sync from aborting tactics?

Issue - State: open - Opened by AndreasLoow 10 months ago - 1 comment

#763 - update Coq ignored extensions and add dired-x compatibility

Pull Request - State: closed - Opened by hendriktews 10 months ago

#762 - Coq: run silently and explicitly Show when necessary - second attempt

Pull Request - State: open - Opened by hendriktews 10 months ago - 8 comments

#761 - fix 3-pane mode for small frame heights

Pull Request - State: closed - Opened by hendriktews 10 months ago - 1 comment

#760 - 3-pane mode broken with small frame heights

Issue - State: closed - Opened by hendriktews 10 months ago

#759 - proof-shell: indentation fix

Pull Request - State: closed - Opened by hendriktews 10 months ago

#758 - add more tests for goals and response buffer

Pull Request - State: closed - Opened by hendriktews 10 months ago

#757 - Indentation issue : "\in"

Issue - State: open - Opened by KimayaBedarkar 11 months ago - 2 comments
Labels: kind: bug, part: indentation

#756 - different styles of comment

Issue - State: open - Opened by ElifUskuplu 11 months ago - 6 comments

#753 - Revert "texi-docstring-magic.el: Fix regression in last change"

Pull Request - State: closed - Opened by hendriktews 11 months ago

#752 - Revert "(texi-docstring-magic-texi-for): Use `help-function-arglist`"

Pull Request - State: closed - Opened by hendriktews 11 months ago - 1 comment

#751 - DON'T MERGE: investigate doc-magic problem in PR #750

Pull Request - State: closed - Opened by hendriktews 11 months ago - 1 comment

#750 - poor PG man's workaround for coq/coq#11479

Pull Request - State: closed - Opened by hendriktews 11 months ago - 9 comments

#749 - ci: fix goals present tests (commit a6bd8185)

Pull Request - State: closed - Opened by hendriktews 11 months ago

#748 - coq: clear goals buffer after admitted

Pull Request - State: closed - Opened by hendriktews 11 months ago

#747 - correctly handle Coq patch levels, improve container deletion

Pull Request - State: closed - Opened by hendriktews 11 months ago

#746 - Bug: Frames in hybrid mode automatically revert to vertical mode

Issue - State: open - Opened by allen-liaoo 11 months ago - 2 comments

#745 - CI: do not artificially restrict parallel test execution

Pull Request - State: closed - Opened by hendriktews 12 months ago

#744 - CI: test 8.19.1 instead of 8.19.0

Pull Request - State: closed - Opened by hendriktews 12 months ago

#743 - coq-tests: fix error introduced by Cyril Anaclet in 0ae25c5a

Pull Request - State: closed - Opened by hendriktews 12 months ago - 2 comments
Labels: kind: fix

#742 - coq: run silently and explicitly Show when necessary

Pull Request - State: closed - Opened by hendriktews 12 months ago - 3 comments

#741 - Adding unicode arrow >->

Pull Request - State: closed - Opened by hoheinzollern almost 1 year ago - 1 comment

#740 - CHANGES: add entry for 9b38f844df79eaf77a64c82d21cfdc70351ccc03

Pull Request - State: closed - Opened by hendriktews about 1 year ago

#739 - proof-shell: document call graph

Pull Request - State: closed - Opened by hendriktews about 1 year ago

#738 - dynamic highlighting

Issue - State: closed - Opened by ElifUskuplu about 1 year ago - 1 comment

#737 - Avoid evaluating void variables

Pull Request - State: open - Opened by haselwarter about 1 year ago - 1 comment

#736 - coq-load-project file should extract META files

Issue - State: open - Opened by hendriktews about 1 year ago - 1 comment

#735 - coq-par-compile: add user options for extra coqc/coqdep arguments

Pull Request - State: closed - Opened by hendriktews about 1 year ago

#734 - void function error

Issue - State: open - Opened by ZHANGTIANYAO1 about 1 year ago

#732 - CI: test 8.19.0 instead of 8.19+rc1

Pull Request - State: closed - Opened by hendriktews about 1 year ago

#731 - wait for proof-goto-point to finish

Issue - State: closed - Opened by aa755 about 1 year ago - 1 comment

#730 - Emacs 29.2 in CI

Pull Request - State: closed - Opened by hendriktews about 1 year ago

#729 - cipg - automated CI maintenance

Pull Request - State: closed - Opened by hendriktews about 1 year ago - 2 comments
Labels: kind: documentation, kind: infrastructure

#728 - proof-goto-point is non-idempotent

Issue - State: closed - Opened by aa755 about 1 year ago - 2 comments

#727 - simple-tests/omit_test: fix Coq sources for 8.19

Pull Request - State: closed - Opened by hendriktews about 1 year ago

#726 - remove executable rights from .el files

Pull Request - State: closed - Opened by hendriktews about 1 year ago - 1 comment

#725 - texinfo manuals: fix obsolete @inforef

Pull Request - State: closed - Opened by hendriktews about 1 year ago - 2 comments

#724 - Build failure when "Compile Before Require" meets imported OCaml plugins

Issue - State: closed - Opened by RalfJung about 1 year ago - 13 comments

#723 - reliably detect coqdep errors for 8.19

Pull Request - State: closed - Opened by hendriktews about 1 year ago - 2 comments

#722 - compile-tests/003-require-error fails sporadically with 8.19-rc1

Issue - State: closed - Opened by hendriktews about 1 year ago - 4 comments

#721 - makeinfo reports warning: @inforef is obsolete

Issue - State: closed - Opened by hendriktews about 1 year ago

#720 - Fix typos

Pull Request - State: closed - Opened by pitmonticone about 1 year ago - 1 comment

#719 - test_wholefile.v incompatible with 8.19

Issue - State: open - Opened by hendriktews about 1 year ago - 4 comments
Labels: kind: bug, kind: test

#718 - CI: update for Coq 8.19+rc1

Pull Request - State: closed - Opened by hendriktews about 1 year ago - 1 comment

#717 - coq/coq-mode.el: Change the definition of 'coq--parent-mode

Pull Request - State: closed - Opened by ayanamists about 1 year ago - 7 comments

#716 - [minor] silence an Emacs warning about above-80-chars docstring

Pull Request - State: closed - Opened by gasche about 1 year ago - 1 comment

#714 - qrhl-test: check translation of \sub

Pull Request - State: closed - Opened by hendriktews over 1 year ago - 1 comment

#712 - ci/doc: document test strategy and the Coq/Emacs release table

Pull Request - State: closed - Opened by hendriktews over 1 year ago - 1 comment

#710 - Compile-before-require setting does not presist

Issue - State: closed - Opened by vzaliva over 1 year ago - 1 comment

#708 - Fix "Bad bounding indices" error on invalid _CoqProject

Pull Request - State: closed - Opened by gasche over 1 year ago - 2 comments