Stream: Coq users

Topic: Coq Module Extraction Issue (ocaml extraction bug?)


view this post on Zulip Karl Palmskog (Oct 23 2022 at 12:02):

generated .mli breaking while being compiled by OCaml compiler is a long-standing issue, see for example: https://github.com/coq/coq/issues/16169

I'm not familiar with any workarounds besides modifying the extracted .mli via something like sed. The next generation of extraction will probably target a lower OCaml interface though, so then the problem likely goes away (see for example this)

view this post on Zulip Calvin Beck (Oct 25 2022 at 00:45):

Thanks for the response! Glad it's a known issue and I'm not alone, at least. Hopefully the future work you pointed to ends up resolving this so we can have fewer load bearing Perl and sed scripts :sweat_smile:.


Last updated: Feb 01 2023 at 11:04 UTC