search

overturetool / vdm-vscode

Visual Studio Code extension for VDM language support
GNU General Public License v3.0
21 stars 6 forks source link

Translation to LaTeX issues for VDM files in a subdirectory #192

Open AaronBuhagiar opened 1 year ago

AaronBuhagiar commented 1 year ago

Hi,

I've been trying out the translation functionality of the VDM extension and seems to be working fine on the first attempt. Once a file has been generated it is placed in .generated/latex/(folder name)/file.tex. If I make a change in my original VDM source file and attempt to run the translation again, the old generated file is deleted but a new one is not created. Beyond this point, the translation will fail to generate any file.

In order to be able to use translation again the generated subfolder needs to be removed manually (.generated/latex/(folder name)) and the translation will work again.

This issue seems to be related to files that exist within a subdirectory of my VDM workspace. For files that are in the root folder, this issue does not occur.

I have tried this out with Word translation the same happens for files in a subdirectory.

nickbattle commented 1 year ago

Thanks for reporting this. I'm having trouble reproducing this with version 1.3.6 on Linux though. What version/OS are you using?

AaronBuhagiar commented 1 year ago

Hi Nick,

I am on Windows 10 and using version 1.3.6 of the extension.

See the gif below illustrating the example. Here I am using a lib file as an example but I was able to replicate it with any file that exists in a subdirectory of the workspace.

latex

nickbattle commented 1 year ago

Curious. OK, thank you for the GIF, which is almost identical to the test I did on Linux (even using IO.vdmsl). So it's starting to look like something strange about Windows with subfolders. Perhaps a problem with handling backslashes in filenames that include path information.

It would be interesting to try on a Mac. @leouk, are you able to try this?

I don't think the problem is in the LSP server, rather in the UI - the protocol uses canonical URIs to give file/path names.

AaronBuhagiar commented 1 year ago

Ah that's interesting. I guess it might be the difference in how the different OSes process pathing. I would be interested to see if the same issue occurs in mac although given it doesn't occur in Linux, I would suspect not.

leouk commented 1 year ago

I haven't tried yet. @AaronBuhagiar show me next time we meet and I will try on the Mac as well.

AaronBuhagiar commented 1 year ago

Hi Nick,

Tested it out on @leouk mac environment and was unable to replicate the issue. It seems that this might be exclusive to windows.

nickbattle commented 1 year ago

OK, thanks for this Aaron.