Stream: Coq users

Topic: file io


view this post on Zulip Quinn (Jan 17 2022 at 16:10):

Can I read a file into coq? assume it's just ascii characters in the file.

view this post on Zulip Karl Palmskog (Jan 17 2022 at 16:13):

Coq is a pure language, and there is no IO monad built in, so no, not without using some tool or extension. Most people define their own custom Coq code generators, such as the famous proprietary Clightgen tool: https://github.com/AbsInt/CompCert/tree/master/export

view this post on Zulip Michael Soegtrop (Jan 17 2022 at 16:18):

I once implemented simple (ASCII) file IO in Ltac2, but it was rejected for security reasons (being able to write arbitrary files). Maybe I make a plugin out of this.

view this post on Zulip Quinn (Jan 17 2022 at 16:19):

what about this? http://coq.io/getting_started.html

view this post on Zulip Quinn (Jan 17 2022 at 16:19):

also can i do something with ocaml interop?

view this post on Zulip Karl Palmskog (Jan 17 2022 at 16:21):

"ocaml interop" can mean a lot of things. You may want to take a look at https://github.com/coq-community/coqffi if you haven't already.

view this post on Zulip Quinn (Jan 17 2022 at 16:22):

I hadn't, so thanks!

view this post on Zulip Michael Soegtrop (Jan 17 2022 at 16:25):

Quinn said:

what about this? http://coq.io/getting_started.html

As far as I understood this, this is for doing IO in extracted OCaml code, not in Coq itself.

view this post on Zulip Karl Palmskog (Jan 17 2022 at 16:28):

theoretically, one could let Menhir generate a Coq parser of some desired grammar, then run that parser within Coq for a given string by first creating a Coq file which loads the CLI string into a Coq string and runs the Menhir parser on that string, then doing coqc on that Coq file

view this post on Zulip Michael Soegtrop (Jan 17 2022 at 16:38):

For parsing strings one could also use parsec. Menhir is better for complicated grammars, though (say C++).

But the initial question was if one can read files from within Coq, and for that IMHO an extension to Ltac2 would still makes most sense. It was actually only a few 10 lines of code. As I said, I should make a plugin out of it.

view this post on Zulip Yishuai Li (Jan 17 2022 at 17:08):

Michael Soegtrop said:

For parsing strings one could also use parsec. Menhir is better for complicated grammars, though (say C++).

Menhir is better whenever it is usable. I use Parsec for parameterized parsing like HTTP messages, and as a lexer for Menhir.

view this post on Zulip Karl Palmskog (Jan 18 2022 at 07:27):

there was some recent paper on lexing in Coq as well: https://ieeexplore.ieee.org/abstract/document/9474322


Last updated: Jan 29 2023 at 01:02 UTC