Karl Palmskog (Jun 09 2020 at 15:34): Karl Palmskog (Jun 09 2020 at 15:34):Is it possible to remove an extracted .mli file? Having some trouble to get code to compile since the generated interface is over-constraining. Or could one set up some workflow to process/transform the .mli?
Emilio Jesús Gallego Arias (Jun 09 2020 at 15:54):I had similar problems in the past with bugs for extraction, that's a pita
Emilio Jesús Gallego Arias (Jun 09 2020 at 15:54):we even thought of adding some post-processing action, but I am trying to fix the bug in coq instead
Emilio Jesús Gallego Arias (Jun 09 2020 at 15:55)::S
Emilio Jesús Gallego Arias (Jun 09 2020 at 15:56):certainly you could try to use (modules ...) in your library stanza + a copy file only for the ml
Emilio Jesús Gallego Arias (Jun 09 2020 at 15:56):I think that may work
Emilio Jesús Gallego Arias (Jun 09 2020 at 15:56):if we have extraction producing A_wrong.mli A_wrong.ml
Emilio Jesús Gallego Arias (Jun 09 2020 at 15:56):and we do (copy A_wrong.ml A.ml)
Emilio Jesús Gallego Arias (Jun 09 2020 at 15:57):then you exclude A_wrong from you lib modules
Karl Palmskog (Jun 09 2020 at 15:57):ah OK, right
Emilio Jesús Gallego Arias (Jun 09 2020 at 15:57):seems to me that the dependency path is sane
Emilio Jesús Gallego Arias (Jun 09 2020 at 15:57):still a hack :S
Last updated: Oct 13 2024 at 01:02 UTC