Adding extracted_files field to rocq.extraction stanza#13997
Adding extracted_files field to rocq.extraction stanza#13997Alizter merged 6 commits intoocaml:mainfrom
extracted_files field to rocq.extraction stanza#13997Conversation
Durbatuluk1701
force-pushed
the
rocq_extraction_improv
branch
from
eba458c to
cced9a9
Compare
|
I'm in favour of supporting more extractions features of Rocq, however I think we should think a bit harder about reducing the fields in the extraction stanza. I think guarding the We don't do such upgrades for the rest of dune lang, however until rocq lang is considered stable, I think its fine to make it better. @rlepigre-skylabs-ai I would like to get your input on this also. |
Signed-off-by: Will Thomas <30wthomas@gmail.com>
…`, duplicate rocq.extraction files warning instead of error Signed-off-by: Will Thomas <30wthomas@gmail.com>
Durbatuluk1701
force-pushed
the
rocq_extraction_improv
branch
3 times, most recently
from
8b02d9b to
3d4d5b6
Compare
…tracted_modules for version 0.13 Signed-off-by: Will Thomas <30wthomas@gmail.com>
Durbatuluk1701
force-pushed
the
rocq_extraction_improv
branch
from
3d4d5b6 to
d7d8744
Compare
rlepigre-skylabs-ai
left a comment
rlepigre-skylabs-ai
left a comment
There was a problem hiding this comment.
This seems fine to me, but I've not used extraction very much myself. It might be good to check with other users.
|
|
||
| - ``(extracted_files <filenames>)`` is a list of filenames (with extensions) | ||
| that will be produced by the extraction. This allows extraction to languages | ||
| other than OCaml, such as Haskell (``.hs``) or Scheme (``.scm``). Available |
There was a problem hiding this comment.
We have a since field somewhere in the docs. That should be used when describing this field.
There was a problem hiding this comment.
I couldn't exactly find a since field, but maybe what I ended up doing is what you intended?
There was a problem hiding this comment.
Sorry, my memory this morning was very poor, its
.. versionadded:: 3.23
|
|
||
| - ``(extracted_modules <names>)`` is an exhaustive list of OCaml modules | ||
| extracted. | ||
| - ``(extracted_modules <names>)`` specifies the OCaml modules to be extracted. |
There was a problem hiding this comment.
I would put the information about upgrading in this section, and move this section below.
| Rocq may be instructed to *extract* sources as part of the compilation | ||
| process by using the ``rocq.extraction`` stanza: | ||
|
|
||
| For ``(rocq 0.12)`` and below: |
There was a problem hiding this comment.
Let's only keep the new version otherwise it risks being confusing.
There was a problem hiding this comment.
i.e. don't repeat the stanza, just show the new version.
There was a problem hiding this comment.
I moved info about extracted_modules into a note, because it felt a bit orphaned now
…fixes Signed-off-by: Will Thomas <30wthomas@gmail.com>
Signed-off-by: Will Thomas <30wthomas@gmail.com>
This is a good idea, topic opened up here |
|
Needs a changelog entry |
Signed-off-by: Will Thomas <30wthomas@gmail.com>
3 participants
This PR adds an
extracted_filesfield to therocq.extractionstanza. In particular, this field is used to specify files that should be produced by extraction other than those purely meant for OCaml extraction (the currentextracted_modulesfield behavior).The primary motivation for this is the following behavior: given a Rocq extraction prelude
X.vthat extracts to Haskell and produces a fileX.hs, a singledune buildwill produce this file, but subsequentdune buildwill wipe theX.hsfrom_build/....This behavior is mitigated by this PR and specifically witnessed by the
Test rebuild does not clean extracted files:test intest/blackbox-tests/test-cases/rocq/extraction/extracted-files.tIt is my belief that the
extracted_filesstanza could subsumeextracted_modules:(extracted_modules F1 ... FN) --> (extracted_files F1.ml F1.mli ... FN.ml FN.mli), however for compatibility I did not do this, although maybe it is worth discussing.