# HG changeset patch # User wenzelm # Date 1667232613 -3600 # Node ID 389d77e6be9fec3a8b939a1f571d691c70be7933 # Parent fac28b6c37e8c42a0a16511652672c5ee1e75922 support for Easychair style with demo document; diff -r fac28b6c37e8 -r 389d77e6be9f Admin/components/components.sha1 --- a/Admin/components/components.sha1 Mon Oct 31 15:50:13 2022 +0100 +++ b/Admin/components/components.sha1 Mon Oct 31 17:10:13 2022 +0100 @@ -90,6 +90,7 @@ 813b66ca151d7a39b5cacb39ab52acabc2a54845 e-2.5.tar.gz 6e63f9f354b8c06035952845b987080699a12d55 e-2.6-1.tar.gz a3bebab5df4294dac2dd7fd2065a94df00e0b3ff e-2.6.tar.gz +239e7b8bebbfc29a1c5151e8fb261ffad44877f1 easychair-3.5.tar.gz 6d34b18ca0aa1e10bab6413045d079188c0e2dfb exec_process-1.0.1.tar.gz 8b9bffd10e396d965e815418295f2ee2849bea75 exec_process-1.0.2.tar.gz e6aada354da11e533af2dee3dcdd96c06479b053 exec_process-1.0.3.tar.gz diff -r fac28b6c37e8 -r 389d77e6be9f Admin/components/main --- a/Admin/components/main Mon Oct 31 15:50:13 2022 +0100 +++ b/Admin/components/main Mon Oct 31 17:10:13 2022 +0100 @@ -6,6 +6,7 @@ csdp-6.1.1 cvc4-1.8 e-2.6-1 +easychair-3.5 flatlaf-2.4 idea-icons-20210508 isabelle_fonts-20211004 diff -r fac28b6c37e8 -r 389d77e6be9f NEWS --- a/NEWS Mon Oct 31 15:50:13 2022 +0100 +++ b/NEWS Mon Oct 31 17:10:13 2022 +0100 @@ -9,9 +9,11 @@ *** Document preparation *** -* The Dagstuhl LIPIcs style is included as Isabelle component. The -session "Demo_LIPIcs" provides an example document, which is also -included in the regular Isabelle documentation as "demo_lipics". +* Various well-known LaTeX styles are included as Isabelle components, +with demo documents in the regular Isabelle "doc" space: + + - Easychair as session "Demo_Easychair" / doc "demo_easychair" + - Dagstuhl LIPIcs style as session "Demo_LIPIcs" / doc "demo_lipics" *** HOL *** diff -r fac28b6c37e8 -r 389d77e6be9f doc/Contents --- a/doc/Contents Mon Oct 31 15:50:13 2022 +0100 +++ b/doc/Contents Mon Oct 31 17:10:13 2022 +0100 @@ -19,6 +19,7 @@ jedit Isabelle/jEdit Demo Documents + demo_easychair Demo for Easychair style demo_lipics Demo for Dagstuhl LIPIcs style Old Isabelle Manuals diff -r fac28b6c37e8 -r 389d77e6be9f etc/build.props --- a/etc/build.props Mon Oct 31 15:50:13 2022 +0100 +++ b/etc/build.props Mon Oct 31 17:10:13 2022 +0100 @@ -16,6 +16,7 @@ src/Pure/Admin/build_cygwin.scala \ src/Pure/Admin/build_doc.scala \ src/Pure/Admin/build_e.scala \ + src/Pure/Admin/build_easychair.scala \ src/Pure/Admin/build_fonts.scala \ src/Pure/Admin/build_history.scala \ src/Pure/Admin/build_jcef.scala \ diff -r fac28b6c37e8 -r 389d77e6be9f src/Doc/Demo_Easychair/Document.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Demo_Easychair/Document.thy Mon Oct 31 17:10:13 2022 +0100 @@ -0,0 +1,64 @@ +theory Document + imports Main +begin + +section \Some section\ + +subsection \Some subsection\ + +subsection \Some subsubsection\ + +subsubsection \Some subsubsubsection\ + +paragraph \A paragraph.\ + +text \Informal bla bla.\ + +definition "foo = True" \ \side remark on \<^const>\foo\\ + +definition "bar = False" \ \side remark on \<^const>\bar\\ + +lemma foo unfolding foo_def .. + + +paragraph \Another paragraph.\ + +text \See also @{cite \\S3\ "isabelle-system"}.\ + + +section \Formal proof of Cantor's theorem\ + +text_raw \\isakeeptag{proof}\ +text \ + Cantor's Theorem states that there is no surjection from + a set to its powerset. The proof works by diagonalization. E.g.\ see + \<^item> \<^url>\http://mathworld.wolfram.com/CantorDiagonalMethod.html\ + \<^item> \<^url>\https://en.wikipedia.org/wiki/Cantor's_diagonal_argument\ +\ + +theorem Cantor: "\f :: 'a \ 'a set. \A. \x. A = f x" +proof + assume "\f :: 'a \ 'a set. \A. \x. A = f x" + then obtain f :: "'a \ 'a set" where *: "\A. \x. A = f x" .. + let ?D = "{x. x \ f x}" + from * obtain a where "?D = f a" by blast + moreover have "a \ ?D \ a \ f a" by blast + ultimately show False by blast +qed + + +subsection \Lorem ipsum dolor\ + +text \ + Lorem ipsum dolor sit amet, consectetur adipiscing elit. Donec id ipsum + sapien. Vivamus malesuada enim nibh, a tristique nisi sodales ac. Praesent + ut sem consectetur, interdum tellus ac, sodales nulla. Quisque vel diam at + risus tempus tempor eget a tortor. Suspendisse potenti. Nulla erat lacus, + dignissim sed volutpat nec, feugiat non leo. Nunc blandit et justo sed + venenatis. Donec scelerisque placerat magna, et congue nulla convallis vel. + Cras tristique dolor consequat dolor tristique rutrum. Suspendisse ultrices + sem nibh, et suscipit felis ultricies at. Aliquam venenatis est vel nulla + efficitur ornare. Lorem ipsum dolor sit amet, consectetur adipiscing elit. +\ + +end diff -r fac28b6c37e8 -r 389d77e6be9f src/Doc/Demo_Easychair/document/root.bib --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Demo_Easychair/document/root.bib Mon Oct 31 17:10:13 2022 +0100 @@ -0,0 +1,4 @@ +@manual{isabelle-system, + author = {Makarius Wenzel}, + title = {The {Isabelle} System Manual}, + note = {\url{https://isabelle.in.tum.de/doc/system.pdf}}} diff -r fac28b6c37e8 -r 389d77e6be9f src/Doc/Demo_Easychair/document/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Demo_Easychair/document/root.tex Mon Oct 31 17:10:13 2022 +0100 @@ -0,0 +1,31 @@ +\documentclass[a4paper,11pt]{easychair} +\usepackage{amssymb} +\usepackage{hyperref}\urlstyle{rm} + +\usepackage{isabelle,isabellesym}\isabellestyle{it} + +\isadroptag{theory} +\isafoldtag{proof} + + +\begin{document} + +\title{Isabelle document preparation with Easychair style} +\titlerunning{Easychair style} +\author{Makarius Wenzel} +\authorrunning{M. Wenzel} +\institute{\url{https://sketis.net}} +\maketitle + +\begin{abstract} +Isabelle is a formal document preparation system. This example shows how to +use it together with the Easychair style. See +\url{https://easychair.org/publications/for_authors} for further information. +\end{abstract} + +\input{session} + +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document} diff -r fac28b6c37e8 -r 389d77e6be9f src/Doc/ROOT --- a/src/Doc/ROOT Mon Oct 31 15:50:13 2022 +0100 +++ b/src/Doc/ROOT Mon Oct 31 17:10:13 2022 +0100 @@ -489,6 +489,16 @@ "root.tex" "style.sty" +session Demo_Easychair (doc) in "Demo_Easychair" = HOL + + options [document_variants = "demo_easychair"] + theories + Document + document_files (in "$ISABELLE_EASYCHAIR_HOME") + "easychair.cls" + document_files + "root.bib" + "root.tex" + session Demo_LIPIcs (doc) in "Demo_LIPIcs" = HOL + options [document_variants = "demo_lipics", document_build = "pdflatex", document_heading_prefix = "", document_comment_latex] diff -r fac28b6c37e8 -r 389d77e6be9f src/Pure/Admin/build_easychair.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Admin/build_easychair.scala Mon Oct 31 17:10:13 2022 +0100 @@ -0,0 +1,108 @@ +/* Title: Pure/Admin/build_easychair.scala + Author: Makarius + +Build Isabelle component for Easychair style. + +See also: https://easychair.org/publications/for_authors +*/ + +package isabelle + + +object Build_Easychair { + /* build easychair component */ + + val default_url = "https://easychair.org/publications/easychair.zip" + + def build_easychair( + download_url: String = default_url, + target_dir: Path = Path.current, + progress: Progress = new Progress + ): Unit = { + Isabelle_System.require_command("unzip", test = "-h") + + Isabelle_System.with_tmp_file("download", ext = "zip") { download_file => + Isabelle_System.with_tmp_dir("download") { download_dir => + + /* download */ + + Isabelle_System.download_file(download_url, download_file, progress = progress) + Isabelle_System.bash("unzip -x " + File.bash_path(download_file), + cwd = download_dir.file).check + + val easychair_dir = + File.read_dir(download_dir) match { + case List(name) => download_dir + Path.explode(name) + case bad => + error("Expected exactly one directory entry in " + download_file + + bad.mkString("\n", "\n ", "")) + } + + + /* component */ + + val version = + Library.try_unprefix("EasyChair", easychair_dir.file_name) + .getOrElse("Failed to detect version from " + quote(easychair_dir.file_name)) + + val component = "easychair-" + version + val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component)) + progress.echo("Component " + component_dir) + + component_dir.file.delete + Isabelle_System.copy_dir(easychair_dir, component_dir) + + + /* settings */ + + val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc")) + File.write(etc_dir + Path.basic("settings"), + """# -*- shell-script -*- :mode=shellscript: + +ISABELLE_EASYCHAIR_HOME="$COMPONENT" +""") + + + /* README */ + + File.write(component_dir + Path.basic("README"), + """This is the Easychair style for authors from +""" + download_url + """ + + + Makarius + """ + Date.Format.date(Date.now()) + "\n") + } + } + } + + + /* Isabelle tool wrapper */ + + val isabelle_tool = + Isabelle_Tool("build_easychair", "build component for Easychair style", + Scala_Project.here, + { args => + var target_dir = Path.current + var download_url = default_url + + val getopts = Getopts(""" +Usage: isabelle build_easychair [OPTIONS] + + Options are: + -D DIR target directory (default ".") + -U URL download URL (default: """" + default_url + """") + + Build component for Easychair style. +""", + "D:" -> (arg => target_dir = Path.explode(arg)), + "U:" -> (arg => download_url = arg)) + + val more_args = getopts(args) + if (more_args.nonEmpty) getopts.usage() + + val progress = new Console_Progress() + + build_easychair(download_url = download_url, target_dir = target_dir, progress = progress) + }) +} diff -r fac28b6c37e8 -r 389d77e6be9f src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala Mon Oct 31 15:50:13 2022 +0100 +++ b/src/Pure/System/isabelle_tool.scala Mon Oct 31 17:10:13 2022 +0100 @@ -159,6 +159,7 @@ Build_Cygwin.isabelle_tool, Build_Doc.isabelle_tool, Build_E.isabelle_tool, + Build_Easychair.isabelle_tool, Build_Fonts.isabelle_tool, Build_JCEF.isabelle_tool, Build_JDK.isabelle_tool,