Stream: Coq users

Topic: what are mlg files?


view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Jul 30 2022 at 12:53):

It's not ocaml per say, it's a descent of ml5 files of camlp5.

view this post on Zulip Théo Zimmermann (Jul 30 2022 at 12:53):

They are compiled to OCaml by a preprocessor (coqpp).

view this post on Zulip walker (Jul 30 2022 at 12:56):

thanks!

view this post on Zulip walker (Jul 30 2022 at 12:57):

one more thing, it says it allows users to extend the syntax of ocaml

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip walker (Jul 30 2022 at 12:58):

I was going to ask if there was documentation for coq's specific syntax extensions

view this post on Zulip 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.

view this post on Zulip walker (Jul 30 2022 at 13:03):

that will be helpful, thanks a lot

view this post on Zulip 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: Jan 31 2023 at 13:02 UTC