From 458e35c0d8ee86e1be0904d23d8fbc129c6367c2 Mon Sep 17 00:00:00 2001 From: Michael Kirsten Date: Wed, 30 Aug 2023 04:02:17 +0200 Subject: [PATCH 1/3] Minor refactorings --- .../formal/virage/core/ConfigReader.java | 73 +++++++++++-------- .../core/VirageCommandLineInterface.java | 2 +- .../isabelle/IsabelleFrameworkExtractor.java | 6 +- .../virage/isabelle/ScalaIsabelleFacade.java | 6 +- 4 files changed, 50 insertions(+), 37 deletions(-) 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 6a3532b..12f6522 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 @@ -121,7 +121,7 @@ public final class ConfigReader { /** * SWI-Prolog option to dump runtime variables. */ - private static final String DUMP_RUNTIME_VARIABLES = " --dump-runtime-variables"; + private static final String DUMP_RUNTIME_VARIABLES = "--dump-runtime-variables"; /** * THe xdg-open command. Maybe only makes real sense for unix systems, but well. @@ -220,6 +220,23 @@ public static ConfigReader getInstance() { return instance; } + /** + * Short-hand method for the command output within the command line interface. + * + * @param command the given command + * @param option the option given as parameter for the command + * @return the printed command output + * @throws IOException exception in case the process yields I/O problems + * @throws InterruptedException exception in case the process is interrupted + */ + 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; + } + /** * Checks whether all external software is available and prints the version numbers of said * software. @@ -233,12 +250,9 @@ public String checkAvailabilityAndGetVersions() { // ISABELLE try { - res += "Isabelle: \t\t" - + ProcessUtils.runTerminatingProcess(this.getIsabelleExecutable() + " version") - .getFirstValue(); - res += "Scala (via Isabelle): " + ProcessUtils - .runTerminatingProcess(this.getIsabelleExecutable() + " scalac -version") - .getFirstValue(); + final String isaExec = this.getIsabelleExecutable(); + res += "Isabelle: \t\t" + getCommandOutput(isaExec, "version"); + res += "Scala (via Isabelle): " + getCommandOutput(isaExec + " scalac", "-version"); } catch (final IOException e) { res += "Isabelle: \t\tNOT FOUND\n"; this.isabelleAvailable = false; @@ -250,9 +264,8 @@ public String checkAvailabilityAndGetVersions() { // SWIPL try { - res += "SWI-Prolog: \t\t" + ProcessUtils - .runTerminatingProcess(this.properties.get(SWIPL_BIN) + " --version") - .getFirstValue(); + res += "SWI-Prolog: \t\t" + + getCommandOutput((String)this.properties.get(SWIPL_BIN), "--version"); } catch (final IOException e) { System.out.println("SWI-Prolog: NOT FOUND\n"); this.swiplAvailable = false; @@ -306,18 +319,16 @@ private Pair> checkConfigCompatibility() throws IOExceptio private String computeIsabelleHome() throws IOException, InterruptedException, ExternalSoftwareUnavailableException { - final String output = ProcessUtils - .runTerminatingProcess(this.getIsabelleExecutable() + " getenv ISABELLE_HOME") - .getFirstValue(); + final String output = + getCommandOutput(this.getIsabelleExecutable(), "getenv ISABELLE_HOME"); return output.split(KEY_VALUE_SEPARATOR)[1].trim(); } private String computeIsabelleSessionDir() throws IOException, InterruptedException, ExternalSoftwareUnavailableException { - final String output = ProcessUtils - .runTerminatingProcess(this.getIsabelleExecutable() + " getenv ISABELLE_HOME_USER") - .getFirstValue(); + final String output = + getCommandOutput(this.getIsabelleExecutable(), "getenv ISABELLE_HOME_USER"); return output.split(KEY_VALUE_SEPARATOR)[1].trim(); } @@ -375,7 +386,7 @@ public List getAdditionalProperties() { String prop = this.properties.getProperty(SESSION_SPECIFIC_ASSUMPTIONS); prop = this.replaceTypeAliases(prop); - return this.readAndSplitList(prop); + return readAndSplitList(prop); } /** @@ -400,7 +411,7 @@ public List getAtomicTypes() { String prop = this.properties.getProperty("SESSION_SPECIFIC_ATOMIC_TYPES"); prop = this.replaceTypeAliases(prop); - return this.readAndSplitList(prop); + return readAndSplitList(prop); } /** @@ -490,7 +501,7 @@ public String getIsabelleSessionDir() throws ExternalSoftwareUnavailableExceptio } public List getIsabelleTactics() { - return this.readAndSplitList(this.properties.getProperty("ISABELLE_TACTICS")); + return readAndSplitList(this.properties.getProperty("ISABELLE_TACTICS")); } public String getPathToRootFile() { @@ -503,8 +514,8 @@ public String getPathToRootFile() { */ public Map getComponentAliases() { final Map toReturn = new HashMap(); - final List pairStrings = this.readAndSplitList( - this.properties.getProperty(COMPONENT_ALIASES)); + final List pairStrings = + readAndSplitList(this.properties.getProperty(COMPONENT_ALIASES)); for(final String pairString: pairStrings) { final String[] elements = pairString.split(PAIR_SEPARATOR); @@ -527,9 +538,9 @@ public String getSwiplHome() throws ExternalSoftwareUnavailableException { if (this.swiplHome == null) { try { - final String output = ProcessUtils.runTerminatingProcess( - this.properties.getProperty(SWIPL_BIN) + DUMP_RUNTIME_VARIABLES) - .getFirstValue(); + final String output = + getCommandOutput(this.properties.getProperty(SWIPL_BIN), + DUMP_RUNTIME_VARIABLES); final String[] lines = output.split(System.lineSeparator()); String value = ""; for (final String line : lines) { @@ -569,9 +580,9 @@ public String getSwiplLib() throws ExternalSoftwareUnavailableException { if (this.swiplLib == null) { try { - final String output = ProcessUtils.runTerminatingProcess( - this.properties.getProperty(SWIPL_BIN) + DUMP_RUNTIME_VARIABLES) - .getFirstValue(); + final String output = + getCommandOutput(this.properties.getProperty(SWIPL_BIN), + DUMP_RUNTIME_VARIABLES); final String[] lines = output.split(System.lineSeparator()); String value = ""; String path = ""; @@ -633,7 +644,7 @@ public List> getTypeSynonyms() throws IllegalArgumentExcept String prop = this.properties.getProperty("SESSION_SPECIFIC_TYPE_SYNONYMS"); prop = this.replaceTypeAliases(prop); - final List typeSynonyms = this.readAndSplitList(prop); + final List typeSynonyms = readAndSplitList(prop); for (final String synonym : typeSynonyms) { final String synonymCopy = this.replaceTypeAliases(synonym); @@ -722,7 +733,7 @@ public void openConfigFileForEditing() throws ExternalSoftwareUnavailableExcepti } } - private List readAndSplitList(final String list) { + private static List readAndSplitList(final String list) { final String[] splits = list.split(LIST_SEPARATOR); final List result = new LinkedList(); @@ -789,8 +800,8 @@ private String replaceTypeAliases(final String s) { return copyOfs; } - final List replacements = this - .readAndSplitList(this.properties.getProperty(SESSION_SPECIFIC_TYPE_ALIASES)); + final List replacements = + readAndSplitList(this.properties.getProperty(SESSION_SPECIFIC_TYPE_ALIASES)); final Map replMap = new HashMap(); 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 382f600..a1670fd 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 @@ -232,7 +232,7 @@ private void setupLibswipl() { newValue = this.requestString(StringUtils.appendPeriod("Please input the path to " + LIBSWIPL_SO) + " " + "For your setup of SWI-Prolog, typical values are " - + this.addQuotationsToPath("/usr/lib/" + LIBSWIPL_SO) + "or " + + this.addQuotationsToPath("/usr/lib/" + LIBSWIPL_SO) + " or " + this.addQuotationsToPath( ConfigReader.getInstance().getSwiplLib() + LIBSWIPL_SO) + ", but" diff --git a/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/IsabelleFrameworkExtractor.java b/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/IsabelleFrameworkExtractor.java index 09e2e89..68abd8d 100644 --- a/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/IsabelleFrameworkExtractor.java +++ b/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/IsabelleFrameworkExtractor.java @@ -201,7 +201,7 @@ private String convertIsabelleToProlog(final String s) { final String copyOfs = s.strip(); - for (int i = 0; i < copyOfs.length(); i++) { + for (int i = 0; i < copyOfs.length();) { final char cur = copyOfs.charAt(i); switch (cur) { @@ -218,11 +218,11 @@ private String convertIsabelleToProlog(final String s) { if (endIdx < copyOfs.length() - 1 && copyOfs.charAt(endIdx + 1) != ')') { res += PrologPredicate.SEPARATOR; } - // Checkstyle does not like this, I think it is reasonable here. i = endIdx + 1; } else { insideBrackets = true; res += cur; + i++; } break; case ' ': @@ -232,9 +232,11 @@ private String convertIsabelleToProlog(final String s) { res += '('; insideBrackets = true; } + i++; break; default: res += cur; + i++; break; } } 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 7c2a31b..ecd2c99 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 @@ -134,7 +134,7 @@ public ScalaIsabelleFacade(final String sessionDirValue, final String sessionNam + " the session manually within Isabelle " + "might help. If the session is supposed" + " to generate documentation, " - + "texlive is required!"); + + "TeX Live is required!"); throw new IsabelleBuildFailedException(); } this.init(); @@ -175,7 +175,7 @@ public static void buildSession(final String sessionDir, final String sessionNam LOGGER.error("Building session " + sessionName + " failed. Restarting ViRAGe or building" + " the session manually within Isabelle might help. If the session is supposed" - + " to generate documentation, texlive is required!"); + + " to generate documentation, TeX Live is required!"); throw new IsabelleBuildFailedException(); } @@ -346,7 +346,7 @@ private void init() { /** * Required, as StringConverter cannot be instantiated. */ - private static class JavaStringConverter extends Converter { + private static final class JavaStringConverter extends Converter { @Override public String exnToValue(final Isabelle localIsabelle, final ExecutionContext ec) { From 56494fa00b2ba1be611f10ff7af8820ec96a75bd Mon Sep 17 00:00:00 2001 From: Michael Kirsten Date: Wed, 30 Aug 2023 04:02:33 +0200 Subject: [PATCH 2/3] More updates to pom file --- virage/pom.xml | 53 ++++++++++++++++++++++++++++---------------------- 1 file changed, 30 insertions(+), 23 deletions(-) diff --git a/virage/pom.xml b/virage/pom.xml index 426fc4c..ca52502 100644 --- a/virage/pom.xml +++ b/virage/pom.xml @@ -41,10 +41,10 @@ UTF-8 UTF-8 3.8.1 - 11 - 11 - 11 - 11 + 17 + 17 + 17 + 17 edu.kit.kastel.formal.virage.core.VirageMain @@ -94,7 +94,7 @@ com.github.SWI-Prolog packages-jpl - V9.1.7 + V9.1.14 @@ -105,12 +105,12 @@ commons-io commons-io - 2.11.0 + 2.13.0 com.fasterxml.jackson.core jackson-databind - 2.14.2 + 2.15.2 @@ -125,7 +125,7 @@ org.apache.commons commons-configuration2 - 2.8.0 + 2.9.0 commons-beanutils @@ -181,7 +181,7 @@ org.apache.maven.plugins maven-enforcer-plugin - 3.2.1 + 3.4.0 enforce-versions @@ -205,14 +205,14 @@ 3.2.4 package shade - edu.kit.kastel.formal.virage.core.VirageMain + ${exec.mainClass} true --> org.codehaus.mojo versions-maven-plugin - 2.15.0 + 2.16.0 file:///${basedir}/rules.xml false @@ -231,9 +231,10 @@ org.codehaus.mojo properties-maven-plugin - 1.1.0 + 1.2.0 + read-settings process-resources read-project-properties @@ -253,7 +254,7 @@ org.apache.maven.plugins maven-surefire-plugin - 3.0.0 + 3.1.2 @@ -270,7 +271,7 @@ - edu.kit.kastel.formal.virage.core.VirageMain + ${exec.mainClass} ${SWI_PROLOG_LIBSWIPL_PATH} ${SWI_PROLOG_LIBRARIES_PATH} @@ -289,12 +290,12 @@ org.apache.maven.plugins maven-clean-plugin - 3.2.0 + 3.3.1 org.apache.maven.plugins maven-resources-plugin - 3.3.0 + 3.3.1 org.apache.maven.plugins @@ -305,16 +306,23 @@ org.apache.maven.plugins maven-jar-plugin 3.3.0 + + + + ${exec.mainClass} + + + org.apache.maven.plugins maven-install-plugin - 3.1.0 + 3.1.1 org.apache.maven.plugins maven-deploy-plugin - 3.1.0 + 3.1.1 org.apache.maven.plugins @@ -327,14 +335,13 @@ org.apache.maven.plugins maven-checkstyle-plugin - 3.2.1 + 3.3.0 false true true true checks.xml - UTF-8 true true false @@ -343,14 +350,14 @@ com.puppycrawl.tools checkstyle - 10.9.2 + 10.12.3 com.github.spotbugs spotbugs-maven-plugin - 4.7.3.2 + 4.7.3.5 true false @@ -378,7 +385,7 @@ org.apache.maven.plugins maven-project-info-reports-plugin - 3.4.2 + 3.4.5 From 0d60d9cfa57eeb5b80f78503a42472d876daae5d Mon Sep 17 00:00:00 2001 From: Michael Kirsten Date: Sat, 2 Sep 2023 17:24:36 +0200 Subject: [PATCH 3/3] A few small fixes, mainly regarding environment variables. Still need to have a look at the call to Scala-Isabelle --- virage/pom.xml | 57 +++++++---- .../kit/kastel/formal/util/ProcessUtils.java | 97 +++++++++++-------- .../kit/kastel/formal/util/SystemUtils.java | 9 +- .../formal/virage/core/ConfigReader.java | 9 +- .../core/VirageCommandLineInterface.java | 7 +- .../virage/isabelle/ScalaIsabelleFacade.java | 36 ++++--- virage/src/main/resources/settings | 8 +- 7 files changed, 131 insertions(+), 92 deletions(-) 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