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

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

Pull Request - State: open - Opened by Matafou 12 days ago - 7 comments
Labels: kind: fix, part: indentation

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

Pull Request - State: open - Opened by Matafou 13 days ago

#787 - CI: add Coq 8.20

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

#786 - Warnings with emacs 29.3

Issue - State: closed - Opened by fblanqui 18 days ago - 2 comments

#785 - Coq: make printing parentheses flag accessible

Pull Request - State: closed - Opened by hendriktews 20 days ago - 16 comments

#784 - Change _CoqProject separator settings

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

#783 - EasyCrypt: add `ecall` keyword

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

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

Pull Request - State: closed - Opened by Matafou 2 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 2 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 3 months ago - 2 comments

#779 - REGRESSION: ProofGeneral cannot step over Fail correctly

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

#778 - CI: add Coq 8.20+rc1

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

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

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

#776 - Update Makefile

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

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

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

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

Issue - State: closed - Opened by erikmd 3 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 3 months ago - 5 comments
Labels: kind: enhancement, kind: test

#771 - Incompatibility with `package-quickstart`

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

#770 - Why retracting before restarting coqtop?

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

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

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

#768 - Reduce splash time to 1s.

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

#767 - DONT MERGE - test strange CI behavior

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

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

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

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

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

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

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

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

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

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

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

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

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

#759 - proof-shell: indentation fix

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

#758 - add more tests for goals and response buffer

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

#757 - Indentation issue : "\in"

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

#756 - different styles of comment

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

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

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

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

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

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

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

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

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

#748 - coq: clear goals buffer after admitted

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

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

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

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

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

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

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

#744 - CI: test 8.19.1 instead of 8.19.0

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

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

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

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

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

#741 - Adding unicode arrow >->

Pull Request - State: closed - Opened by hoheinzollern 7 months ago - 1 comment

#739 - proof-shell: document call graph

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

#738 - dynamic highlighting

Issue - State: closed - Opened by ElifUskuplu 7 months ago - 1 comment

#737 - Avoid evaluating void variables

Pull Request - State: open - Opened by haselwarter 7 months ago - 1 comment

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

Issue - State: open - Opened by hendriktews 7 months ago - 1 comment

#734 - void function error

Issue - State: open - Opened by ZHANGTIANYAO1 8 months ago

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

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

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

Issue - State: closed - Opened by aa755 8 months ago - 1 comment

#730 - Emacs 29.2 in CI

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

#729 - cipg - automated CI maintenance

Pull Request - State: closed - Opened by hendriktews 8 months ago - 2 comments
Labels: kind: documentation, kind: infrastructure

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

Issue - State: closed - Opened by aa755 8 months ago - 2 comments

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

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

#726 - remove executable rights from .el files

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

#725 - texinfo manuals: fix obsolete @inforef

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

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

Issue - State: closed - Opened by RalfJung 9 months ago - 13 comments

#723 - reliably detect coqdep errors for 8.19

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

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

Issue - State: closed - Opened by hendriktews 9 months ago - 4 comments

#721 - makeinfo reports warning: @inforef is obsolete

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

#720 - Fix typos

Pull Request - State: closed - Opened by pitmonticone 9 months ago - 1 comment

#719 - test_wholefile.v incompatible with 8.19

Issue - State: open - Opened by hendriktews 9 months ago - 4 comments
Labels: kind: bug, kind: test

#718 - CI: update for Coq 8.19+rc1

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

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

Pull Request - State: closed - Opened by ayanamists 10 months ago - 7 comments

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

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

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

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

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

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

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

Issue - State: closed - Opened by vzaliva 12 months ago - 1 comment

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

Pull Request - State: closed - Opened by gasche 12 months ago - 2 comments

#707 - confusing error on incorrect _CoqProject file

Issue - State: closed - Opened by gasche 12 months ago

#704 - generic/pg-goals.el shouldn't be executable

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

#702 - Automatic indenting for Easycrypt

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

#701 - Merging the Abella fork of PG

Issue - State: open - Opened by phikal about 1 year ago - 11 comments

#696 - Omit let fix

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

#694 - omit-proofs: handle commands that may have global effects

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

#688 - "Omit proofs" breaks other proofs because it also skips hints

Issue - State: closed - Opened by Blaisorblade over 1 year ago - 14 comments

#687 - "Omit proof" on a Let in a section leads to warning

Issue - State: closed - Opened by RalfJung over 1 year ago - 14 comments
Labels: needs: documentation, issue: upstream

#686 - Tons of warnings when using certain PG features

Issue - State: open - Opened by RalfJung over 1 year ago - 12 comments

#679 - Fixed an error when `proof-ignore-for-undo-count` is a function.

Pull Request - State: open - Opened by rssoc almost 2 years ago

#656 - coq: make ProofGeneral/Coq opam-mode aware

Pull Request - State: closed - Opened by hendriktews over 2 years ago - 2 comments

#654 - add customizable variables to configure which part of a goal the goal buffer will focus on

Pull Request - State: open - Opened by cipher1024 over 2 years ago - 6 comments
Labels: kind: enhancement

#631 - CI workflow: add Emacs 27.2

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

#622 - do not merge: test coq-emacs container action

Pull Request - State: closed - Opened by hendriktews almost 3 years ago - 4 comments
Labels: kind: infrastructure

#612 - PG goes bananas (accepts any string after `{|`)

Issue - State: closed - Opened by samuelgruetter almost 3 years ago - 3 comments

#592 - PG accepts `}.` but `coqc` doesn't

Issue - State: closed - Opened by samuelgruetter about 3 years ago - 2 comments

#586 - Test that the Proof General prelude is correct

Pull Request - State: closed - Opened by hendriktews over 3 years ago - 2 comments
Labels: kind: test

#585 - add tests for checking that goals are correctly shown

Pull Request - State: closed - Opened by hendriktews over 3 years ago - 2 comments

#577 - coq-par-compile: use doubly graph to unlock ancestors efficiently

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

#552 - protect uses of coq-callcoq

Pull Request - State: closed - Opened by hendriktews over 3 years ago
Labels: kind: fix

#540 - add Coq compile test for a delayed require

Pull Request - State: closed - Opened by hendriktews over 3 years ago