Migration to java.nio.Path

[wadoon]

Merging main into weigl/key-javaparser3 gets more and more complicated. One reason is the usage of java.nio.Path on the JavaParser branch.

This PR brings the java.nio.Path into KeY exhaustively for the following reason:

• Final goal of FileRepo removal and easier handling of proof bundles.

  Java NIO supports reading and writing to Zip files directly w/o unzipping as a regular file system.

• Uniform usage of one file API across KeY.

  Currently it is a mess between the old java.io.File and java.nio.Path. The latter one supports common functionalities like recursively listing directories or globbing folders.

Intended Change

On all major places, Java NIO replaces the old Java IO.

Type of pull request

• Refactoring (behaviour should not change or only minimally change)
• Breaking change (fix or feature that would cause existing functionality to change)
• There are changes to the (Java) code

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I have tested the feature as follows: test cases

[Drodt]

Seems like good progress.

Do you want to remove all uses of java.io.File?

[wadoon]

Do you want to remove all uses of java.io.File?

In general, I would say that the usage of java.io.File should be discouraged. For this PR, I tried to remove java.io.File from the central components, as a preparation to load proof bundles w/o unpacking in advance.

Therefore, in some smaller local cases, j.i.F might remain, e.g., the proof statistic classes which rely heavily on File and are overengineered in comparison to their purpose.

[wadoon]

@FliegendeWurst EndToEndTests in slicing fail, and I can not figure out why.

[FliegendeWurst]

Probably this method in ProofSaver

    public static void saveToFile(File file, Proof proof) throws IOException {
        saveProofObligationToFile(file.toPath(), proof);
    }

[FliegendeWurst]

This change works:

diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingProofReplayer.java b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingProofReplayer.java
index f0e150de6e..589e4b1f40 100644
--- a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingProofReplayer.java
+++ b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingProofReplayer.java
@@ -247,9 +247,9 @@ public final class SlicingProofReplayer extends AbstractProofReplayer {
             filename = filename + sliceSuffix + "1";
         }
         filename = filename + ".proof";
-        File tempFile = tempDir.resolve(filename).toFile();
+        var tempFile = tempDir.resolve(filename);
         ProofSaver.saveToFile(tempFile, proof);
         proof.dispose();
-        return tempFile.toPath();
+        return tempFile;
     }
 }

Still I would suggest to rename the method I mentioned in the last comment.

[wadoon]

@Drodt Only windows is failing in few test cases...

[Drodt]

@Drodt Only windows is failing in few test cases...

Do we have someone w/ a Windows PC who can run some manual tests?

[wadoon]

@Drodt Only windows is failing in few test cases...

Do we have someone w/ a Windows PC who can run some manual tests?

My home computer, ... so I'll take care today or tomorrow evening it. But you can still finalize the review.