Automatically compile Import does not work properly on Windows

[JimmyZJX]

When the file is located in a directory with space in it, say "C:\Google Drive", the auto compile does not work properly. Error information like "Error: Multiple files specified as input" is shown.

[chaudhuri]

Can you run it from a directory without spaces for the time being? Our treatment of filenames is not very portable at the moment.

[JimmyZJX]

Sure. No big deal. Looking forward to the fix :)

[chaudhuri]

Jimmy, can you try out the master branch to see if the problem is fixed? I've done some light testing with a Windows 10 VM and it seems to work with directories containing spaces, but I don't know if that was the entirety of the problem. I tried it with a mingw64 cross-compiled binary from Linux -- if you compile Abella yourself in Windows you may have a different experience of which I would be curious to learn.

[JimmyZJX]

I just tested with my environment (Cygwin32+OCaml). It seems that the quote is correctly added, but there is another issue: filenames are escaped one more time per resursion. A log may look like this:

Importing from "C:\\Users\\Jimmy\\Google Drive\\decidability".
Warning: "C:\\Users\\Jimmy\\Google Drive\\decidability.thc" was compiled with a different version (2.0.7-dev) of Abella; recompiling...
Running: abella "C:\\Users\\Jimmy\\Google Drive\\decidability.thm" -o "C:\\Users\\Jimmy\\Google Drive\\decidability".out -c "C:\\Users\\Jimmy\\Google Drive\\decidability.thc".
Warning: "C:\\\\Users\\\\Jimmy\\\\Google Drive\\decidability_inst.thc" was compiled with a different version (2.0.7-dev) of Abella; recompiling...
Running: abella "C:\\\\Users\\\\Jimmy\\\\Google Drive\\decidability_inst.thm" -o "C:\\\\Users\\\\Jimmy\\\\Google Drive\\decidability_inst".out -c "C:\\\\Users\\\\Jimmy\\\\Google Drive\\decidability_inst.thc".
...
Error: Could not create "C:\\\\\\\\\\\\\\\\Users\\\\\\\\\\\\\\\\Jimmy\\\\\\\\\\\\\\\\Google Drive...

But I've tested when the dependency chain is short. Seems like when too many '\' characters occur in the path, Windows just give up lol

[chaudhuri]

Wow. OK, I clearly need to test more thoroughly. Thanks.