coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
- To: Jason Gross <jasongross9 AT gmail.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] any Ltac2 examples out there?
- Date: Wed, 22 Apr 2020 01:56:30 -0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk1-f174.google.com
- Ironport-phdr: 9a23:kd3ToB8pCBHunP9uRHKM819IXTAuvvDOBiVQ1KB20+0cTK2v8tzYMVDF4r011RmVBNidt6wP2rWempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffgVFiCCybL5zIxm7qQfcvdQKjIV/Lao81gHHqWZSdeRMwmNoK1OTnxLi6cq14ZVu7Sdete8/+sBZSan1cLg2QrJeDDQ9LmA6/9brugXZTQuO/XQTTGMbmQdVDgff7RH6WpDxsjbmtud4xSKXM9H6QawyVD+/9KpgVgPmhzkbOD446GHXi9J/jKRHoBK6uhdzx5fYbJyJOPZie6/Qe84RS2hcUcZLTyFPDIOyYZUSAeQCP+lYoY7zqFQSohWxHgSsGOHixyVUinLswaE2zeIsGhzG0gw6GNIOtWzZoNv3NKcVV+C1zarIwivHb/xIxzjw84fIchU7rvGNWbJ8a9beyU4qFw/Lk16dro7lPzST1uQMsGiU8e5gWvyxhGM8pAFxpyKgxsYoioXTmo0VzVXE+Dx/zY0oK9O4T0t7bsSlEJtWryyaOIp2Qt8iQ2F1oyk20KEJuZm+fCUM1Z8pxAbfZuSZf4SU5h/vTuWcLDdiiH57Zr6zmQy+/VWix+DzTsW4zldHojZYntTJq3wA0wDc582IR/Z84kutxTOC2x7I5exLPEw5kKXWJ4A8zrM1iJYfrUrDHiHzlUX4kqCbdEEp9+2y5Oj7YLjropmRPJJuhA7kKKQhgMm/DPw4MgcQW2ib/vyx1Lj58k34RLVGl+Q2kqrEvJzDK8QXu6y0DgBP3oYs7Ba/CDim0NAGknUdMF1FfxeHg5DoO1HIPv/4Ee+yj0qwnDpv3fzLPb3sDo/TInTdjrvtZ6tx5kxTxQYryNBQ/ZNUCrUPIPLpXU/xscTVDh0+MwyywubnC8ty1ocAVm2RGaKZP6bSvkWJ5uIrOeWDeIgVuDPlJ/g/+/HulWM5mUMafaSxwZQXb2m4Eu16LEWdfHrjmcwMEXwKvwo7VOzlkkeOUT9VZ3aoXqIz/Cs3CIy8DdSLeof4orWa2yHzMYdRfXsOXlKFCnDueJ+DQOxdQC2XK85l1DcDUO7yZZUm0ETktgj8yrlqKufZ0iIdvJPnktNy4qebwRM18z13AsCQ3kmCSmh1miUDQDpgj/M3mlB01lrWifswuPdfD9EGoqoRCl5rZ66Z9PRzDpXJYiyEe96ITFi8RdD/WGM+S9swx5kFZEMvQoz/3CCG5DKjBvour5LOBJEw9fiCjX34JsI40nWfkad40AVgTcxIOmmrwKV48lqLXtKbowCij6+vMJ8k8mvV7m7alDiBuUhZVEh7VqCXBX0=
On Wed, 22 Apr 2020 00:16:12 -0400
Jason Gross
<jasongross9 AT gmail.com>
wrote:
> Examples: I have some Ltac2 files in
> https://github.com/JasonGross/doctoral-thesis/tree/master/performance-experiments
> (see
> files with ltac2 in the names)
> There's also two implementations of reification using a slightly older
> version of Ltac2 at
> https://github.com/mit-plv/reification-by-parametricity (see files
> starting with Ltac2)
Thanks for that, Jason!
>
> I believe the exception-catching mechanism is Control.case (in
> https://github.com/coq/coq/blob/master/user-contrib/Ltac2/Control.v).
> It can catch exceptions from Control.zero, and the bit you were
> reading about uncatchable exceptions was probably talking about those
> raised by Control.throw.
Oh - I was not making the connection between "catching an exception"
and tactic branching - which is what zero, plus, and case appear to be
for. It looks like zero is like Ltac1's fail, and plus is like Ltac1's
'+' branching tactical. I'm not sure what case is for, though. And I
don't see how this semantics eliminates the need for those kludgy Ltac1
numeric failure levels. Is there a way to catch conditionally based on
type, allowing non-matching values to continue to unwind? I think that
how proof state and backtracking is handled by the monad needs to be
described in more detail for those
- [Coq-Club] any Ltac2 examples out there?, jonikelee AT gmail.com, 04/22/2020
- Re: [Coq-Club] any Ltac2 examples out there?, Jason Gross, 04/22/2020
- Re: [Coq-Club] any Ltac2 examples out there?, jonikelee AT gmail.com, 04/22/2020
- Re: [Coq-Club] any Ltac2 examples out there?, jonikelee AT gmail.com, 04/22/2020
- Re: [Coq-Club] any Ltac2 examples out there?, jonikelee AT gmail.com, 04/22/2020
- Re: [Coq-Club] any Ltac2 examples out there?, Tej Chajed, 04/22/2020
- Re: [Coq-Club] any Ltac2 examples out there?, jonikelee AT gmail.com, 04/22/2020
- [Coq-Club] Ltac2 retraction bug?, jonikelee AT gmail.com, 04/22/2020
- Re: [Coq-Club] Ltac2 retraction bug?, Maximilian Wuttke, 04/22/2020
- Re: [Coq-Club] Ltac2 retraction bug?, Pierre Courtieu, 04/23/2020
- Re: [Coq-Club] Ltac2 retraction bug?, jonikelee AT gmail.com, 04/23/2020
- Re: [Coq-Club] Ltac2 retraction bug?, Pierre Courtieu, 04/23/2020
- Re: [Coq-Club] Ltac2 retraction bug?, Maximilian Wuttke, 04/22/2020
- Re: [Coq-Club] any Ltac2 examples out there?, Jason Gross, 04/22/2020
Archive powered by MHonArc 2.6.18.