root edited this page Oct 11, 2017 · 87 revisions

What happens at the Coq Coding Sprint

This page is to log all the activities done during the Coq Implementors Workshop. Please put here links to the bugs you've fixed, to the git repository containing your plugin or your experimental branch.

Monday 12

  • Intro talk by Matthieu
  • Matthieu: Unification, universes in template-coq and CONTRIBUTING
  • Nicolas, Thierry no particular projects
  • Abhishek: unused variables test and universes in template-coq
  • Emilio: Few minor PRs.

Tuesday 13

  • Emilio: Talk about UI; spend afternoon discussing about side-effects and STM init. Ported ELPI to jsCoq.

Wednesday 14

Thursday 15

Friday 16

Abhishek: Tested the above-mentioned "reduce away var" plugin to strengthen a free theorem produced by paramcoq-iff. The above plugin removes a hypothesis in 0.8s. Using coq's [lazy] tactic takes 30s.

Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.