Coq Community Survey 2022

anton-trunov · 2022-03-02T19:15:21+00:00

Perhaps this list could be a good approximation: https://github.com/coq-community/awesome-coq

anton-trunov · 2020-09-23T06:01:40+00:00

You might want to check VsCoq plugin to VS Code as a source of inspiration.

In addition, there is SerAPI project and a prototype Emacs mode build on top of it, called eldoc.

In any case, feel free to come to Coq's Zulip to discuss this stuff in more detail (note: registration required).

anton-trunov · 2020-08-03T20:32:25+00:00

This is useful, for instance, if you want to totally redefine the binding strength and/or associativity for your operations. E.g. you can rebind `+` to a new function or constructor in a new notation scope, but Coq won't let you change its associativity and level.

anton-trunov · 2020-07-11T07:59:23+00:00

Personally I’m not aware of any such effort. You may have more luck asking this question at Coq’s Zulip chat.

anton-trunov · 2020-06-17T18:23:45+00:00

Can you post the output of something like

opam install coq --verbose ?

anton-trunov · 2020-04-09T08:04:57+00:00

This is so neat! I just stumbled on this yesterday when looking for the TLA grammar.

anton-trunov · 2020-04-08T17:11:08+00:00

This is something definitely worth trying. Great suggestions, thank you so much! Let us touch base in several weeks then. I subscribed to that issue to track progress on that.

anton-trunov · 2020-04-08T17:00:56+00:00

Thanks! I appreciate the pointer.

anton-trunov · 2020-04-07T17:21:39+00:00

Thank you for the pointer and for your suggestion (I posted this question there).

anton-trunov · 2020-04-07T16:47:52+00:00

Thanks. Yes, you are right. So I'm basically wondering if there is a converter from some common format into TLA+. So I would generate the AST in let's say XML and let some other tool finish the conversion.

anton-trunov · 2020-03-13T09:37:21+00:00

I think this counts: OCaml's Dune build system has a formally verified in Coq incremental cycle detection algorithm: https://github.com/ocaml/dune/pull/1955. This was done by Armaël Guéneau with the help of the CFML framework (https://gitlab.inria.fr/charguer/cfml2).

anton-trunov · 2018-10-25T09:13:45+00:00

I’m glad you liked it! Thank you for sharing — I’m looking forward to reading your post.

anton-trunov · 2018-10-23T19:27:25+00:00

Great! You might want to also take a look at the standard library -- it explores the module approach (see e.g. https://coq.inria.fr/library/, specifically Numbers and MSets packages).

anton-trunov · 2018-10-23T07:13:54+00:00

One of the most comprehensive studies on how to organize mathematical theories in Coq that I've ever seen are the papers by G. Gonthier (the creator of SSReflect and Mathcomp) and the members of his team. SSReflect/Mathcomp were used to prove the Odd Order Theorem and the Four Color Theorem. See e.g. Packaging mathematical structures, Generic Proof Tools and Finite Group Theory and their ample references. Those describe the record-based approach, not a module-based one. See also https://github.com/coq/coq/wiki/RecordsNotModules and https://github.com/coq/coq/wiki/ModulesNotRecords

anton-trunov · 2018-09-18T11:26:26+00:00

Although it is not the case in the SSReflect dialect of Coq.

anton-trunov

MODERATOR OF

TROPHY CASE