whonore / coqtail Goto Github PK

This is actually not a problem of Coqtail - it works very well in the terminal. But since gvim is not started from an interactive bash session, the opam envs cannot be loaded. I installed coq following the official guide which uses opam, and in this case coq cannot be found.

I'm looking forward to some advice on how to get around this. I have tried to set $BASH_ENV in my .vimrc but it didn't work.

I'm trying out the Equations package, which introduces a new Equations command, and of course it would be nice to have it properly highlighted.

• Equations
• Derive Signature for _type_

Naturally, this also raises the more general question of what can be done about syntactic extensions outside of a limited "standard" core.

In the case of Equations, it seems to substantially improve dependently-typed programming in Coq to the point that I would consider it standard.
PG already highlights the Equations keyword but I don't know much more than that.

In general, for less essential packages, it makes sense to not support them individually. But unknown commands are currently highlighted in red, while it might be a good idea to not highlight them at all, as a more neutral choice.

The following coq file is currently processed incorrectly:

Goal nat * unit.
  intros.
  split.
  2: { (* there should be a sentence boundary here *)
    exact tt.
  }
  exact O.
Defined.

See coq/coq#6551 for context. The "Focus" syntax is now deprecated, so it would be good to support this one instead (and bedrock2 uses it...).

Hi !
I updated my vim / plugins this morning and I got the following error message after my first evaluation command (leader c j, :CoqStart is fine):

Error detected while processing :
Traceback (most recent call last):
  File "<string>", line 1, in <module>
  File "/Users/vsiles/.vim/bundle/Coqtail/python/coqtail.py", line 162, in step
    self.send_until_fail()
  File "/Users/vsiles/.vim/bundle/Coqtail/python/coqtail.py", line 276, in send_until_fail
    self.reset_color()
  File "/Users/vsiles/.vim/bundle/Coqtail/python/coqtail.py", line 612, in reset_color
    _make_matcher((sline, scol + 1), (eline + 1, ecol)),
  File "/Users/vsiles/.vim/bundle/Coqtail/python/coqtail.py", line 734, in matchadd
    vim.command("let b:{} = matchadd('{}', '{}')".format(var, group, zone))
vim.error: Vim(let):E28: No such highlight group name: CoqtailSent

Here are my revisions/versions:

• coqtail: 97d1633
• VIM - Vi IMproved 8.1 (2018 May 18, compiled Jun 3 2019 04:49:45)
  macOS version
  Included patches: 1-1450
  Compiled by Homebrew
• The Coq Proof Assistant, version 8.8.0 (February 2019)
  compiled on Feb 1 2019 10:31:25 with OCaml 4.07.0

Simple example:

Coercion Tyvar : tyvar >-> ty.

Everything after Coercion gets highlighted in red.

The first Print is not highlighted here:

From foo Require Import bar.

Print 0.
Print 0.

The following fail because the line beginning with Set is being parsed as a command to set an option. Also a problem for lines beginning with Unset or Test.

Require Import
  Setoid.
Variable x : 
  Set.

