The Coq mailing list

[Helmut Brandl <helmut.brandl AT gmx.net>]

I have observed a potential code bloat when extracting from Coq to OCaml.

I want to use modules extensively to structure my code. E.g. I have written a module ‘Binary_tree.v’ which defines the basic data types and access function for binary trees.

The basic module ‘Binary_tree.v’ is used by another module called ‘Avl_tree.v’. The ‘Avl_tree’ uses the basic services of ‘Binary_tree’ by including it.

In the extracted code of ‘Avl_tree’ I see the module ‘Binary_tree’ physically copied into the module ‘Avl_tree’ i.e. all data type definitions and functions are copied.

Since it is often the case that one module extends the functionality of another more basic module I am worried that in the end I will get OCaml code which is very bloated.

Can anybody comment on this observation? Are there experiences with code extraction using modules extensively to structure the code? Thanks for any hint.

The code can be found at http://github.com/hbr/coqlib.

Regards

Helmut