added isabelle build option -k, for fast off-line checking of theory sources;
authorwenzelm
Wed Apr 01 15:41:08 2015 +0200 (2015-04-01)
changeset 598919ce697050455
parent 59890 01aff5aa081d
child 59892 2a616319c171
added isabelle build option -k, for fast off-line checking of theory sources;
NEWS
lib/Tools/build
src/Doc/System/Sessions.thy
src/Pure/PIDE/batch_session.scala
src/Pure/Tools/build.scala
src/Pure/Tools/check_keywords.scala
src/Pure/build-jars
     1.1 --- a/NEWS	Wed Apr 01 13:32:32 2015 +0200
     1.2 +++ b/NEWS	Wed Apr 01 15:41:08 2015 +0200
     1.3 @@ -396,6 +396,8 @@
     1.4  * The Isabelle tool "update_cartouches" changes theory files to use
     1.5  cartouches instead of old-style {* verbatim *} or `alt_string` tokens.
     1.6  
     1.7 +* The Isabelle tool "build" provides new option -k.
     1.8 +
     1.9  
    1.10  
    1.11  New in Isabelle2014 (August 2014)
     2.1 --- a/lib/Tools/build	Wed Apr 01 13:32:32 2015 +0200
     2.2 +++ b/lib/Tools/build	Wed Apr 01 15:41:08 2015 +0200
     2.3 @@ -34,6 +34,7 @@
     2.4    echo "    -d DIR       include session directory"
     2.5    echo "    -g NAME      select session group NAME"
     2.6    echo "    -j INT       maximum number of parallel jobs (default 1)"
     2.7 +  echo "    -k KEYWORD   check theory sources for conflicts with proposed keywords"
     2.8    echo "    -l           list session source files"
     2.9    echo "    -n           no build -- test dependencies only"
    2.10    echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
    2.11 @@ -68,13 +69,14 @@
    2.12  declare -a INCLUDE_DIRS=()
    2.13  declare -a SESSION_GROUPS=()
    2.14  MAX_JOBS=1
    2.15 +declare -a CHECK_KEYWORDS=()
    2.16  LIST_FILES=false
    2.17  NO_BUILD=false
    2.18  eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
    2.19  SYSTEM_MODE=false
    2.20  VERBOSE=false
    2.21  
    2.22 -while getopts "D:Rabcd:g:j:lno:sv" OPT
    2.23 +while getopts "D:Rabcd:g:j:k:lno:sv" OPT
    2.24  do
    2.25    case "$OPT" in
    2.26      D)
    2.27 @@ -102,6 +104,9 @@
    2.28        check_number "$OPTARG"
    2.29        MAX_JOBS="$OPTARG"
    2.30        ;;
    2.31 +    k)
    2.32 +      CHECK_KEYWORDS["${#CHECK_KEYWORDS[@]}"]="$OPTARG"
    2.33 +      ;;
    2.34      l)
    2.35        LIST_FILES="true"
    2.36        ;;
    2.37 @@ -145,7 +150,8 @@
    2.38    "$REQUIREMENTS" "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
    2.39    "$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
    2.40    "${INCLUDE_DIRS[@]}" $'\n' "${SELECT_DIRS[@]}" $'\n' \
    2.41 -  "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
    2.42 +  "${SESSION_GROUPS[@]}" $'\n' "${CHECK_KEYWORDS[@]}" $'\n' \
    2.43 +  "${BUILD_OPTIONS[@]}" $'\n' "$@"
    2.44  RC="$?"
    2.45  
    2.46  if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
     3.1 --- a/src/Doc/System/Sessions.thy	Wed Apr 01 13:32:32 2015 +0200
     3.2 +++ b/src/Doc/System/Sessions.thy	Wed Apr 01 15:41:08 2015 +0200
     3.3 @@ -284,6 +284,7 @@
     3.4      -d DIR       include session directory
     3.5      -g NAME      select session group NAME
     3.6      -j INT       maximum number of parallel jobs (default 1)
     3.7 +    -k KEYWORD   check theory sources for conflicts with proposed keywords
     3.8      -l           list session source files
     3.9      -n           no build -- test dependencies only
    3.10      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    3.11 @@ -369,7 +370,12 @@
    3.12    \medskip Option @{verbatim "-v"} increases the general level of
    3.13    verbosity.  Option @{verbatim "-l"} lists the source files that
    3.14    contribute to a session.
    3.15 -\<close>
    3.16 +
    3.17 +  \medskip Option @{verbatim "-k"} specifies a newly proposed keyword for
    3.18 +  outer syntax (multiple uses allowed). The theory sources are checked for
    3.19 +  conflicts wrt.\ this hypothetical change of syntax, e.g.\ to reveal
    3.20 +  occurrences of identifiers that need to be quoted.\<close>
    3.21 +
    3.22  
    3.23  subsubsection \<open>Examples\<close>
    3.24  
     4.1 --- a/src/Pure/PIDE/batch_session.scala	Wed Apr 01 13:32:32 2015 +0200
     4.2 +++ b/src/Pure/PIDE/batch_session.scala	Wed Apr 01 15:41:08 2015 +0200
     4.3 @@ -29,7 +29,7 @@
     4.4          dirs = dirs, sessions = List(parent_session)) != 0)
     4.5        new RuntimeException
     4.6  
     4.7 -    val deps = Build.dependencies(Build.Ignore_Progress, false, verbose, false, session_tree)
     4.8 +    val deps = Build.dependencies(verbose = verbose, tree = session_tree)
     4.9      val resources =
    4.10      {
    4.11        val content = deps(parent_session)
     5.1 --- a/src/Pure/Tools/build.scala	Wed Apr 01 13:32:32 2015 +0200
     5.2 +++ b/src/Pure/Tools/build.scala	Wed Apr 01 15:41:08 2015 +0200
     5.3 @@ -427,8 +427,13 @@
     5.4      def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
     5.5    }
     5.6  
     5.7 -  def dependencies(progress: Progress, inlined_files: Boolean,
     5.8 -      verbose: Boolean, list_files: Boolean, tree: Session_Tree): Deps =
     5.9 +  def dependencies(
    5.10 +      progress: Progress = Ignore_Progress,
    5.11 +      inlined_files: Boolean = false,
    5.12 +      verbose: Boolean = false,
    5.13 +      list_files: Boolean = false,
    5.14 +      check_keywords: Set[String] = Set.empty,
    5.15 +      tree: Session_Tree): Deps =
    5.16      Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
    5.17        { case (deps, (name, info)) =>
    5.18            if (progress.stopped) throw Exn.Interrupt()
    5.19 @@ -484,16 +489,28 @@
    5.20              val keywords = thy_deps.keywords
    5.21              val syntax = thy_deps.syntax.asInstanceOf[Outer_Syntax]
    5.22  
    5.23 +            val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
    5.24              val loaded_files = if (inlined_files) thy_deps.loaded_files else Nil
    5.25  
    5.26              val all_files =
    5.27 -              (thy_deps.deps.map(dep => Path.explode(dep.name.node)) ::: loaded_files :::
    5.28 +              (theory_files ::: loaded_files :::
    5.29                  info.files.map(file => info.dir + file) :::
    5.30                  info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
    5.31  
    5.32              if (list_files)
    5.33                progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
    5.34  
    5.35 +            if (check_keywords.nonEmpty) {
    5.36 +              for {
    5.37 +                path <- theory_files
    5.38 +                (tok, pos) <- Check_Keywords.conflicts(syntax.keywords, check_keywords, path)
    5.39 +              } {
    5.40 +                progress.echo(Output.warning_text(
    5.41 +                  "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) +
    5.42 +                    Position.here(pos)))
    5.43 +              }
    5.44 +            }
    5.45 +
    5.46              val sources = all_files.map(p => (p, SHA1.digest(p.file)))
    5.47  
    5.48              val session_graph = thy_deps.deps_graph(info.parent getOrElse "", loaded_theories0)
    5.49 @@ -517,7 +534,7 @@
    5.50      sessions: List[String]): Deps =
    5.51    {
    5.52      val (_, tree) = find_sessions(options, dirs = dirs).selection(false, false, Nil, sessions)
    5.53 -    dependencies(Ignore_Progress, inlined_files, false, false, tree)
    5.54 +    dependencies(inlined_files = inlined_files, tree = tree)
    5.55    }
    5.56  
    5.57    def session_content(
    5.58 @@ -737,6 +754,7 @@
    5.59      session_groups: List[String] = Nil,
    5.60      max_jobs: Int = 1,
    5.61      list_files: Boolean = false,
    5.62 +    check_keywords: Set[String] = Set.empty,
    5.63      no_build: Boolean = false,
    5.64      system_mode: Boolean = false,
    5.65      verbose: Boolean = false,
    5.66 @@ -748,7 +766,7 @@
    5.67      val (selected, selected_tree) =
    5.68        full_tree.selection(requirements, all_sessions, session_groups, sessions)
    5.69  
    5.70 -    val deps = dependencies(progress, true, verbose, list_files, selected_tree)
    5.71 +    val deps = dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
    5.72  
    5.73      def make_stamp(name: String): String =
    5.74        sources_stamp(selected_tree(name).entry_digest :: deps.sources(name))
    5.75 @@ -988,6 +1006,7 @@
    5.76      session_groups: List[String] = Nil,
    5.77      max_jobs: Int = 1,
    5.78      list_files: Boolean = false,
    5.79 +    check_keywords: Set[String] = Set.empty,
    5.80      no_build: Boolean = false,
    5.81      system_mode: Boolean = false,
    5.82      verbose: Boolean = false,
    5.83 @@ -996,7 +1015,7 @@
    5.84      val results =
    5.85        build_results(options, progress, requirements, all_sessions,
    5.86          build_heap, clean_build, dirs, select_dirs, session_groups, max_jobs,
    5.87 -        list_files, no_build, system_mode, verbose, sessions)
    5.88 +        list_files, check_keywords, no_build, system_mode, verbose, sessions)
    5.89  
    5.90      val rc = (0 /: results)({ case (rc1, (_, rc2)) => rc1 max rc2 })
    5.91      if (rc != 0 && (verbose || !no_build)) {
    5.92 @@ -1024,13 +1043,15 @@
    5.93            Properties.Value.Boolean(no_build) ::
    5.94            Properties.Value.Boolean(system_mode) ::
    5.95            Properties.Value.Boolean(verbose) ::
    5.96 -          Command_Line.Chunks(dirs, select_dirs, session_groups, build_options, sessions) =>
    5.97 +          Command_Line.Chunks(
    5.98 +              dirs, select_dirs, session_groups, check_keywords, build_options, sessions) =>
    5.99              val options = (Options.init() /: build_options)(_ + _)
   5.100              val progress = new Console_Progress(verbose)
   5.101              progress.interrupt_handler {
   5.102                build(options, progress, requirements, all_sessions, build_heap, clean_build,
   5.103                  dirs.map(Path.explode(_)), select_dirs.map(Path.explode(_)), session_groups,
   5.104 -                max_jobs, list_files, no_build, system_mode, verbose, sessions)
   5.105 +                max_jobs, list_files, check_keywords.toSet, no_build, system_mode,
   5.106 +                verbose, sessions)
   5.107              }
   5.108          case _ => error("Bad arguments:\n" + cat_lines(args))
   5.109        }
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Pure/Tools/check_keywords.scala	Wed Apr 01 15:41:08 2015 +0200
     6.3 @@ -0,0 +1,37 @@
     6.4 +/*  Title:      Pure/Tools/check_keywords.scala
     6.5 +    Author:     Makarius
     6.6 +
     6.7 +Check theory sources for conflicts with proposed keywords.
     6.8 +*/
     6.9 +
    6.10 +package isabelle
    6.11 +
    6.12 +
    6.13 +object Check_Keywords
    6.14 +{
    6.15 +  def conflicts(
    6.16 +    keywords: Keyword.Keywords,
    6.17 +    check: Set[String],
    6.18 +    input: CharSequence,
    6.19 +    start: Token.Pos): List[(Token, Position.T)] =
    6.20 +  {
    6.21 +    object Parser extends Parse.Parser
    6.22 +    {
    6.23 +      private val conflict =
    6.24 +        position(token("token", tok => !(tok.is_command || tok.is_keyword) && check(tok.source)))
    6.25 +      private val other = token("token", _ => true)
    6.26 +      private val item = conflict ^^ (x => Some(x)) | other ^^ (_ => None)
    6.27 +
    6.28 +      val result =
    6.29 +        parse_all(rep(item), Token.reader(Token.explode(keywords, input), start)) match {
    6.30 +          case Success(res, _) => for (Some(x) <- res) yield x
    6.31 +          case bad => error(bad.toString)
    6.32 +        }
    6.33 +    }
    6.34 +    Parser.result
    6.35 +  }
    6.36 +
    6.37 +  def conflicts(
    6.38 +    keywords: Keyword.Keywords, check: Set[String], path: Path): List[(Token, Position.T)] =
    6.39 +    conflicts(keywords, check, File.read(path), Token.Pos.file(path.expand.implode))
    6.40 +}
     7.1 --- a/src/Pure/build-jars	Wed Apr 01 13:32:32 2015 +0200
     7.2 +++ b/src/Pure/build-jars	Wed Apr 01 15:41:08 2015 +0200
     7.3 @@ -92,6 +92,7 @@
     7.4    Tools/build.scala
     7.5    Tools/build_console.scala
     7.6    Tools/build_doc.scala
     7.7 +  Tools/check_keywords.scala
     7.8    Tools/check_source.scala
     7.9    Tools/doc.scala
    7.10    Tools/main.scala