Jason Gross

Use module names rather than file names for output

26

Fixes #14 Code adjusted from https://github.com/JasonGross/coq-tools/blob/9b81719a2172e4301126378e5aebf83e3f2b43e6/import_util.py#L99-L111

How do I get identifiers in Coq to link correctly?

4

I'd like to be able to click on an identifier in code to jump to it's definition, and click on modules that are `Require`d to jump to their definition. (For...

Please report file names and line/column numbers on `!! Warning:`

1

I'd like to be able to process them in GH annotations, and this is tricky without knowing what file they come from

autocompletion hangs emacs for unacceptably long

1

If I start typing `Redirect`, and complete that to `Redirect "file" command.`, and then in `file` I start typing `/tmp`, after typing `m`, emacs hangs for at least 10-15 seconds...

It should be easy to [discover how to] disable code folding

4

Code folding is by far the most annoying feature of company-coq for me; I use `TAB` in the middle of a line to indent my code, and sometimes I hit...

code completion should not interrupt search

2

If I do `C-s Goal`, then I get command completion at the first location of `Goal ` in my code; if I keep typing, it ends up in the document,...

Company Coq is sometimes noticeably laggy at obtaining symbols

26

Perhaps this is an instance of "doctor, it hurts when I poke myself". (This is in Coq 8.6) ``` coq Require Import Coq.btauto.Algebra Coq.btauto.Reflect Coq.btauto.Btauto Coq.derive.Derive Coq.extraction.ExtrHaskellBasic Coq.extraction.ExtrHaskellNatNum Coq.extraction.ExtrHaskellNatInt Coq.extraction.ExtrHaskellNatInteger...

Company-Coq is slow at `Require Import` completion when there are a large number ( > 1000) files in the project

2

Here are some debug traces: 1. ``` Debugger entered--Lisp error: (quit) redisplay_internal\ \(C\ function\)() ``` 2. ``` Debugger entered--Lisp error: (quit) redisplay_internal\ \(C\ function\)() ``` 3. ``` Debugger entered--Lisp error:...

company-coq does not stay off when I turn it off

4

When I disable company-coq with `M-x company-coq-mode`, it comes back whenever I have Coq start evaluating a new file. In conjunction with #131, this is extremely annoying.

Request: `induction!` and `inversion!` like `intros!`

6

I think PG might already have support for something vaguely like this using `infoH`, but I'd like autocompletion support for it as well. (Does PG have support for it?)