walker (Jul 30 2022 at 12:51): walker (Jul 30 2022 at 12:51):i am tryin to follow up official tutorial on how to write coq library plugins https://github.com/coq/coq/blob/master/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg
I thought mlg is something like ml/mli the the content of the files is very strange. note: I have 2 days worth of knowledge of ocaml, so it could still ocaml
Théo Zimmermann (Jul 30 2022 at 12:53):It's not ocaml per say, it's a descent of ml5 files of camlp5.
Théo Zimmermann (Jul 30 2022 at 12:53):They are compiled to OCaml by a preprocessor (coqpp).
walker (Jul 30 2022 at 12:56):thanks!
walker (Jul 30 2022 at 12:57):one more thing, it says it allows users to extend the syntax of ocaml
Théo Zimmermann (Jul 30 2022 at 12:57):I was looking for coqpp documentation but it looks like it doesn't exist beyond a small mention in dev/doc/changes.md. But you do not need to know much about it, you can just learn by example (and avoid writing any important OCaml code directly in the mlg files).
Théo Zimmermann (Jul 30 2022 at 12:58):walker said:
one more thing, it says it allows users to extend the syntax of ocaml
Camlp5 yes, not coqpp.
walker (Jul 30 2022 at 12:58):I was going to ask if there was documentation for coq's specific syntax extensions
Théo Zimmermann (Jul 30 2022 at 13:02):See https://github.com/coq/coq/blob/master/dev/doc/changes.md#ml4-pre-processing and https://github.com/coq/coq/blob/master/dev/doc/changes.md#transitioning-away-from-camlp5.
walker (Jul 30 2022 at 13:03):that will be helpful, thanks a lot
Théo Zimmermann (Jul 30 2022 at 13:03):BTW, since you are learning how to make a plugin, I should also point out this relevant message in case you have not seen it: https://coq.zulipchat.com/#narrow/stream/237655-Miscellaneous/topic/Plugin.20development.20with.20Coq-Elpi.2C.20Template.2FMetaCoq.2C.20Mtac2.2E.2E.2E/near/291183643
Last updated: Oct 13 2024 at 01:02 UTC