When "-tool mathematica" is used, the mathematica paths in ~/.keymaerax/keymaerax.conf are ignored?

[ANogin]

The code in Keymaera main function: https://github.com/LS-Lab/KeYmaeraX-release/blob/7056de7778013c51e72cc4edae0b133f9b92b2f5/keymaerax-webui/src/main/scala/edu/cmu/cs/ls/keymaerax/launcher/KeYmaeraX.scala#L161-L162 and https://github.com/LS-Lab/KeYmaeraX-release/blob/7056de7778013c51e72cc4edae0b133f9b92b2f5/keymaerax-webui/src/main/scala/edu/cmu/cs/ls/keymaerax/launcher/KeYmaeraX.scala#L168-L169 means that whenever -tool mathematica on the command line is used, the tool paths from ~/.keymaerax/keymaerax.conf are ignored and the default search path is used instead.

This seems like an unreasonable thing to do - just because the caller (in my case, rv-monitor) knows that it need Keymaera to use Mathematica, does not mean that it should be in charge of knowing where to find it in a particular installation.

Suggestion: use options ++ configFromFile(...) whether the options.contains('tool) or not, just replace the default tool with the one specified by the -tool option

[ANogin]

Actually, wait - I looked at the code for configFromFile and it already does the right thing with consulting the tool option first and using the argument as the default tool otherwise, so the right thing would probably be to just remove the if...else part in the two above code snippets and keep the existing options ++ configFromFile(...) as is.

diff --git a/keymaerax-webui/src/main/scala/edu/cmu/cs/ls/keymaerax/launcher/KeYmaeraX.scala b/keymaerax-webui/sr
index 51e539b..f522758 100644
--- a/keymaerax-webui/src/main/scala/edu/cmu/cs/ls/keymaerax/launcher/KeYmaeraX.scala
+++ b/keymaerax-webui/src/main/scala/edu/cmu/cs/ls/keymaerax/launcher/KeYmaeraX.scala
@@ -157,16 +157,12 @@ object KeYmaeraX {
       } else if (options.get('mode).contains(Modes.CODEGEN)) {
         //@note Mathematica needed for quantitative ModelPlex
         if (options.get('quantitative).isDefined) {
-          initializeProver(
-            if (options.contains('tool)) options
-            else options ++ configFromFile(Tools.MATHEMATICA))
+          initializeProver(options ++ configFromFile(Tools.MATHEMATICA))
         }
         codegen(options)
       } else if (!options.get('mode).contains(Modes.UI) ) {
         try {
-          initializeProver(
-            if (options.contains('tool)) options
-            else options ++ configFromFile("z3"))
+          initializeProver(options ++ configFromFile("z3"))

           //@todo allow multiple passes by filter architecture: -prove bla.key -tactic bla.scal -modelplex -code
           options.get('mode) match {

[ANogin]

Stefan, note that your fix runs initializeProver(combineToolConfigs(options, configFromFile("z3"))) even when -tool mathematica is given on the command line :(