From 762c3bcbe1a6df9e0b0d69046f943264e2db6106 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Wed, 2 Oct 2024 13:31:04 -0700
Subject: [PATCH] Util: fix mkdir for trailing slashes

When calling F* as in
```
$ fstar.exe --cache_dir a/b/
wrong argument given to option `cache_dir`
```
when `a` does not yet exist, F* is supposed to attempt to create the
directory, but it fails due to the trailing slash. The problem is that
when mkdir raises an ENOENT, we attempt to create parent directories,
but we are computing the parent of 'a/b/' to be 'a/b' (since we naively
removed the last slash component). So the process is:

- Try to mkdir a/b/, get ENOENT
- Try to mkdir a/b, get ENOENT
- Try to mkdir a, works
- Retry mkdir a/b, works
- Retry mkdir a/b/, fails since it already exists.

This fixes the problem ignoring trailing slashes. Moving to a full,
F*-based filename library would be a lot better.
---
 ocaml/fstar-lib/FStar_Compiler_Util.ml | 18 +++++++++++++++---
 1 file changed, 15 insertions(+), 3 deletions(-)

diff --git a/ocaml/fstar-lib/FStar_Compiler_Util.ml b/ocaml/fstar-lib/FStar_Compiler_Util.ml
index a6470961837..5f1d5bb4600 100644
--- a/ocaml/fstar-lib/FStar_Compiler_Util.ml
+++ b/ocaml/fstar-lib/FStar_Compiler_Util.ml
@@ -866,9 +866,21 @@ let concat_dir_filename d f = Filename.concat d f
 let slash_code : int =
   BatUChar.code (BatUChar.of_char '/')
 
+let rec dropWhile f xs =
+  match xs with
+  | [] -> []
+  | x::xs ->
+    if f x
+    then dropWhile f xs
+    else x::xs
+
 let path_parent (fn : string) : string =
-    let cs = FStar_String.split [slash_code] fn in
-    FStar_String.concat "/" (FStar_List.init cs)
+  let cs = FStar_String.split [slash_code] fn in
+  (* ^ Components of the path *)
+  let cs = cs |> List.rev |> dropWhile (fun s -> s = "") |> List.rev in
+  (* ^ Remove empty trailing components, so we interpret a/b/c/ as a/b/c *)
+  (* Remove last component to get parent and concat. *)
+  FStar_String.concat "/" (FStar_List.init cs)
 
 let rec __mkdir clean mkparents nm =
   let remove_all_in_dir nm =
@@ -883,7 +895,7 @@ let rec __mkdir clean mkparents nm =
   | Unix_error (EEXIST, _, _) ->
     if clean then remove_all_in_dir nm
 
-  (* failed due to existing directory, mkparents is true, and nm has a slash:
+  (* failed due to nonexisting directory, mkparents is true, and nm has a slash:
       attempt to recursively create parent and retry. *)
   | Unix_error (ENOENT, _, _) when mkparents && FStar_String.index_of nm slash_code <> (Z.of_int (-1)) ->
     __mkdir false true (path_parent nm);