Stream: Dune devs & users

Topic: debugging extracted code


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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 02 2022 at 21:38):

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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 02 2022 at 21:38):

copy the ml files to a debug dir

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 02 2022 at 21:43):

you need to add them to the rule

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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 02 2022 at 21:43):

like if you do

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

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

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

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

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

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

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

view this post on Zulip Vadim Zaliva (Nov 02 2022 at 22:08):

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

view this post on Zulip Gaëtan Gilbert (Nov 02 2022 at 22:17):

remove the extraction stanza and manually copy the file from _build

view this post on Zulip Vadim Zaliva (Nov 02 2022 at 22:22):

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

view this post on Zulip Vadim Zaliva (Nov 02 2022 at 22:23):

it looks like I need to find other way

view this post on Zulip Gaëtan Gilbert (Nov 02 2022 at 22:29):

is removing the one module from coq.extraction hard?

view this post on Zulip Vadim Zaliva (Nov 02 2022 at 22:33):

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

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

view this post on Zulip 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: Feb 04 2023 at 01:03 UTC