system: delete_file

[perazz]

This PR is spun off #904 for clarity.

The delete_file subroutine removes a file from the filesystem.
The function ensures the file exists and is not a directory before attempting deletion.
If deletion fails due to permissions, being a directory, or other issues, an error is raised.

Some questions to discuss:

• Naming: Should this be delete, delete_file, or another name?
• Should it work on files only (current version), or should it delete directories natively (without asking), or should a logical argument be added to control this? The directory case is more complicated because it should handle either empty directories, or directories with contents, recursively.
• Should this belong in stdlib_system or stdlib_io, or elsewhere?

cc: @jvdp1 @jalvesz

[jalvesz]

Hi @perazz thanks for this PR!

Regarding the naming, I think it will depend indeed on the functionality. If deleting folders is also included then it could be delete otherwise delete_file is better to remain explicit.

Another possibility would be to leave this procedure for deleting only single files and then add another procedure for deleting a whole folder tree

I think that it makes sense to leave it in the system module as it is an OS related feature.

[perazz]

I agree with your opinion: all OSes have a similar differentiation between 3 options basically:

• delete files only (maybe with globbing)
• delete directories (empty only)
• delete entire directory trees (recursive)

So I think it makes sense to have a delete_file , and then delete_dir or delete_directory later. Note that we have is_directory, so maybe delete_directory would be more consistent with the naming.

[jvdp1]

Thank you @perazz . LGTM. I only have a minor question regarding its behaviour. I wonder if it should raise a warning, instead of an error, if the file does not exist.

[jalvesz]

LGTM @perazz Thanks for this nice addition!

[perazz]

Thank you @jalvesz @jvdp1. With two approvals, I would wait a bit longer and then merge this one.