Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/Pure/Tools/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 5 kB

Quelle mkroot.scala Sprache: Scala

/*  Title:      Pure/Tools/mkroot.scala
    Author:     Makarius

Create session root directory.
*/

package isabelle

object Mkroot {
  /** mkroot **/

  def root_name(name: String): String =
    Token.quote_name(Sessions.root_syntax.keywords, name)

  def latex_name(name: String): String =
    (for (c <- name.iterator if c != '\\')
     yield if (c == '_') '-' else c).mkString

  def mkroot(
    session_name: String = "",
    session_dir: Path = Path.current,
    session_parent: String = "",
    init_repos: Boolean = false,
    title: String = "",
    author: String = "",
    quiet: Boolean = false,
    progress: Progress = new Progress
  ): Unit = {
    Isabelle_System.make_directory(session_dir)

    val name = proper_string(session_name) getOrElse session_dir.absolute_file.getName
    val parent = proper_string(session_parent) getOrElse Isabelle_System.default_logic()

    val root_path = session_dir + Sessions.ROOT
    if (root_path.file.exists) error("Cannot overwrite existing " + root_path)

    val document_path = session_dir + Path.explode("document")
    if (document_path.file.exists) error("Cannot overwrite existing " + document_path)

    val root_tex = session_dir + Path.explode("document/root.tex")

    progress.echo(
      (if (quiet) "" else "\n") +
      "Initializing session " + quote(name) + " in " + session_dir.absolute)

    /* ROOT */

    progress.echo_if(!quiet, " creating " + root_path)

    File.write(root_path,
      "session " + root_name(name) + " = " + root_name(parent) + """ +
  options [document = pdf, document_output = "output"]
(*theories [document = false]
    A
    B
  theories
    C
    D*)
  document_files
    "root.tex"
""")

    /* document directory */

    {
      progress.echo_if(!quiet, " creating " + root_tex)

      Isabelle_System.make_directory(root_tex.dir)

      File.write(root_tex,
"""\documentclass[11pt,a4paper]{article}
\""" + """usepackage[T1]{fontenc}
\""" + """usepackage{isabelle,isabellesym}

% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed

%\""" + """usepackage{amssymb}
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
  %\<triangleq>, \<yen>, \<lozenge>

%\""" + """usepackage{eurosym}
  %for \<euro>

%\""" + """usepackage[only,bigsqcap,bigparallel,fatsemi,interleave,sslash]{stmaryrd}
  %for \<Sqinter>, \<Parallel>, \<Zsemi>, \<Parallel>, \<sslash>

%\""" + """usepackage{eufrak}
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)

%\""" + """usepackage{textcomp}
  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
  %\<currency>

% this should be the last package used
\""" + """usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\""" + """urlstyle{rm}
\isabellestyle{it}

% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}

\begin{document}

\title{""" + (proper_string(title) getOrElse latex_name(name)) + """}
\author{""" + (proper_string(author) getOrElse latex_name(System.getProperty("user.name"))) + """}
\maketitle

\tableofcontents

% sane default for proof documents
\parindent 0pt\parskip 0.5ex

% generated text of all theories
\input{session}

% optional bibliography
%\bibliographystyle{abbrv}
%\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
""")
    }

    /* Mercurial repository */

    if (init_repos) {
      progress.echo(
        (if (quiet) "" else "\n") +
        "Initializing Mercurial repository " + session_dir.absolute)

      val hg = Mercurial.init_repository(session_dir)

      val hg_ignore = session_dir + Path.explode(".hgignore")
      File.write(hg_ignore,
"""syntax: glob

*~
*.marks
*.orig
*.rej
.DS_Store
.swp

syntax: regexp

^output/
""")

      hg.add(List(root_path, root_tex, hg_ignore))
    }

    /* notes */

    {
      val print_dir = session_dir.implode
      progress.echo_if(!quiet, """
Now use the following command line to build the session:

  isabelle build -D """ +
        (if (Bash.string(print_dir) == print_dir) print_dir else quote(print_dir)) + "\n")
    }
  }

  /** Isabelle tool wrapper **/

  val isabelle_tool = Isabelle_Tool("mkroot", "create session root directory",
    Scala_Project.here,
    { args =>
      var author = ""
      var init_repos = false
      var title = ""
      var session_name = ""
      var quiet = false

      val getopts = Getopts("""
Usage: isabelle mkroot [OPTIONS] [DIRECTORY]

  Options are:
    -A LATEX     provide author in LaTeX notation (default: user name)
    -I           init Mercurial repository and add generated files
    -T LATEX     provide title in LaTeX notation (default: session name)
    -n NAME      alternative session name (default: directory base name)
    -q           quiet mode: less verbosity

  Create session root directory (default: current directory).
""",
        "A:" -> (arg => author = arg),
        "I" -> (_ => init_repos = true),
        "T:" -> (arg => title = arg),
        "n:" -> (arg => session_name = arg),
        "q" -> (_ => quiet = true))

      val more_args = getopts(args)

      val session_dir =
        more_args match {
          case Nil => Path.current
          case List(dir) => Path.explode(dir)
          case _ => getopts.usage()
        }

      val progress = new Console_Progress

      mkroot(session_name = session_name, session_dir = session_dir, init_repos = init_repos,
        author = author, title = title, quiet = quiet, progress = progress)
    })
}

quality91%

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.