search

the-lambda-church / coquille

Interactive theorem proving with Coq in vim.
ISC License
186 stars 68 forks source link

Allow multiple coq buffers to opened at the same time #66

Open bluelightning32 opened 7 years ago

bluelightning32 commented 7 years ago
  1. Allow multiple instances of coqtop to run for different coq source buffers.
  2. Support python 2 or 3.
  3. Parse default coqtop args from _CoqProject
  4. Allow multiple line ranges for the checked, sent, and error regions. This shows when coq processes statements out of order.
  5. Fix parsing comments longer than 995 lines
  6. Fix parsing strings over 995 lines
  7. Add a utility to capture protocol traces from coqide
  8. Use better default colors when the background is dark
nomeata commented 7 years ago

Use better default colors when the background is dark

\o/

sergei-mironov commented 5 years ago

Coquille with this PR seems to work fine. I saw few errors requiring restart, but they don't block the workflow completely and probably may be fixed later. Does anybody plan to merge it? Or maybe is there a coquille fork with it applied?

bluelightning32 commented 5 years ago

I pretty much gave up on getting this merged. You can use my fork, bluelightning32:pathogen-bundle.

sergei-mironov commented 5 years ago

Thanks! Could you please enable issues for this repository? I don't feel brave enough to fix possible errors but I am ready to report them.

bluelightning32 commented 5 years ago

Done.

I won't have time to work on issues for the next few weeks, but go ahead and file them. I am interested in supporting this project.

XVilka commented 5 years ago

Should be rebased on top of the master.

bluelightning32 commented 5 years ago

I rebased it on top of the pathogen-bundle. Is that what you meant?