From 672e403af0692a58f3ab35e01bd106d883025ffe Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 24 Apr 2015 17:50:08 +0200
Subject: [PATCH] Improve help message
---
src/main/scala/leon/Main.scala | 16 ++++++++++------
src/main/scala/leon/SharedOptions.scala | 7 ++++++-
2 files changed, 16 insertions(+), 7 deletions(-)
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index da74e9878..5035e0e36 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -33,33 +33,37 @@ object Main {
object MainComponent extends LeonComponent {
val name = "main"
- val description = "The main Leon component, handling the top-level options"
+ val description = "Options that determine the feature of Leon to be used (mutually exclusive). Default: verify"
val optTermination = LeonFlagOptionDef("termination", "Check program termination", false)
val optRepair = LeonFlagOptionDef("repair", "Repair selected functions", false)
val optSynthesis = LeonFlagOptionDef("synthesis", "Partial synthesis of choose() constructs", false)
val optXLang = LeonFlagOptionDef("xlang", "Support for extra program constructs (imperative,...)", false)
- val optWatch = LeonFlagOptionDef("watch", "Rerun pipeline when file changes", false)
val optNoop = LeonFlagOptionDef("noop", "No operation performed, just output program", false)
val optVerify = LeonFlagOptionDef("verify", "Verify function contracts", true )
val optHelp = LeonFlagOptionDef("help", "Show help message", false)
val optEval = LeonFlagOptionDef("eval", "Evaluate ground functions", false)
override val definedOptions: Set[LeonOptionDef[Any]] =
- Set(optTermination, optRepair, optSynthesis, optXLang, optWatch, optNoop, optHelp, optVerify, optEval)
+ Set(optTermination, optRepair, optSynthesis, optXLang, optNoop, optHelp, optVerify, optEval)
}
lazy val allOptions: Set[LeonOptionDef[Any]] = allComponents.flatMap(_.definedOptions)
def displayHelp(reporter: Reporter, error: Boolean) = {
- reporter.info("Top-level options:")
+ reporter.info(MainComponent.description)
+ for (opt <- MainComponent.definedOptions.toSeq.sortBy(_.name)) {
+ reporter.info(opt.helpString)
+ }
reporter.info("")
- for (opt <- (MainComponent.definedOptions ++ SharedOptions.definedOptions).toSeq.sortBy(_.name)) {
+ reporter.info("Additional top-level options")
+ for (opt <- SharedOptions.definedOptions.toSeq.sortBy(_.name)) {
reporter.info(opt.helpString)
}
reporter.info("")
+
reporter.info("Additional options, by component:")
for (c <- (allComponents - MainComponent - SharedOptions).toSeq.sortBy(_.name) if c.definedOptions.nonEmpty) {
@@ -198,7 +202,7 @@ object Main {
ctx.interruptManager.registerSignalHandler()
- val doWatch = ctx.findOptionOrDefault(MainComponent.optWatch)
+ val doWatch = ctx.findOptionOrDefault(SharedOptions.optWatch)
if (doWatch) {
val watcher = new FilesWatcher(ctx, ctx.files)
diff --git a/src/main/scala/leon/SharedOptions.scala b/src/main/scala/leon/SharedOptions.scala
index 4541fc0fc..4cd05cc65 100644
--- a/src/main/scala/leon/SharedOptions.scala
+++ b/src/main/scala/leon/SharedOptions.scala
@@ -12,6 +12,8 @@ object SharedOptions extends LeonComponent {
val optStrictPhases = LeonFlagOptionDef("strict", "Terminate after each phase if there is an error", true)
+ val optWatch = LeonFlagOptionDef("watch", "Rerun pipeline when file changes", false)
+
val optFunctions = new LeonOptionDef[Seq[String]] {
val name = "functions"
val description = "Only consider functions f1, f2, ..."
@@ -31,7 +33,10 @@ object SharedOptions extends LeonComponent {
val optDebug = new LeonOptionDef[Set[DebugSection]] {
import OptionParsers._
val name = "debug"
- val description = "Enable detailed messages per component"
+ val description = (
+ "Enable detailed messages per component.\nAvailable:" +:
+ DebugSections.all.toSeq.map(_.name).sorted
+ ).mkString("\n ")
val default = Set[DebugSection]()
val usageRhs = "d1,d2,..."
val debugParser: OptionParser[Set[DebugSection]] = s => {
--
GitLab