Stream: Coq devs & plugin devs

Topic: Tips for Starting Contributing?


view this post on Zulip Peter Gao (Dec 01 2022 at 05:06):

Hello all. I'm interested in this comment here: https://github.com/coq/coq/issues/9039#issuecomment-821842114
However, as dumb as it sounds, I do not know how to get started -- for example, where in the code base are the reduction strategies implemented? What about specific tactics like simpl? Thanks!

view this post on Zulip Andres Erbsen (Dec 01 2022 at 05:30):

I think the suggestion there is still valid, but now it might actually be easier to try out an Ltac2 implementation using Ltac2.Constr.Unsafe first. This API is quite similar to the Coq internal representation and a prototype based on it could serve as a stepping stone for an OCaml implementation. OTOH It's possible that you'll run into missing functionality in Ltac2.

view this post on Zulip Peter Gao (Dec 01 2022 at 05:54):

Andres Erbsen said:

I think the suggestion there is still valid, but now it might actually be easier to try out an Ltac2 implementation using Ltac2.Constr.Unsafe first. This API is quite similar to the Coq internal representation and a prototype based on it could serve as a stepping stone for an OCaml implementation. OTOH It's possible that you'll run into missing functionality in Ltac2.

Thanks for the suggestion! I still want to see how the reduction strategies and tactics are implemented in the current Coq core first, as a reference point. Any idea on where they are in the repository? (or better yet, how to find specific implementations in general? The Standard Library didn't seem to help...)

view this post on Zulip Gaƫtan Gilbert (Dec 01 2022 at 08:56):

In that issue Jason says

the reduction strategies (match, fix, delta, beta, iota, zeta

but I would call these reduction flags (parsed by https://github.com/coq/coq/blob/e9f7e871638e0a0c48ceb2a21fdc9a4962d1d28f/plugins/ltac/g_tactic.mlg#L336 but the main type after parsing phases is https://github.com/coq/coq/blob/e9f7e871638e0a0c48ceb2a21fdc9a4962d1d28f/kernel/cClosure.mli#L25)

What I call reduction strategies is rather lazy cbv cbn vm_compute simpl etc
they get dispatched here https://github.com/coq/coq/blob/e9f7e871638e0a0c48ceb2a21fdc9a4962d1d28f/tactics/redexpr.ml#L238
from there use your editor's jump to definition to find the implementations


Last updated: Feb 05 2023 at 19:29 UTC