whonore / coqtail Goto Github PK
View Code? Open in Web Editor NEWInteractive Coq Proofs in Vim
License: MIT License
Interactive Coq Proofs in Vim
License: MIT License
2019-07-02 10:52:39,592: <?xml version="1.0" ?>
<call val="SetOptions">
<list>
<pair>
<list>
<string>Printing</string>
<string>Width</string>
<string>999999</string>
</list>
<option_value val="boolvalue">
<bool val="true"/>
</option_value>
</pair>
</list>
</call>
2019-07-02 10:52:39,596: <?xml version="1.0" ?>
<response>
<feedback object="state" route="0">
<state_id val="0"/>
<feedback_content val="message">
<message>
<message_level val="warning"/>
<option val="none"/>
<richpp>
<_>
<pp>There is no option Printing Width 999999. [unknown-option,option]</pp>
</_>
</richpp>
</message>
</feedback_content>
</feedback>
<value val="good">
<unit/>
</value>
</response>
2019-07-02 10:52:39,599: goals
2019-07-02 10:52:39,600: <?xml version="1.0" ?>
<call val="Goal">
<unit/>
</call>
2019-07-02 10:52:39,602: <?xml version="1.0" ?>
<response>
<feedback object="state" route="0">
<state_id val="1"/>
<feedback_content val="processed"/>
</feedback>
<value val="good">
<option val="none"/>
</value>
</response>
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.
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 { }
.
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...).
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.
Like this fork of Coquille had done. See this commit: https://framagit.org/tyreunom/coquille/commit/3323c46cfa521395c88ece0b854bbdc9f8399672
The From my_lib Require my_module
syntax doesn't seem to be handled.
Proofs of the form
Goal True.
Proof I.
confuse the highlighting and indenting because they expect a Qed
.
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 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
.
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).
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. *)
#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 first Print
is not highlighted here:
From foo Require Import bar.
Print 0.
Print 0.
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.
Goal True.
Set Nested Proofs Allowed.
Goal True. (* j k j --> previous option ignored *)
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.
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
).
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?
Goal True. Proof. do 5 idtac ".". Abort.
only results in one .
being printed instead of 5.
Simple example:
Coercion Tyvar : tyvar >-> ty.
Everything after Coercion
gets highlighted in red.
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
Might be interesting to use https://github.com/ejgallego/coq-serapi instead of talking to coqtop directly.
Goal True.
pose proof (eq_refl 0).
do 500 match goal with H: ?x = ?x |- _ => pose proof (eq_refl (S x)) end.
(* "True" should be visible in the goal buffer at this point, as in coqide and PG *)
Abort.
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
Would it be easy to make it so :Coq About nat
behaves like :Coq About nat.
?
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 ?
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.
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:
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?
it should probably leave the cursor untouched?
probably just #11, as C-c C-c fixes it
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. *)
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 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?
in particular it should do the thing without moving the cursor
Goal True.
Proof.
{ destruct H10; intuition eauto.
{ eexists. split.
{ subst a1. subst a.
rewrite List.app_assoc; trivial. }
eexists. split. (* unindent here *)
{ eapply Forall2_app; eauto. }
eexists _, _; split.
{ subst v; trivial. }
left; split; eauto.
eapply concat_app; cbv [any choice lightbulb_spec.spi_timeout]; eauto. }
split. (* unindent here *)
{ rewrite List.app_assoc; trivial. }
eexists.
split.
{ eapply Forall2_app; eauto. }
eexists _, _; split.
{ subst v. eauto. }
right. split; eauto.
cbv [lightbulb_spec.spi_xchg].
(* why is this so indented? *)
assert (Trace__concat_app : forall T (P Q:list T->Prop) x y, P x -> Q y -> (P +++ Q) (y ++ x)). {
cbv [concat]; eauto. } (* unindent here *)
eauto using Trace__concat_app. }
Qed.
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.
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.
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.
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.
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
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 ?
Should support interactive ltac debugging provided by Set Ltac 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
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.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.