Description:
Like many Linux users, several subdirectories of my $HOME are symbolic links to directories that live on a separate data partition. This is used to keep a consistent workspace across distros. This also means that every file in my various projects has two separate paths which alias to the same file; for example:
~/src/tlaplus/java-tools/tlatools/org.lamport.tlatools/test/tla2sany/semantic/error_corpus/E4200_Test.tla/mnt/data/src/tlaplus/java-tools/tlatools/org.lamport.tlatools/test/tla2sany/semantic/error_corpus/E4200_Test.tla
When I open the /mnt-prefixed directory in VS Code then run the "Parse TLA+" command, it works fine - the error is underlined in red in the file. However, when I open the ~/-prefixed symlink directory in VS Code then run the "Parse TLA+" command, the SANY output pane shows the expected error but no error underlining occurs. Presumably this is because the VS Code extension works with the /mnt-prefixed path and does not think the current ~/-prefixed buffer is the actual file containing the error.
This is the latest in a growing list of development tooling issues I've run into when using symlinked directories in this way; one starts to wonder at the point of it all:
Steps to reproduce:
On a unix-like OS, use the ln command to create a symbolic link for a directory; I believe the command is ln -s /mnt/actual_tla_src_dir /home/username/symbolic_tla_src_dir (people always mix up the source and target order here). Then open the symbolic TLA+ source dir in VS Code, create a TLA+ file containing a parse error, and run "Parse TLA+".
Expectations:
I expected the extension to still use red parse error underlining when operating within a symbolically-linked directory.
Version Information:
- Plugin Version: 2026.1.161649
- OS: Arch Linux
Description:
Like many Linux users, several subdirectories of my
$HOMEare symbolic links to directories that live on a separate data partition. This is used to keep a consistent workspace across distros. This also means that every file in my various projects has two separate paths which alias to the same file; for example:~/src/tlaplus/java-tools/tlatools/org.lamport.tlatools/test/tla2sany/semantic/error_corpus/E4200_Test.tla/mnt/data/src/tlaplus/java-tools/tlatools/org.lamport.tlatools/test/tla2sany/semantic/error_corpus/E4200_Test.tlaWhen I open the
/mnt-prefixed directory in VS Code then run the "Parse TLA+" command, it works fine - the error is underlined in red in the file. However, when I open the~/-prefixed symlink directory in VS Code then run the "Parse TLA+" command, the SANY output pane shows the expected error but no error underlining occurs. Presumably this is because the VS Code extension works with the/mnt-prefixed path and does not think the current~/-prefixed buffer is the actual file containing the error.This is the latest in a growing list of development tooling issues I've run into when using symlinked directories in this way; one starts to wonder at the point of it all:
Steps to reproduce:
On a unix-like OS, use the
lncommand to create a symbolic link for a directory; I believe the command isln -s /mnt/actual_tla_src_dir /home/username/symbolic_tla_src_dir(people always mix up the source and target order here). Then open the symbolic TLA+ source dir in VS Code, create a TLA+ file containing a parse error, and run "Parse TLA+".Expectations:
I expected the extension to still use red parse error underlining when operating within a symbolically-linked directory.
Version Information: