Stream: Dune devs & users

Topic: Extraction support


view this post on Zulip Rudi Grinberg (May 31 2022 at 20:11):

you could also consider making extraction a separate binary if it would be possible to strip many dependencies from it

view this post on Zulip Ali Caglayan (May 31 2022 at 20:16):

I don't know if it would be possible to separate an extraction binary. The extraction commands are quite complicated: https://coq.inria.fr/refman/addendum/extraction.html

view this post on Zulip Rudi Grinberg (May 31 2022 at 21:05):

Sure, it was just a thought.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 01 2022 at 12:07):

It is possible to make extraction a binary, it should not be hard unless I'm missing something. Similiar to coqnative


Last updated: Jan 30 2023 at 17:03 UTC