ProofGeneral/PG issues and pull requests

#707 - confusing error on incorrect _CoqProject file

Issue - State: closed - Opened by gasche over 1 year ago

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

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

#702 - Automatic indenting for Easycrypt

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

#701 - Merging the Abella fork of PG

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

#696 - Omit let fix

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

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

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

#691 - add tests for recent omit-proofs issues

Pull Request - State: closed - Opened by hendriktews almost 2 years ago - 1 comment
Labels: kind: test

#690 - PG incorrectly interprets `}.` as a single token, which results in incorrectly accepting files that coqc rejects

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

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

Issue - State: closed - Opened by Blaisorblade about 2 years ago - 14 comments

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

Issue - State: closed - Opened by RalfJung about 2 years ago - 14 comments
Labels: needs: documentation, issue: upstream

#686 - Tons of warnings when using certain PG features

Issue - State: open - Opened by RalfJung about 2 years ago - 12 comments

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

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

#663 - Adding QRHL-tool in the CHANGES file.

Pull Request - State: closed - Opened by Matafou over 2 years ago - 2 comments
Labels: kind: documentation

#660 - update CHANGES file

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

#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 about 3 years ago - 1 comment

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

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

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

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

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

Issue - State: closed - Opened by samuelgruetter over 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 almost 4 years ago - 1 comment

#552 - protect uses of coq-callcoq

Pull Request - State: closed - Opened by hendriktews almost 4 years ago
Labels: kind: fix

#540 - add Coq compile test for a delayed require

Pull Request - State: closed - Opened by hendriktews about 4 years ago

#536 - make-temp-file without text argument for emacs 25

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

#532 - Compile tests

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

#526 - fix coq-callcoq for emacs 27

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

#503 - coq-par-compile: use hash for ancestors

Pull Request - State: closed - Opened by hendriktews over 4 years ago - 5 comments
Labels: kind: fix, part: coq-compile

#478 - coq-par-compile: support -vos for coq >= 8.11 and default setting change

Pull Request - State: closed - Opened by hendriktews almost 5 years ago - 9 comments

#452 - Generic monadic indentation + specifically ext-lib / Compcert + doc.

Pull Request - State: closed - Opened by Matafou about 5 years ago - 4 comments

#445 - Uncommented coq-find-comment-start, coq-find-comment-end as quick fix…

Pull Request - State: closed - Opened by vzaliva about 5 years ago - 1 comment
Labels: pg: proof-shell, kind: fix

#439 - Prooftree updates

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

#438 - coq-par-compile: fix 8.10 -schedule-vio2vo incompatibility

Pull Request - State: closed - Opened by hendriktews over 5 years ago - 3 comments
Labels: kind: fix, part: coq-compile

#437 - Coq PG doesn't recognize the new quotation mechanism of coq/coq#9733

Issue - State: open - Opened by pi8027 over 5 years ago - 8 comments

#432 - fix coqtags that can't find some theorem and output empty definition

Pull Request - State: closed - Opened by fuyu0425 over 5 years ago - 1 comment

#392 - Syntax of `-arg` in `_CoqProject`

Issue - State: open - Opened by herbelin over 6 years ago - 13 comments

#100 - coq-end-Section should handle Modules and Module Types

Issue - State: open - Opened by tchajed over 8 years ago

#99 - Set Implicit Arguments is out of place in the options menu

Issue - State: closed - Opened by tchajed over 8 years ago - 3 comments

#98 - Ensure PG overlays have pg-span property

Pull Request - State: closed - Opened by tchajed over 8 years ago - 7 comments

#97 - Retracting to a point with multiple overlays fails

Issue - State: closed - Opened by tchajed over 8 years ago - 6 comments

#96 - coq-compile-before-require issue with Coq's command Add LoadPath

Issue - State: open - Opened by jonleivent over 8 years ago - 21 comments

#95 - Add Reserved Infix like Reserved Notation

Pull Request - State: closed - Opened by JasonGross over 8 years ago - 1 comment

#94 - some idtac output printed multiple times

Issue - State: open - Opened by jonleivent over 8 years ago - 1 comment

