diff --git a/virage/pom.xml b/virage/pom.xml index ca52502..8994d5c 100644 --- a/virage/pom.xml +++ b/virage/pom.xml @@ -41,11 +41,17 @@ UTF-8 UTF-8 3.8.1 + 3.3.1 + 3.1.1 + 3.3.0 17 17 17 17 - edu.kit.kastel.formal.virage.core.VirageMain + 2.20.0 + 4.7.3 + /usr/lib/swi-prolog + edu.kit.kastel.formal.virage.core.VirageMain @@ -83,12 +89,17 @@ org.apache.logging.log4j log4j-api - 2.20.0 + ${log4j.version} org.apache.logging.log4j log4j-core - 2.20.0 + ${log4j.version} + + + org.apache.logging.log4j + log4j-slf4j-impl + ${log4j.version} @@ -205,7 +216,7 @@ 3.2.4 package shade - ${exec.mainClass} + ${main.class} true --> @@ -220,6 +231,7 @@ + versions-display compile display-dependency-updates @@ -235,7 +247,7 @@ read-settings - process-resources + initialize read-project-properties @@ -267,21 +279,24 @@ 3.1.0 - test + execute + + exec + - ${exec.mainClass} - - ${SWI_PROLOG_LIBSWIPL_PATH} - ${SWI_PROLOG_LIBRARIES_PATH} - java + ${main.class} -classpath - edu.kit.kastel.formal.virage.core.VirageMain + ${main.class} + + ${swi.home.dir} + ${swi.home.dir}/lib/x86_64-linux/libswipl.so + @@ -290,12 +305,12 @@ org.apache.maven.plugins maven-clean-plugin - 3.3.1 + ${maven.clean.version} org.apache.maven.plugins maven-resources-plugin - 3.3.1 + ${maven.clean.version} org.apache.maven.plugins @@ -305,11 +320,11 @@ org.apache.maven.plugins maven-jar-plugin - 3.3.0 + ${maven.jar.version} - ${exec.mainClass} + ${main.class} @@ -317,12 +332,12 @@ org.apache.maven.plugins maven-install-plugin - 3.1.1 + ${maven.install.version} org.apache.maven.plugins maven-deploy-plugin - 3.1.1 + ${maven.install.version} org.apache.maven.plugins @@ -335,7 +350,7 @@ org.apache.maven.plugins maven-checkstyle-plugin - 3.3.0 + ${maven.jar.version} false true @@ -357,7 +372,7 @@ com.github.spotbugs spotbugs-maven-plugin - 4.7.3.5 + ${spotbugs.version}.5 true false @@ -373,7 +388,7 @@ com.github.spotbugs spotbugs - 4.7.3 + ${spotbugs.version} diff --git a/virage/src/main/java/edu/kit/kastel/formal/util/ProcessUtils.java b/virage/src/main/java/edu/kit/kastel/formal/util/ProcessUtils.java index a0c29c2..602f6ae 100644 --- a/virage/src/main/java/edu/kit/kastel/formal/util/ProcessUtils.java +++ b/virage/src/main/java/edu/kit/kastel/formal/util/ProcessUtils.java @@ -18,16 +18,16 @@ public class ProcessUtils { private static final Logger LOGGER = LogManager.getLogger(ProcessUtils.class); /** - * Executes a terminating command and logs it outputs, stderr foing to logger.warn(), stdout to - * logger.info(). Does not return if the command is non-terminating! + * Executes a terminating command and prints its output to System.out/System.err, respectively. + * Does not return if the command is non-terminating! * * @param command the command to be executed (as is, i.e. the String has to contain all * parameters etc.) - * @return the exit code (usually 0 on success, but depending on the command) + * @return a Pair of strings representing stdout and stderr of the process * @throws IOException if reading the outputs fails * @throws InterruptedException if command execution is interrupted */ - public static int runTerminatingProcessAndLogOutput(final String command) + public static Output runTerminatingProcess(final String command) throws IOException, InterruptedException { final Runtime rt = Runtime.getRuntime(); @@ -37,19 +37,12 @@ public static int runTerminatingProcessAndLogOutput(final String command) final String stdErr = new String(p.getErrorStream().readAllBytes(), StandardCharsets.UTF_8); final String stdOut = new String(p.getInputStream().readAllBytes(), StandardCharsets.UTF_8); - if (!stdErr.isEmpty()) { - LOGGER.warn(stdErr); - } - if (!stdOut.isEmpty()) { - LOGGER.info(stdOut); - } - - return status; + return new Output(stdOut, stdErr, status); } /** - * Executes a terminating command and prints its output to System.out/System.err, respectively. - * Does not return if the command is non-terminating! + * Executes a terminating command and logs it outputs, stderr going to logger.warn(), stdout to + * logger.info(). Does not return if the command is non-terminating! * * @param command the command to be executed (as is, i.e. the String has to contain all * parameters etc.) @@ -57,24 +50,16 @@ public static int runTerminatingProcessAndLogOutput(final String command) * @throws IOException if reading the outputs fails * @throws InterruptedException if command execution is interrupted */ - public static int runTerminatingProcessAndPrintOutput(final String command) + public static int runTerminatingProcessAndLogOutput(final String command) throws IOException, InterruptedException { - final Runtime rt = Runtime.getRuntime(); - - final Process p = rt.exec(StringUtils.stripAndEscape(command)); - final int status = p.waitFor(); - - final String stdErr = new String(p.getErrorStream().readAllBytes(), StandardCharsets.UTF_8); - final String stdOut = new String(p.getInputStream().readAllBytes(), StandardCharsets.UTF_8); - - if (!stdErr.isEmpty()) { - System.err.print(stdErr); + final Output output = runTerminatingProcess(command); + if (!output.stdErr.isEmpty()) { + LOGGER.warn(output.stdErr); } - if (!stdOut.isEmpty()) { - System.out.print(stdOut); + if (!output.stdOut.isEmpty()) { + LOGGER.info(output.stdOut); } - - return status; + return output.status; } /** @@ -83,20 +68,54 @@ public static int runTerminatingProcessAndPrintOutput(final String command) * * @param command the command to be executed (as is, i.e. the String has to contain all * parameters etc.) - * @return a Pair of strings representing stdout and stderr of the process + * @return the exit code (usually 0 on success, but depending on the command) * @throws IOException if reading the outputs fails * @throws InterruptedException if command execution is interrupted */ - public static Pair runTerminatingProcess(final String command) + public static int runTerminatingProcessAndPrintOutput(final String command) throws IOException, InterruptedException { - final Runtime rt = Runtime.getRuntime(); - - final Process p = rt.exec(StringUtils.stripAndEscape(command)); - p.waitFor(); - - final String stdErr = new String(p.getErrorStream().readAllBytes(), StandardCharsets.UTF_8); - final String stdOut = new String(p.getInputStream().readAllBytes(), StandardCharsets.UTF_8); + final Output output = runTerminatingProcess(command); + if (!output.stdErr.isEmpty()) { + System.err.print(output.stdErr); + } + if (!output.stdOut.isEmpty()) { + System.out.print(output.stdOut); + } + return output.status; + } - return new Pair(stdOut, stdErr); + /** + * The static data structure to store the text from the standard output and the error output + * stream as well as the integer status value. + * + * @author VeriVote + */ + public static class Output { + /** + * The standard output stream as a string. + */ + public final String stdOut; + /** + * The error output stream as a string. + */ + public final String stdErr; + /** + * The status output as an integer value. + */ + public final int status; + + /** + * Constructor method for the static data structure to store the text from the standard + * output and the error output stream as well as the integer status value. + * + * @param outStream The standard output stream as a string. + * @param errStream The error output stream as a string. + * @param statusValue The status output as an integer value. + */ + public Output(final String outStream, final String errStream, final int statusValue) { + stdOut = outStream; + stdErr = errStream; + status = statusValue; + } } } diff --git a/virage/src/main/java/edu/kit/kastel/formal/util/SystemUtils.java b/virage/src/main/java/edu/kit/kastel/formal/util/SystemUtils.java index 6ee726d..64607c7 100644 --- a/virage/src/main/java/edu/kit/kastel/formal/util/SystemUtils.java +++ b/virage/src/main/java/edu/kit/kastel/formal/util/SystemUtils.java @@ -7,7 +7,7 @@ import java.lang.reflect.Field; import java.nio.charset.StandardCharsets; import java.nio.file.Files; -import java.time.LocalDateTime; +import java.time.ZonedDateTime; import java.time.format.DateTimeFormatter; import java.util.Map; @@ -67,13 +67,12 @@ public static void addDirToLibraryPath(final String s) throws IOException { } /** - * Returns current time (yyyy-MM-dd HH:mm:ss). + * Returns current time (yyyy-MM-dd HH:mm:ss OOOO). * @return the time */ public static String getTime() { - final DateTimeFormatter dtf = DateTimeFormatter.ofPattern("yyyy-MM-dd HH:mm:ss"); - final LocalDateTime now = LocalDateTime.now(); - + final DateTimeFormatter dtf = DateTimeFormatter.ofPattern("yyyy-MM-dd HH:mm:ss OOOO"); + final ZonedDateTime now = ZonedDateTime.now(); return dtf.format(now); } diff --git a/virage/src/main/java/edu/kit/kastel/formal/virage/core/ConfigReader.java b/virage/src/main/java/edu/kit/kastel/formal/virage/core/ConfigReader.java index 12f6522..4b4753a 100644 --- a/virage/src/main/java/edu/kit/kastel/formal/virage/core/ConfigReader.java +++ b/virage/src/main/java/edu/kit/kastel/formal/virage/core/ConfigReader.java @@ -233,8 +233,9 @@ private static String getCommandOutput(final String command, final String option throws IOException, InterruptedException { final String none = "" + '\n'; final String proc = command + " " + option; - final String output = ProcessUtils.runTerminatingProcess(proc).getFirstValue(); - return output.isEmpty() ? none : output; + final ProcessUtils.Output output = ProcessUtils.runTerminatingProcess(proc); + final String result = output.stdOut.isEmpty() ? output.stdErr : output.stdOut; + return result.isEmpty() ? none : result; } /** @@ -758,7 +759,9 @@ public void readConfigFile(final boolean overwriteIfNecessary) throws IOExceptio final File virageDir = new File(virageFolderPath); this.configFile = new File(configPath); if (!this.configFile.exists()) { - Files.createDirectory(virageDir.toPath()); + if (!virageDir.exists()) { + Files.createDirectory(virageDir.toPath()); + } Files.createFile(this.configFile.toPath()); this.copyConfigToExpectedPath(); } diff --git a/virage/src/main/java/edu/kit/kastel/formal/virage/core/VirageCommandLineInterface.java b/virage/src/main/java/edu/kit/kastel/formal/virage/core/VirageCommandLineInterface.java index a1670fd..4d422b2 100644 --- a/virage/src/main/java/edu/kit/kastel/formal/virage/core/VirageCommandLineInterface.java +++ b/virage/src/main/java/edu/kit/kastel/formal/virage/core/VirageCommandLineInterface.java @@ -8,8 +8,6 @@ import java.io.StringWriter; import java.io.Writer; import java.nio.charset.StandardCharsets; -import java.time.LocalDateTime; -import java.time.format.DateTimeFormatter; import java.util.ArrayList; import java.util.Collections; import java.util.LinkedList; @@ -699,10 +697,9 @@ private void printSettings() { } private void printTimestamp() { - final DateTimeFormatter dtf = DateTimeFormatter.ofPattern("yyyy-MM-dd HH:mm:ss"); - final LocalDateTime now = LocalDateTime.now(); + final String now = SystemUtils.getTime(); this.displayMessage(HEADER_LINE_START + "Version " + VirageCore.getVersion() - + ", Timestamp: " + dtf.format(now)); + + ", Timestamp: " + now); this.displayMessage(HEADER_LINE_START + "If you need help, type \"help\", \"h\" or \"?\"."); this.displayMessage(HEADER_LINE_START + "To exit ViRAGe, type \"exit\"."); } diff --git a/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/ScalaIsabelleFacade.java b/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/ScalaIsabelleFacade.java index ecd2c99..f4aecff 100644 --- a/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/ScalaIsabelleFacade.java +++ b/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/ScalaIsabelleFacade.java @@ -112,14 +112,18 @@ public ScalaIsabelleFacade(final String sessionDirValue, final String sessionNam final List sessionDirs = new LinkedList(); sessionDirs.add(Path.of(this.sessionDir)); - - this.setup = new Setup(Path.of(ConfigReader.getInstance().getIsabelleHome()), - sessionNameValue, - new Some(Path.of(ConfigReader.getInstance().getIsabelleSessionDir())), - Path.of(sessionDirValue), - JavaConverters.asScalaIteratorConverter(sessionDirs.iterator()).asScala().toSeq(), - true, true /*try verbose first*/, null, null /* try to get away with null first */); - + final String isabelleHome = ConfigReader.getInstance().getIsabelleHome(); + this.setup = // JIsabelle.setupSetBuild(true, JIsabelle.setup(Path.of(isabelleHome))); + new Setup(Path.of(isabelleHome), + sessionNameValue, + new Some( + Path.of(ConfigReader.getInstance().getIsabelleSessionDir())), + Path.of(sessionDirValue), + JavaConverters.asScalaIteratorConverter( + sessionDirs.iterator()).asScala().toSeq(), + true, true /*try verbose first*/, + (Isabelle i) -> i.exceptionManager(), + null /* try to get away with null first */); try { isabelle = new Isabelle(this.setup); // Scala has no checked Exceptions and the constructor is not annotated. @@ -158,13 +162,15 @@ public static void buildSession(final String sessionDir, final String sessionNam final List sessionDirs = new LinkedList(); sessionDirs.add(Path.of(new File(sessionDir).getAbsolutePath())); - final Setup setup = new Setup(Path.of(ConfigReader.getInstance().getIsabelleHome()), - sessionName, - new Some(Path.of(ConfigReader.getInstance().getIsabelleSessionDir())), - Path.of(sessionDir), - JavaConverters.asScalaIteratorConverter(sessionDirs.iterator()).asScala().toSeq(), - true, true /*try verbose first*/, null, null /* try to get away with null first */); - + final Setup setup = + new Setup(Path.of(ConfigReader.getInstance().getIsabelleHome()), + sessionName, + new Some(Path.of(ConfigReader.getInstance().getIsabelleSessionDir())), + Path.of(sessionDir), + JavaConverters.asScalaIteratorConverter(sessionDirs.iterator()) + .asScala().toSeq(), + true, true /*try verbose first*/, (Isabelle i) -> i.exceptionManager(), + null /* try to get away with null first */); try { isabelle = new Isabelle(setup); isabelle.destroy(); diff --git a/virage/src/main/resources/settings b/virage/src/main/resources/settings index cf031f5..ba54cb3 100644 --- a/virage/src/main/resources/settings +++ b/virage/src/main/resources/settings @@ -1,4 +1,4 @@ -TIMESTAMP= +TIMESTAMP=2023-09-01 00:00:00 GMT+02:00 # This value is used for internal consistency checks, please do not alter it! VIRAGE_CONFIG_VERSION=0.1.0 @@ -13,11 +13,11 @@ GCC_EXECUTABLE=gcc SWI_PROLOG_EXECUTABLE=swipl # Path to libswipl.so -SWI_PROLOG_LIBSWIPL_PATH= +SWI_PROLOG_LIBSWIPL_PATH=/usr/lib/swi-prolog/lib/x86_64-linux/libswipl.so # Path to the SWI-Prolog library (usually, $SWI_HOME_DIR/lib/$ARCHITECTURE # should contain libjpl.so, otherwise install swi-prolog-java) -SWI_PROLOG_LIBRARIES_PATH= +SWI_PROLOG_LIBRARIES_PATH=/usr/lib/swi-prolog/lib/x86_64-linux/ ## System settings @@ -28,7 +28,7 @@ SYSTEM_DEFAULT_OUTPUT_PATH=./target/generated-sources/ # Custom text editor (only used when xdg-open fails; if empty, environment # variable $EDITOR is used). -SYSTEM_TEXT_EDITOR= +SYSTEM_TEXT_EDITOR=/usr/bin/kate ## Isabelle settings