Hi ! My project is growing a bit and I'd like to use _CoqProject. Is this supported ?
At the moment I have something very simple with a Makefile (from https://izgzhen.github.io/2016/09/19/coq-dev.html) and a _CoqProject like:

-Q . MyPrj
A.v
B.v

A.v:

Definition t := nat.

B.v:

Require Import List MyPrj.A.
Definition t := list A.t

Building on the command line works:

$ make
coq_makefile -f _CoqProject | sed 's/$(COQCHK) $(COQCHKFLAGS) $(COQLIBS)/$(COQCHK) $(COQCHKFLAGS) $(subst -Q,-R,$(COQLIBS))/' > Makefile.coq
Warning: Omitting -o is deprecated

make -f Makefile.coq all
COQDEP VFILES
COQC A.v
COQC B.v

The overall experience work: I can evaluate A.v and B.v interactively, but I get an error message in B.v: B.v|1 col 15 error| Error: Cannot find a physical path bound to logical path matching suffix MyPrj.

Am I missing something ?

Stretch goal: Coqtail tries to solve the current goal in the background and automatically fills in a proof if found. Should be toggle-able option

Even before supporting #2, should restructure things so that Vim does not have to wait on Coq for certain editing actions. E.g., while waiting for Coq to check some lines, it should be possible to move the cursor, edit text (at least that which comes after those lines), and open/edit other files.

Hi !
I'm not sure it's a bug, more likely a bad interaction with my config. Here is what happens when I open a non Coq file, and I press O on a line starting with *:
https://asciinema.org/a/W0i3Tea9HXtqVIjfSu0YpLsAQ

Here is what happens when I open a Coq file and I press O on a line starting with *:

https://asciinema.org/a/7boKSFb7ExKehoG8DGdudBcHF

Does that ring a bell to anyone ?

At least 1 or 2 of the Coq tests almost always fail with error: file 'nixpkgs' was not found in the Nix search path (add it using $NIX_PATH or -I). Rerunning usually fixes it on the first try.

https://coq.github.io/doc/v8.10/refman/proof-engine/proof-handling.html?highlight=diff#coq:opt.diffs. Use hl-DiffAdd, hl-DiffChange, etc for colors.

CoqIDE supports asynchronous editing of files where one can work on a later part of a file while the earlier parts are checked in the background. It would be cool to support this too.

The plugin is great to use, as it offers experience in vim like native Coq IDE ;P

I would like to know which lines have already been proved, so I always know where I am.
Does Coqtail offer this feature? I see CoqIDE and coquille have this feature, and for Coqtail when I enable cursorline I can see indications at the end of line when I place the cursor onto a line that is already proved. But I would like the indication to work even if cursorline is not enabled. Also I would like it to be clearer e.g. different bgcolor for proven / unproven lines.

Is it easy to do this in Coqtail?

I have added au FileType coq CoqStart to my .vimrc. When I open a .v file I am presented with a duplicate panel. What should I do?

Goal False.
Proof.
  { idtac. }
Admitted.

Coqtail let's this go through as if } was admit. } but coqc gives the error Error: This proof is focused, but cannot be unfocused this way. Coqtail also gives this error for empty braces { }.

Create some Python tests for at least the vim-independent files (coqtop, and xmlInterface). Could make a script to use nix to automatically run tests for different versions of Coq and Python.

Hi !
When I try to evaluate SearchAbout nat, the plugin stop responding (it display a couple entries and that's it). Is there a way to use SearchAbout with this plugin ?
Note: coq-au-vim has the same issue :p

#31 adds support for an unreleased version of coq, but no tests. I have been having an okay time testing bedrock2 against coq master using this script: https://github.com/mit-plv/bedrock2/blob/master/.builds/nixos-coqmaster.yml

The From my_lib Require my_module syntax doesn't seem to be handled.

in particular it should do the thing without moving the cursor

Goal True. Proof. do 5 idtac ".". Abort. only results in one . being printed instead of 5.

currently, the parsing api only supports parsing at the tip of the document.
you wanted to parse at: 2479 but the current tip is: 2492

I have the session open still

The code following := {||}. gets highlighted in bright red. Note that := {}. is also possible, though it is going to be deprecated.

Instance Foo := {||}.
Proof.
  intros.
Qed.

Currently after solving a subgoal, the goals window only shows 0 subgoals, i.e., you only see subgoals under the current bullet. When you're done with a bullet, it would be nice to know whether more bullets remain (and ideally, which bullet is next).

Goal True /\ False.
Proof.
  split.
  - constructor.
    (* Says "0 subgoals", but there is still the False branch of the other "-" bullet left. *)

Should support interactive ltac debugging provided by Set Ltac Debug.

https://github.com/sifive/Kami/blob/bf1564ecd875872aa465f14e97bf6f52825f82e1/Tutorial/SPI.v#L414

Currently some of the Coqtop commands (GetOptions, Hints, etc) are not supported. It would be good to add support for these even if they are only exposed to the user through raw commands of the form Coq Hints, Coq Evars. This would make it easier to add more features in the future.

Calling to_cursor() when the last endpoint is further than the current line will rewind to just before that line, but calling it when the endpoint is on the same line does not move the checked section.

Might be interesting to use https://github.com/ejgallego/coq-serapi instead of talking to coqtop directly.

probably just #11, as C-c C-c fixes it

open a file, CoqToCursor to the middle of it, then open the same file in the bottom-right window:

Error detected while processing function coqtail#OpenPanels:
line   19:
Traceback (most recent call last):
  File "<string>", line 1, in <module>
  File "/home/andres-erbsen/.vim/pack/coq/start/coqtail/python/coqtail.py", line 590, in reset_color
    vim.command("call coqtail#ClearHighlight()")

this happens even if i split the bottom-right window first

the effect should be visible on a file like this one:

Goal True.
  do 5 (idtac "."; do 400 pose I).
Abort.

A real use case would be hunting down the reason why typeclass resolution doesn't terminate using Set Typeclasses Debug.

When I try to autocomplete with ctrl+n I get the errors below. Reproducing this seems to require at least one Require loaded.

Require List. (* stop Coq buffer here *)
f (* ctrl+n here *)

Scanning tags.
Error detected while processing function coqtail#FindLib:
line    1:
Traceback (most recent call last):
Press ENTER or type command to continue
Error detected while processing function coqtail#FindLib:
line    1:
  File "<string>", line 1, in <module>
Press ENTER or type command to continue
Error detected while processing function coqtail#FindLib:
line    1:
NameError: name 'Coqtail' is not defined
Press ENTER or type command to continue
Error detected while processing function coqtail#FindLib:
line    1:
E858: Eval did not return a valid python object

I'd love to try using this plugin, and especially to recommend it to vim users, but we prefer to support only the latest release of Coq and Coq master, which is now Coq 8.9 and 8.10+alpha.

What is needed to support Coq 8.9 and above?

Would it be easy to make it so :Coq About nat behaves like :Coq About nat.?

Proofs of the form

Goal True.
Proof I.

confuse the highlighting and indenting because they expect a Qed.

In the following case Coqtail should print an error and highlight the unmatched token instead of silently refusing to take a step.

Definition x := "unmatched.
Definition y := 1.

(* Unmatched

Definition x := 1. *) 

it should probably leave the cursor untouched?

Ltac named_pose x := let H := fresh in let __ := match constr:(Set) with _ => pose x as H end in H.
Goal True. let n := named_pose I in idtac n. (* H *) Abort.

Ltac pn := let n := numgoals in idtac n.

Goal True /\ True.
  assert_succeeds (split; pn).
  assert_succeeds (split; [pn..]).
Abort.

Module goodfresh.
  Ltac myfresh := fresh.
  Goal True.
    let v := myfresh in
    let w := myfresh in
    idtac v w. (* H H *)
  Abort.
End goodfresh.

Module badfresh.
  Ltac myfresh x := let __ := match constr:(Set) with _ => idtac "FRESH" x end in fresh.
  Goal True.
    let v := myfresh 1 in
    let w := myfresh 2 in
    idtac w v. (* H H *)
  Abort.
End badfresh.

Module testfresh.
  Ltac myfresh := let __ := match constr:(Set) with _ => idtac "FRESH" end in fresh.
  Goal True.
    let v := myfresh in
    let w := myfresh in
    idtac w v. (* H H *)
  Abort.
End testfresh.

coqide output:

H
2
1
1
H H0
FRESH 1
FRESH 2
H H
FRESH
FRESH
H0 H

coqtail output:

named_pose is defined

H

pn is defined

2

1

Interactive Module goodfresh started

myfresh is defined

H H0

Module goodfresh is defined

Interactive Module badfresh started

myfresh is defined

FRESH 2

FRESH 1

H H

Module badfresh is defined

Interactive Module testfresh started

myfresh is defined

FRESH

H0 H

Module testfresh is defined

The red highlighting when an error occurs starts a few characters too early.

in ProofGeneral, CoqToCursor moves back and forth over the sentence at the point when executed repeatedly with the same sentence. This is useful for "before and after" inspection of the effect of a command. would you consider it a desirable behavior for coqtail?

Like this fork of Coquille had done. See this commit: https://framagit.org/tyreunom/coquille/commit/3323c46cfa521395c88ece0b854bbdc9f8399672

The -I option to add paths for plugins is currently not recognized.

For an example test case, there's MetaCoq or QuickChick (I don't have something more lightweight offhand), you can build them from source and then try to load one of the examples (e.g., metacoq/test-suite/demo.v).

Goal True. Proof. idtac "."; do 1000 pose I. Abort. only prints . after the tactic completes, but the feedback message from Coq is available earlier. Would be nice to display output as early as possible for cases like #39 (comment).