如何在K框架中给`krun`传递字符串参数？

Question

在K框架中，可以使用krun的-c开关将默认$PGM以外的其他变量传递给初始配置。例如，一个人可能有这样的代码：

configuration <T color="yellow">
                <k color="green"> $PGM:Pgm </k>
                <something> $SOMEARG:Int </something>
              </T>

然后运行kompile imp.k; krun tests/sum.imp -cSOMEARG=3，$SOMEARG变量将获得值3。然而，当我试图传递一个字符串时，我遇到了问题：

configuration <T color="yellow">
                <k color="green"> $PGM:Pgm </k>
                <something> $SOMEARG:String </something>
              </T>

在kompile之后，命令

krun tests/sum.imp -cSOMEARG=\"hello\" --debug

输出：

org.kframework.utils.errorsystem.KEMException: [Error] Critical: Parser returned a non-zero exit code: 113
Stdout:

Stderr:
[Error] Inner Parser: Parse error: unexpected token 'hello'.
    Source(<command line: -e>)
    Location(1,1,1,6)

    at org.kframework.utils.errorsystem.KEMException.create(KEMException.java:130)
    at org.kframework.utils.errorsystem.KEMException.criticalError(KEMException.java:39)
    at org.kframework.krun.KRun.externalParse(KRun.java:237)
    at org.kframework.krun.KRun.parseConfigVars(KRun.java:161)
    at org.kframework.krun.KRun.run(KRun.java:77)
    at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:95)
    at org.kframework.main.FrontEnd.main(FrontEnd.java:62)
    at org.kframework.main.Main.runApplication(Main.java:118)
    at org.kframework.main.Main.runApplication(Main.java:108)
    at org.kframework.main.Main.main(Main.java:56)

如何传递字符串参数？

Answer 1

这是我们正在使用的选项解析库版本中的一个错误，导致它尝试取消引号，尽管这实际上是shell的角色。在最新版本的选项库中已修复此问题。您可以在此处跟踪错误修复的进度：https://github.com/kframework/k/pull/1335

我预计它将在不久的将来得到修复。