Skip to content

fix: dune files from source tree#6585

Merged
rgrinberg merged 1 commit intomainfrom
ps/rr/fix__dune_files_from_source_tree
Nov 26, 2022
Merged

fix: dune files from source tree#6585
rgrinberg merged 1 commit intomainfrom
ps/rr/fix__dune_files_from_source_tree

Conversation

@rgrinberg
Copy link
Copy Markdown
Member

The dune file path returned by Source_tree.Dune_file is always present.
This is wrong because some dune files are generated using subdir. This
commit tweaks the API to reflect this fact and updates the rest of the
code to handle such virtual dune files.

Signed-off-by: Rudi Grinberg me@rgrinberg.com

ps-id: b2dfc4df-ea48-491c-987e-b9b3d193e597

@rgrinberg rgrinberg requested a review from anmonteiro November 26, 2022 07:02
@rgrinberg rgrinberg mentioned this pull request Nov 26, 2022
Copy link
Copy Markdown
Collaborator

@anmonteiro anmonteiro left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks, this is a lot better than #6584.

  • Added an optional suggestion
  • TODOs to be fixed later?

Comment on lines +560 to +562
match file_exists with
| None -> None
| Some fname -> Some (Path.Source.relative path fname)
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
match file_exists with
| None -> None
| Some fname -> Some (Path.Source.relative path fname)
Option.map file_exists ~f:Path.Source.relative path

@rgrinberg
Copy link
Copy Markdown
Member Author

The TODOs will indeed to be addressed later.

The dune file path returned by Source_tree.Dune_file is always present.
This is wrong because some dune files are generated using subdir. This
commit tweaks the API to reflect this fact and updates the rest of the
code to handle such virtual dune files.

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

ps-id: b2dfc4df-ea48-491c-987e-b9b3d193e597
@rgrinberg rgrinberg force-pushed the ps/rr/fix__dune_files_from_source_tree branch from 986c099 to e912144 Compare November 26, 2022 07:15
@rgrinberg rgrinberg merged commit a790dd3 into main Nov 26, 2022
@Alizter Alizter deleted the ps/rr/fix__dune_files_from_source_tree branch November 26, 2022 14:46
moyodiallo pushed a commit to moyodiallo/dune that referenced this pull request Dec 2, 2022
The dune file path returned by Source_tree.Dune_file is always present.
This is wrong because some dune files are generated using subdir. This
commit tweaks the API to reflect this fact and updates the rest of the
code to handle such virtual dune files.

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants