Localisation of errors during extraction of cloned module
Recently, I tried to extract some code written in Why3 into OCaml. I did not manage to use modular extraction so I used flat extraction which seemed easier to handle. Something like:
why3 extract -L . --recursive -D ocaml64 -D driver/ocaml_ext.drv interface.mlw -o extract/all.ml
In my Why3 code, I cloned the hasthbl.mlw file. So, I need to provide a driver for this cloned module so that I instantiate all axiomatic parts with real OCaml code. My feature wish would be to improve the error that why3extract
outputs when it cannot find an implementation for a specific ident. I currently typically get:
File "$MY_PATH_TO_WHY3/why3/share/stdlib/hashtbl.mlw", line 30, characters 6-9:
Symbol mem1 cannot be extracted
I would like to know which chain of clone is used to find this error. For example, in my case, I clone this library two different times (not with the same key type) and in one of the cases I clone the resulting module. So, this gets pretty confusing. I would like something along the lines of:
Symbol mem1 cannot be extracted during cloning of Hashtbl at file my_hashtbl.mlw line 15 characters 42
The symbol is originally defined in
File "$MY_PATH_TO_WHY3/why3/share/stdlib/hashtbl.mlw", line 30, characters 6-9:
The chain of cloning is the following:
Hashtbl at file hashtbl.mlw ...
H at file my_hashtbl.mlw ...
Ha at file my_code.mlw ...
Looking at the code for extraction, I think that the cloning module can be tracked and the error could be better handled. I can try to look at how this could be done if there is no time ?