needlessly long pathnames from sessions
We have trouble with long path names. On windows, paths longer than 250 chars (or so) don't work. That's a known limitation of the win32 API.
In why3 sessions, usually the file name of the .mlw file(s) is stored like this:
<file>
<path name=".."/><path name="example.mlw"/>
...
which leads the session mechanism to look for a file name /path/to/session_file/../example.mlw
. In our case (and I think that's in fact the default in Why3), the last component of /path/to/session_file/
is in fact derived from the .mlw file and has the same name. So the real path looks more like /path/to/example/../example.mlw
.
In our use case, "example" can become quite long, so we have something like this: /path/to/really_long_example_name_with_many_components/../really_long_example_name_with_many_components.mlw
. So we would like to contract the ..
and remove one copy of the long name: /path/to/really_long_example_name_with_many_components.mlw
.
The code that constructs the path name is Sysutil.system_dependent_absolute_path
. I think this function should remove occurrences of ..
(and the parent dir). Does somebody know why it doesn't?
I recall some discussions about symlinks, but inside the same process, contracting a/../b/
to b/
should always be correct even in the presence of symlinks, and if two processes (e.g. the why3 process creating the session file and the why3 process later reading it) disagree what the prefix a/
is because of symlinks, I don't see why not contracting helps - the path ../b
is still wrong if the wrong prefix is applied, even if not contracted.
I will suggest a patch on this ticket later.