[Coq-Club] Mtac2 1.0 is here!

[Beta Ziliani]

We are proud to announce the official 1.0 release of Mtac2.

A little FAQ:

1.

What is it?
It is a plugin providing Coq with a *typed* tactic language. It is
described in this paper
<https://people.mpi-sws.org/~beta/papers/Kaiseretal18.pdf>.
2.

Can you give a quick example?
For instance, in a recent email someone got bitten by Ltac’s lack of
support for coercions. In Mtac2, the terms you write are Coq’s terms, as
Coq understands them.

Definition show_H:=
match_goal with
| [[? (O:ordType) (x y : O) (G:Prop) | (H: x == y) |- G]] => M.print_term H
end.

Of course, the price to pay is that you need to provide the typing
information. But once you write it down, you know it works!

Much more can be found in Mtac2’s github page
<https://github.com/Mtac2/Mtac2>.
3.

Is there an opam archive?
We just created the PR <https://github.com/coq/opam-coq-archive/pull/395>
for Coq’s opam’s archive. Once its processed it should be available simply
typing opam install coq-mtac2.
4.

Which version of Coq does it support?
Currently only 8.7.X, but we plan to add 8.8 soon. Feel free to ask!
5.

Why the 2 in the name? Why not Mtac 2.0?
We wanted to make clear that there is much more to Mtac2 than what there
was in Mtac. So if you’ve heard about Mtac, and its limitations, take a new
look at Mtac2, it has a lot more to it.
6.

I heard about some MetaCoq, is it related?
Yes, MetaCoq was the name for Mtac2 before we decided that the name
didn’t really express what Mtac2 is. Actually, the first project Mtac
should’ve been named MetaCoq, since it only provides meta-programming and
not tactic programming in full.

The Mtac2’s team.

[Beta Ziliani]

Quick update: Coq 8.8 and master are now supported. We have and opam
package for 8.7, and one for 8.8 is on the way.

Post by Beta Ziliani
We are proud to announce the official 1.0 release of Mtac2.
1.
What is it?
It is a plugin providing Coq with a *typed* tactic language. It is
described in this paper
<https://people.mpi-sws.org/~beta/papers/Kaiseretal18.pdf>.
2.
Can you give a quick example?
For instance, in a recent email someone got bitten by Ltac’s lack of
support for coercions. In Mtac2, the terms you write are Coq’s terms, as
Coq understands them.
Definition show_H:=
match_goal with
| [[? (O:ordType) (x y : O) (G:Prop) | (H: x == y) |- G]] => M.print_term H
end.
Of course, the price to pay is that you need to provide the typing
information. But once you write it down, you know it works!
Much more can be found in Mtac2’s github page
<https://github.com/Mtac2/Mtac2>.
3.
Is there an opam archive?
We just created the PR
<https://github.com/coq/opam-coq-archive/pull/395> for Coq’s opam’s
archive. Once its processed it should be available simply typing opam
install coq-mtac2.
4.
Which version of Coq does it support?
Currently only 8.7.X, but we plan to add 8.8 soon. Feel free to ask!
5.
Why the 2 in the name? Why not Mtac 2.0?
We wanted to make clear that there is much more to Mtac2 than what
there was in Mtac. So if you’ve heard about Mtac, and its limitations, take
a new look at Mtac2, it has a lot more to it.
6.
I heard about some MetaCoq, is it related?
Yes, MetaCoq was the name for Mtac2 before we decided that the name
didn’t really express what Mtac2 is. Actually, the first project Mtac
should’ve been named MetaCoq, since it only provides meta-programming and
not tactic programming in full.
The Mtac2’s team.