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!

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.

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...)

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: Oct 12 2024 at 12:01 UTC