Stream: Coq users

Topic: De-extracting back to Coq


view this post on Zulip Théo Winterhalter (Mar 23 2022 at 16:01):

Hi! Is there any known way for going back from extracted Coq to Coq? Like I have a datatype T representing an AST in Coq which I extract in ocaml to perform some operation on it. Then I would like to get the output back in Coq as a valid .v file producing a value of the original T type.

view this post on Zulip Karl Palmskog (Mar 23 2022 at 16:05):

@Théo Winterhalter have you tried Coq-of-OCaml? That's the closest tool I know of: https://github.com/formal-land/coq-of-ocaml

Maybe QuickChick has some way to track the provenance of code it extracts for running tests (https://github.com/QuickChick/QuickChick/)

view this post on Zulip Théo Winterhalter (Mar 23 2022 at 16:18):

I haven't tried it, but from what I can tell it would produce a new copy of T?


Last updated: Feb 01 2023 at 11:04 UTC