diff --git a/virage/pom.xml b/virage/pom.xml
index 426fc4c..8994d5c 100644
--- a/virage/pom.xml
+++ b/virage/pom.xml
@@ -41,11 +41,17 @@
UTF-8
UTF-8
3.8.1
- 11
- 11
- 11
- 11
- edu.kit.kastel.formal.virage.core.VirageMain
+ 3.3.1
+ 3.1.1
+ 3.3.0
+ 17
+ 17
+ 17
+ 17
+ 2.20.0
+ 4.7.3
+ /usr/lib/swi-prolog
+ edu.kit.kastel.formal.virage.core.VirageMain
@@ -83,18 +89,23 @@
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}
com.github.SWI-Prolog
packages-jpl
- V9.1.7
+ V9.1.14
@@ -105,12 +116,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 +136,7 @@
org.apache.commons
commons-configuration2
- 2.8.0
+ 2.9.0
commons-beanutils
@@ -181,7 +192,7 @@
org.apache.maven.plugins
maven-enforcer-plugin
- 3.2.1
+ 3.4.0
enforce-versions
@@ -205,14 +216,14 @@
3.2.4 package
shade
- edu.kit.kastel.formal.virage.core.VirageMain
+ ${main.class}
true -->
org.codehaus.mojo
versions-maven-plugin
- 2.15.0
+ 2.16.0
file:///${basedir}/rules.xml
false
@@ -220,6 +231,7 @@
+ versions-display
compile
display-dependency-updates
@@ -231,10 +243,11 @@
org.codehaus.mojo
properties-maven-plugin
- 1.1.0
+ 1.2.0
- process-resources
+ read-settings
+ initialize
read-project-properties
@@ -253,7 +266,7 @@
org.apache.maven.plugins
maven-surefire-plugin
- 3.0.0
+ 3.1.2
@@ -266,21 +279,24 @@
3.1.0
- test
+ execute
+
+ exec
+
- edu.kit.kastel.formal.virage.core.VirageMain
-
- ${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
+
@@ -289,12 +305,12 @@
org.apache.maven.plugins
maven-clean-plugin
- 3.2.0
+ ${maven.clean.version}
org.apache.maven.plugins
maven-resources-plugin
- 3.3.0
+ ${maven.clean.version}
org.apache.maven.plugins
@@ -304,17 +320,24 @@
org.apache.maven.plugins
maven-jar-plugin
- 3.3.0
+ ${maven.jar.version}
+
+
+
+ ${main.class}
+
+
+
org.apache.maven.plugins
maven-install-plugin
- 3.1.0
+ ${maven.install.version}
org.apache.maven.plugins
maven-deploy-plugin
- 3.1.0
+ ${maven.install.version}
org.apache.maven.plugins
@@ -327,14 +350,13 @@
org.apache.maven.plugins
maven-checkstyle-plugin
- 3.2.1
+ ${maven.jar.version}
false
true
true
true
checks.xml
- UTF-8
true
true
false
@@ -343,14 +365,14 @@
com.puppycrawl.tools
checkstyle
- 10.9.2
+ 10.12.3
com.github.spotbugs
spotbugs-maven-plugin
- 4.7.3.2
+ ${spotbugs.version}.5
true
false
@@ -366,7 +388,7 @@
com.github.spotbugs
spotbugs
- 4.7.3
+ ${spotbugs.version}
@@ -378,7 +400,7 @@
org.apache.maven.plugins
maven-project-info-reports-plugin
- 3.4.2
+ 3.4.5
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 6a3532b..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
@@ -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,24 @@ 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 ProcessUtils.Output output = ProcessUtils.runTerminatingProcess(proc);
+ final String result = output.stdOut.isEmpty() ? output.stdErr : output.stdOut;
+ return result.isEmpty() ? none : result;
+ }
+
/**
* Checks whether all external software is available and prints the version numbers of said
* software.
@@ -233,12 +251,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 +265,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 +320,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 +387,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 +412,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 +502,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 +515,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 +539,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 +581,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 +645,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 +734,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();
@@ -747,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();
}
@@ -789,8 +803,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..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;
@@ -232,7 +230,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"
@@ -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/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..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.
@@ -134,7 +138,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();
@@ -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();
@@ -175,7 +181,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 +352,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) {
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