#93 - cannot use PG with trunk version of coq: Invalid version syntax: 'trunk'

Issue - State: closed - Opened by jonleivent over 8 years ago - 3 comments

#92 - Compile before require from current directory failing with 8.5

Issue - State: closed - Opened by YaZko over 8 years ago - 15 comments

#91 - Ltac redefs (::=) are not indented properly

Issue - State: closed - Opened by jonleivent over 8 years ago - 2 comments

#90 - idtac output is getting parsed by PG as commands

Issue - State: closed - Opened by jonleivent over 8 years ago - 5 comments
Labels: resolved: duplicate

#89 - PG not compiling with emacs 24.4

Issue - State: closed - Opened by b1rd1e over 8 years ago - 9 comments

#88 - Fix inforef references to the emacs manual.

Pull Request - State: closed - Opened by yuvallanger over 8 years ago - 1 comment

#87 - Fix (next-undo-elt) to return a relevant undo element w.r.t (undo-delta)

Pull Request - State: closed - Opened by erikmd over 8 years ago - 1 comment

#86 - `proof-prog-name-ask` interacts poorly with tab-completion (especially on Windows)

Issue - State: open - Opened by JasonGross over 8 years ago - 4 comments

#85 - Highlight Existing Class like Existing Instance

Pull Request - State: closed - Opened by JasonGross over 8 years ago - 1 comment

#84 - Highlight [nra] like [nia] and [lia] and [lra]

Pull Request - State: closed - Opened by JasonGross over 8 years ago - 1 comment

#83 - Stuck with proof of software foundations.

Issue - State: closed - Opened by mukeshtiwari over 8 years ago - 9 comments

#82 - enhancement: easy way to colorize solution tactics that have some common regexp.

Issue - State: closed - Opened by jonleivent over 8 years ago - 4 comments

#81 - Existing Class is not completely colorized

Issue - State: closed - Opened by jonleivent over 8 years ago

#80 - Strange indentation bug in Emacs master

Issue - State: closed - Opened by cpitclaudel over 8 years ago - 2 comments

#79 - coq-load-path docs: norec -> nonrec

Pull Request - State: closed - Opened by tbrk over 8 years ago - 8 comments

#78 - Color lia, romega, nia, psatz, nsatz, lra

Pull Request - State: closed - Opened by JasonGross over 8 years ago - 6 comments

#77 - `lia`, `romega`, `nia`, `psatz`, `nsatz`, `lra` should all be colored like `omega` and `reflexivity`

Issue - State: closed - Opened by JasonGross over 8 years ago - 1 comment

#76 - Why do we call proof-locate-executable on coq-prog-name (et al)?

Issue - State: closed - Opened by cpitclaudel almost 9 years ago - 7 comments

#75 - Library more.v is required

Issue - State: closed - Opened by YaZko almost 9 years ago - 7 comments

#74 - Free variable smie--parent

Issue - State: open - Opened by psteckler almost 9 years ago - 3 comments

#73 - `Combined Scheme` should be highlighted

Issue - State: open - Opened by JasonGross almost 9 years ago - 10 comments

#72 - `Include` should be highlighted

Issue - State: closed - Opened by JasonGross almost 9 years ago - 1 comment

#71 - Destructuring let breaks coq-Check et al.'s default suggestion

Issue - State: closed - Opened by wilcoxjay almost 9 years ago - 13 comments

#70 - Coq trunk + compile before require => « Invalid version syntax: 'trunk' »

Issue - State: closed - Opened by aspiwack almost 9 years ago - 12 comments

#69 - Coq compilation assumes that coqdep only returns .vo files

Issue - State: closed - Opened by cpitclaudel almost 9 years ago - 1 comment

#68 - Respect user settings in coq-insert-intros

Pull Request - State: closed - Opened by cpitclaudel almost 9 years ago - 4 comments

#67 - intros! ignores some of ProofGeneral settings

Issue - State: closed - Opened by cpitclaudel almost 9 years ago

#66 - ProofGenerar don't work with Isabelle2015 or higher

