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

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

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

#532 - Compile tests

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

#526 - fix coq-callcoq for emacs 27

Pull Request - State: closed - Opened by hendriktews almost 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 over 4 years ago - 9 comments

#439 - Prooftree updates

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

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

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

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

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

#98 - Ensure PG overlays have pg-span property

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

#97 - Retracting to a point with multiple overlays fails

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

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

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

#95 - Add Reserved Infix like Reserved Notation

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

#94 - some idtac output printed multiple times

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

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

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

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

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

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

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

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

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

#89 - PG not compiling with emacs 24.4

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

#88 - Fix inforef references to the emacs manual.

Pull Request - State: closed - Opened by yuvallanger about 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 about 8 years ago - 1 comment

#85 - Highlight Existing Class like Existing Instance

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

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

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

#83 - Stuck with proof of software foundations.

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

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

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

#81 - Existing Class is not completely colorized

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

#80 - Strange indentation bug in Emacs master

Issue - State: closed - Opened by cpitclaudel about 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

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

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

#75 - Library more.v is required

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

#74 - Free variable smie--parent

Issue - State: open - Opened by psteckler over 8 years ago - 3 comments

#73 - `Combined Scheme` should be highlighted

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

#72 - `Include` should be highlighted

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

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

Issue - State: closed - Opened by wilcoxjay over 8 years ago - 13 comments

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

Issue - State: closed - Opened by aspiwack over 8 years ago - 12 comments

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

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

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

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

#67 - intros! ignores some of ProofGeneral settings

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

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

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

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

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

#64 - Paragraph filling is no longer working

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

#63 - weird delay

Issue - State: closed - Opened by lczch over 8 years ago - 12 comments
Labels: resolved: wontfix

#62 - Time Command + bullets = PG hangs

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

#61 - PG does not compile

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

#60 - change coq-prog-name from _CoqProject

Issue - State: closed - Opened by SimonBoulier over 8 years ago - 23 comments

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

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

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

Issue - State: open - Opened by RalfJung over 8 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 over 8 years ago - 4 comments
Labels: resolved: duplicate

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

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

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

Issue - State: closed - Opened by RalfJung over 8 years ago - 18 comments

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

Issue - State: open - Opened by RalfJung over 8 years ago - 19 comments
Labels: resolved: duplicate

#53 - Electric terminator and newlines

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

#52 - Edit Abbrevs broken?

Issue - State: open - Opened by SimonBoulier over 8 years ago - 2 comments

#51 - Support ssreflect-style indentation

Issue - State: open - Opened by ejgallego over 8 years ago - 10 comments

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

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

#48 - Update numbering flag passed to texi2html

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

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

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

#46 - Failure while processing imports

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

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

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

#44 - EasyCrypt PG mode

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

#43 - easycrypt

Issue - State: closed - Opened by spitters over 8 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 over 8 years ago - 5 comments
Labels: resolved: duplicate

#40 - basic proof tree changes for Coq 8.5

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

#39 - Undo does not revert the processed region

Issue - State: closed - Opened by JasonGross over 8 years ago - 26 comments

#38 - More commands are not highlighted

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

#37 - ProofGeneral incorrectly parses unterminated strings in comments in Coq

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

#36 - Some commands are not highlighted correctly

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

#35 - Do we support narrowing?

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

#34 - ProofGeneral (sometimes?) does not build with Emacs 24.3.1 on Windows

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

#33 - Cyclic dependencies

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

#32 - warning building latest version d3d7622

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

#31 - Should we bind C-c C-j in terminals?

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

#30 - prooftree is broken with 8.5 syntax

Issue - State: closed - Opened by Matafou over 8 years ago - 14 comments

#29 - Indentation is wrong after [exists]

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

#28 - travis.yml for emacs 24.{3,4,5}

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

#27 - Add a .travis.yml file for continuous integration emacs 23, 24

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

#26 - Refactor the project file parsing code

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

#25 - PG gets confused when there is another frame visible at start

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

#24 - Tip of master is broken on Coq 8.4pl*

Issue - State: closed - Opened by JasonGross over 8 years ago - 14 comments

#22 - Fix spurious scrolling of *goals* and *response* buffers

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

#20 - Time Print foo doesn't print foo

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

#19 - Is `proof-shell-invisible-cmd-get-result' broken in Coq 8.5?

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

#18 - compile-before-require does not use _CoqProject options or Makefile

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

#17 - "Setting" menu should we pre-fill string options for all provers

Issue - State: open - Opened by Matafou almost 9 years ago - 5 comments

#16 - cursor is covering up my code when used in the terminal

Issue - State: closed - Opened by adnelson almost 9 years ago - 2 comments
Labels: kind: question

#15 - indentation takes a long time, maybe forever

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

#14 - How does one require proof-shell?

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

#13 - 3 frames mode - get frames to appear at specific positions with specific sizes

Issue - State: open - Opened by jonleivent almost 9 years ago - 4 comments

#12 - Highlighting of evars

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

#11 - We should edit the README

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

#10 - constant msg: "Zero or more than one goals window, guessing window width."

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

#9 - Add *.elc to .gitignore

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

#8 - proofdepth sometimes ends up being nil

Issue - State: open - Opened by cpitclaudel almost 9 years ago - 2 comments

#7 - Request to add keystroke for Coq's "Print Assumptions" command

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