Stream: Dune devs & users

Topic: debugging extracted code

Vadim Zaliva (Nov 02 2022 at 21:34):

I am trying to debug OCaml extracted from Coq. Adding some print statements to generated code probably would be enough. But if I modify .ml files extracted from Coq and do dune exec it will re-generate them again from Coq. If there is a way to tell dune temporary not to re-run extraction step?

Emilio Jesús Gallego Arias (Nov 02 2022 at 21:38):

It's a bit clunky but maybe you could use copy files + promote?

Emilio Jesús Gallego Arias (Nov 02 2022 at 21:38):

copy the ml files to a debug dir

Emilio Jesús Gallego Arias (Nov 02 2022 at 21:38):

then set promote on the rule so they are only regenerated when you clean them

Emilio Jesús Gallego Arias (Nov 02 2022 at 21:39):

this seems like an interesting use case but I think we are stuck on a good user interface for it, so don't hesitate to open an issue

Vadim Zaliva (Nov 02 2022 at 21:40):

I am interested in any even hacky solution. I have a bug to find :) I wonder how promotion works for generated files? They are not explicitly mentioned in dune anywhere

Emilio Jesús Gallego Arias (Nov 02 2022 at 21:43):

you need to add them to the rule

Emilio Jesús Gallego Arias (Nov 02 2022 at 21:43):

the trick here is that the file in debug won't be the same than the generated one

Emilio Jesús Gallego Arias (Nov 02 2022 at 21:43):

like if you do

Emilio Jesús Gallego Arias (Nov 02 2022 at 21:44):

(library
 (name debug))
(rule
   (targets foo.ml)
   (mode promote)
   (action (copy ../orig/foo.ml)))

Emilio Jesús Gallego Arias (Nov 02 2022 at 21:44):

now you add the promote, and then dune will respect the file in the source tree

Emilio Jesús Gallego Arias (Nov 02 2022 at 21:45):

see https://dune.readthedocs.io/en/stable/dune-files.html#promote for more details

Emilio Jesús Gallego Arias (Nov 02 2022 at 21:46):

promotion means that the rule is only run _if_ the file needs to be generated

Vadim Zaliva (Nov 02 2022 at 21:52):

I have

(library
 (name extracted)
 (preprocessor_deps CRelationClasses.mli.patch patch.sh)
 (preprocess (per_module
             ((action (run coq/extracted/patch.sh %{input-file})) CRelationClasses)
             ))
 (public_name cerberus.coq)
 (libraries zarith coq-core.kernel)
 (wrapped false)
 (flags (:standard -rectypes -w -27-32-33-39-67-37-20-34))
)

can I add promotion rule for single file in this library?

Vadim Zaliva (Nov 02 2022 at 22:07):

I tried to add rule and the problem is:

(rule
 (targets CheriMemory.ml)
 (mode promote)
 (action (copy ../orig/CheriMemory.ml CheriMemory.ml)))

Vadim Zaliva (Nov 02 2022 at 22:07):

Error: Multiple rules generated for
_build/default/coq/extracted/CheriMemory.ml:
- coq/extracted/dune:7
- coq/extracted/dune:1

Vadim Zaliva (Nov 02 2022 at 22:08):

line 7 is rule I've added and line 1 is original coq.extraction stanza

Gaëtan Gilbert (Nov 02 2022 at 22:17):

remove the extraction stanza and manually copy the file from _build

Vadim Zaliva (Nov 02 2022 at 22:22):

I see. It is one of 227 files generated :)

Vadim Zaliva (Nov 02 2022 at 22:23):

it looks like I need to find other way

Gaëtan Gilbert (Nov 02 2022 at 22:29):

is removing the one module from coq.extraction hard?

Vadim Zaliva (Nov 02 2022 at 22:33):

there are inter-dependecies. it worst case I can try

Vadim Zaliva (Nov 02 2022 at 22:34):

right now I am investigating alternative approach by mapping OCamls print_endline to Coq via Extraction. This way I can try to print from Coq

Ali Caglayan (Nov 03 2022 at 04:13):

You should promote them into a different directory and have another library stanza for debugging.

Last updated: Oct 13 2024 at 01:02 UTC