Issue - State: closed - Opened by KeenS almost 9 years ago - 1 comment

#65 - proof-extend-queue: Wrong type argument: overlayp, nil

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

#64 - Paragraph filling is no longer working

Issue - State: closed - Opened by jwiegley almost 9 years ago - 6 comments

#63 - weird delay

Issue - State: closed - Opened by lczch almost 9 years ago - 12 comments
Labels: resolved: wontfix

#62 - Time Command + bullets = PG hangs

Issue - State: closed - Opened by jonleivent almost 9 years ago - 2 comments

#61 - PG does not compile

Issue - State: closed - Opened by JasonGross almost 9 years ago - 2 comments

#60 - change coq-prog-name from _CoqProject

Issue - State: closed - Opened by SimonBoulier almost 9 years ago - 23 comments

#59 - Highlight ltac:(), constr:(), and uconstr:()

Pull Request - State: closed - Opened by cpitclaudel almost 9 years ago - 1 comment

#58 - Statement splitting incorrect in the presence of some notation

Issue - State: open - Opened by RalfJung almost 9 years ago - 9 comments
Labels: kind: enhancement, help wanted, resolved: wontfix

#57 - Errors encountered when a Compile Before Require fails

Issue - State: closed - Opened by YaZko almost 9 years ago - 4 comments
Labels: resolved: duplicate

#56 - Proof General automatically resizes goals/response windows between proof steps

Issue - State: closed - Opened by sdconsta almost 9 years ago - 15 comments

#55 - (Some) Imports from Coq standard library make the background compilation fail

Issue - State: closed - Opened by RalfJung about 9 years ago - 18 comments

#54 - Buffer coq-compile-response sometimes takes over the whole window

Issue - State: open - Opened by RalfJung about 9 years ago - 19 comments
Labels: resolved: duplicate

#53 - Electric terminator and newlines

Issue - State: open - Opened by OndrejSlamecka about 9 years ago - 5 comments

#52 - Edit Abbrevs broken?

Issue - State: open - Opened by SimonBoulier about 9 years ago - 2 comments

#51 - Support ssreflect-style indentation

Issue - State: open - Opened by ejgallego about 9 years ago - 10 comments

#50 - Implement support for "From ... Require ..."

Pull Request - State: closed - Opened by RalfJung about 9 years ago - 5 comments

#49 - Automatic compliation of dependencies does not work with Coq 8.5's "From ... Require Import..."

Issue - State: closed - Opened by RalfJung about 9 years ago - 4 comments

#48 - Update numbering flag passed to texi2html

Pull Request - State: closed - Opened by tchajed about 9 years ago

#47 - lazymatch with bullets confuses C-M-f

Issue - State: closed - Opened by cpitclaudel about 9 years ago - 3 comments

#46 - Failure while processing imports

Issue - State: closed - Opened by YaZko about 9 years ago - 7 comments

#45 - "Use project file" option does not work

Issue - State: open - Opened by vzaliva about 9 years ago - 4 comments

#44 - EasyCrypt PG mode

Pull Request - State: closed - Opened by strub about 9 years ago - 8 comments
Labels: kind: enhancement

#43 - easycrypt

Issue - State: closed - Opened by spitters about 9 years ago - 31 comments
Labels: kind: enhancement

#42 - Failed on-the-fly compilation dedicates goals window to compilation error message, confusing PG

Issue - State: closed - Opened by cpitclaudel about 9 years ago - 5 comments
Labels: resolved: duplicate

#41 - query-replace inside the processed region selects the first match, rather than the next one

Issue - State: closed - Opened by JasonGross about 9 years ago - 3 comments

#40 - basic proof tree changes for Coq 8.5

Pull Request - State: closed - Opened by hendriktews about 9 years ago - 4 comments
Labels: kind: enhancement

#39 - Undo does not revert the processed region

Issue - State: closed - Opened by JasonGross about 9 years ago - 26 comments

#38 - More commands are not highlighted

Issue - State: closed - Opened by JasonGross about 9 years ago - 8 comments

GitHub / ProofGeneral/PG issues and pull requests