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 02:21:33 -0400
- Authentication-results: mail3-smtp-sop.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-f170.google.com
- Ironport-phdr: 9a23:Q+JQphdUtqht4WL0Mqu0lYqNlGMj4u6mDksu8pMizoh2WeGdxcW7ZB7h7PlgxGXEQZ/co6odzbaP7ua8BydZuc3JmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRW7oR/eu8QXjoduN7o9xxXUqXZUZupawn9lK0iOlBjm/Mew+5Bj8yVUu/0/8sNLTLv3caclQ7FGFToqK2866tHluhnFVguP+2ATUn4KnRpSAgjK9w/1U5HsuSbnrOV92S2aPcrrTbAoXDmp8qlmRAP0hCoBKjU063/chNBug61HoRKhvx1/zJDSYIGJL/p1Y6fRccoHSWZdQspdUipMCZ6+YYQSFeoMJehWoYnjqVUTrhWxBwesCuTgxTBUiXH7xrE63uY7HA3axgEsA8wCvXLJp9v1LqcSVuW1wbHGwTXBaPNW3zb96IvWfRAlv/6DQ6l9ccXUyUY1FgPFik+cppDiPzOQ2OgGrm+W7+hnVeKpim4nqB9+ojyxycgykYTJiYcVxUrF9SV92oo6Odq4SEtibNOiDZBeuSaaN45sTcMjRWFloCk6yrwauZ67YSgF044ryALYa/yCdYWD/xHtVP6JLDtmmH5ofKizihWy/ES61OHwSNe43ExXoidHjtXArm4B2h3P5sSaT/Zx40Os1iqK2g3c6+xIPVw4mK/FJ5E6zbM8i58evEvdEiPrnUj6krOadksq+uWt5eTofLfrq5uZOoBulg3zMKAjl8qiCuoiKAcORXKU+eGk2b3j40L5RLJKg+UzkqbDsZDaId0Xpre6AwNIy4oj5QuzAjW63NgCknkHK1VFeB2Dj4f3IV3BPPf4DfKnj1Stljdk2ezGM6X/DpnRKnXPirTscLZn50JC1gY/08pT649WB70dOP7zX1X+tN3cDh83KQy0xOPnBc1/1oMZX2KPA6yZP73WsVCW+O0iOOaMZIoPtzb8L/gp/eLhjXg8mVMFZ6mmwYMXaGykHvRhO0iWfX3sgs4YHWgWugo+UfflhUaZUT9TYnayR7gz6is6CIKgF4fDR5qijKaP3CehTdVqYTVkA0uLFz/HbYKfQL9YaiuJJcluiDsfTumJRIoo1BXovwj/nelJNO3Rr2caspTi19Vx6uD7mhQ79DgyBMOYmSnZTWZyn2AFQzI79K96qE15jFyE1P4r0LRjCdVP6qYRAU8BPpnGwrk/UoiqA1+TTpKyUF+jB+6eL3QxQ9Y2mYFcZk98H5C7jUmG0XP1W/kakLuEAJFy+aXZjSCodpRNjk3e3axktGEIB85GNGmonKl6rlGBCIvAkkHfnKGvJ/1FgHz9sVybxG/Lh3l2FRZqWPycD38ab0rS69/+4xGaQg==
> ...
> > 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
Oops - that last bit got truncated - it said "those of us unfamiliar
with Coq internals".
I think I am beginning to understand how case works - it looks like
Ltac1's "try tac", with a result that can be interpreted by a match to
determine if tac succeeded or failed. The code in user_contrib/Ltac2
is giving me small clues...
- [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.