Fix Path bug

[wadoon]

Related Issue

Type of pull request

• Bug fix (non-breaking change which fixes an issue)

Ensuring quality

• I have tested the feature as follows: manually, as it does not appear in the test cases.

[unp1]

Thanks. One question, is the filesystem is closed automatically when the path becomes garbage collected?

[wadoon]

Thanks. One question, is the filesystem is closed automatically when the path becomes garbage collected?

The file systems are kept open, and should be closed after the program exists.

In the previous version, the ZipFileSystem was closed after every include, but this just cost performance. ZipFileSystem holds an internal map of opened file systems.

For JAR files, I think this behavior is acceptable. Nobody should alter or delete them anyway when KeY is running. For proof bundle, this looks different.

[WolframPfeifer]

Thanks. One question, is the filesystem is closed automatically when the path becomes garbage collected?

The file systems are kept open, and should be closed after the program exists.

In the previous version, the ZipFileSystem was closed after every include, but this just cost performance. ZipFileSystem holds an internal map of opened file systems.

For JAR files, I think this behavior is acceptable. Nobody should alter or delete them anyway when KeY is running. For proof bundle, this looks different.

Are you sure that this is a good idea? Does this not also prevent concurrent read access (because the file system throws a FileSystemAlreadyExistsException), for example if KeY is started twice from the same jar file? The latter is a not too uncommon use case imo.

Proof Bundles are not relevant here, since they are always extracted into a temporary directory first before reading from it. The possibility to alter a bundle (e.g. adding more proofs or changing them) is currently not implemented.