Stream: Coq users

Topic: Notation tutorial?


view this post on Zulip Lutz Wrage (May 22 2021 at 22:25):

Is there any tutorial available for creating non-trivial notations? I've tried to read through the reference, but I find it quite hard to learn from it.

view this post on Zulip Yannick Forster (May 23 2021 at 11:15):

In my experience, learning how to write notations works best by looking at what other people have done, and then lots of learning by doing (and failing). For what kind of language / mathematics do you want to write notations? Somebody might then be able to point you in a direction where somebody else wrote notations for something similar

view this post on Zulip Paolo Giarrusso (May 23 2021 at 12:50):

It also helps to understand how LL(1) parsing works, and the Camlp5 manual. You can't write an LL(1) grammar without understanding a bit on the implementation, and using Coq notations is no easier. After that, most things become much easier (tho I wouldn’t say “easy”).

view this post on Zulip Paolo Giarrusso (May 23 2021 at 12:52):

I want to say “there are lots of explanations about left factoring” (which is one of the FAQs), but I didn’t find anything great last time it came up and I googled (that is, this week)…

view this post on Zulip Cody Roux (May 23 2021 at 15:55):

Yannick Forster said:

In my experience, learning how to write notations works best by looking at what other people have done, and then lots of learning by doing (and failing). For what kind of language / mathematics do you want to write notations? Somebody might then be able to point you in a direction where somebody else wrote notations for something similar

This suggests that the need for a tutorial is very real...

view this post on Zulip Lutz Wrage (May 25 2021 at 12:47):

Paolo Giarrusso said:

It also helps to understand how LL(1) parsing works, and the Camlp5 manual. You can't write an LL(1) grammar without understanding a bit on the implementation, and using Coq notations is no easier. After that, most things become much easier (tho I wouldn’t say “easy”).

I understand how LL(1) parsing works, so it's off to learning Camlp5, then. It seems there are various tutorials available. Any recommendations on a good one?

view this post on Zulip Paolo Giarrusso (May 26 2021 at 21:33):

To clarify, I haven't "learned Campl5", but I've looked up SELF and NEXT in the Campl5 manual; I don't have a tutorial to recommend, because for the basics I've mostly followed examples in Coq IIRC :-|

It also depends on where you're getting stuck.

view this post on Zulip Paolo Giarrusso (May 26 2021 at 21:34):

FWIW, this is a short summary (not a tutorial) re the left factoring problem https://gitlab.mpi-sws.org/iris/iris/-/blob/3cd45dbc6bf7b1a7e30990df6396401526848c37/docs/proof_guide.md#notations


Last updated: Feb 09 2023 at 00:03 UTC