Avi Shinnar (Dec 10 2020 at 01:38): Avi Shinnar (Dec 10 2020 at 01:38):I am porting a library from an older version of Coq to coq 8.12.1 and can't get (Ocaml) extraction to work properly.
There are three definitions of the int type: in Numeral.ml, Hexadecimal.ml, and Decimal.ml, none of which are compatible with ocaml's int (which is what I expect/want). This breaks the ocaml glue code that calls it.
Any ideas on how to solve this?
This did not happen with older versions of Coq.
The extraction file is using
Require Import ExtrOcamlBasic ExtrOcamlString ExtrOcamlNatInt ExtrOcamlZInt.
The full Coq file used for extraction is available here: https://github.com/IBM/FormalML/blob/coq8.12/ocaml/NnoptExtraction.v
I have not been able to figure out why it is not working anymore. Any ideas?
Matthieu Sozeau (Dec 10 2020 at 02:12):That's a known issue. Extraction handles badly this case, and the current workarounds are discussed here: https://github.com/coq/coq/issues/13288
Matthieu Sozeau (Dec 10 2020 at 02:12):We will hopefully have a solution by 8.13 :fingers_crossed:
Avi Shinnar (Dec 11 2020 at 03:47):Matthieu Sozeau said:
That's a known issue. Extraction handles badly this case, and the current workarounds are discussed here: https://github.com/coq/coq/issues/13288
Thanks! the workaround suggested in the issue linked from that issue resolves the problem and allows extraction to work again.
Last updated: Sep 28 2023 at 10:01 UTC