search

abella-prover / abella

An interactive theorem prover based on lambda-tree syntax
https://abella-prover.org/
GNU General Public License v3.0
89 stars 18 forks source link

Automatically compile Import does not work properly on Windows #115

Open JimmyZJX opened 5 years ago

JimmyZJX commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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

chaudhuri commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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