Stream: Coq users

Topic: Trouble with extraction in coq 8.12.1


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Dec 10 2020 at 02:12):

We will hopefully have a solution by 8.13 :fingers_crossed:

view this post on Zulip 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: Jan 29 2023 at 05:03 UTC