Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Provide a copy_files_rec version of copy_files #11182

Open
rlepigre opened this issue Dec 3, 2024 · 1 comment
Open

Provide a copy_files_rec version of copy_files #11182

rlepigre opened this issue Dec 3, 2024 · 1 comment

Comments

@rlepigre
Copy link
Contributor

rlepigre commented Dec 3, 2024

Desired Behavior

Assume I have a directory structure like the following, with files with the .d and .v extension:

a
├── a.d
├── a.v
├── b
│   ├── ab.d
│   ├── ab.v
│   └── c
│       ├── abc.d
│       └── abc.v
└── d
    ├── ad.d
    └── ad.v

Now, I would like to be able to do something like:

(subdir gen
 (copy_files_rec
  (files ../a/**.v)))

so that dune effectively copies all files with the .v extension in directory a into the directory gen.

Additionally, I would also like to have the option to preserve the directory structure when doing the copy (i.e., files like gen/a/b/c/abc.v would be produced). This would be very useful in combination with (include_subdirs qualified) in the context of Coq projects.

Example

For example, I would expect the following to work.

mkdir -p a/b/c a/d
touch a/a.v a/b/ab.v a/b/c/abc.v a/d/ad.v
touch a/a.d a/b/ab.d a/b/c/abc.d a/d/ad.d

echo "(lang dune 3.18)" > dune-project
cat > dune <<<EOF
(subdir gen_flat
 (copy_files_rec
  (files ../a/**.v)))

(subdir gen_flat
 (copy_files_rec
  (files ../a/**.v)
  (preserve_dir_structure)))
EOF
@rlepigre
Copy link
Contributor Author

rlepigre commented Dec 3, 2024

Note that this is related to #3387, but slightly different.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants