# HG changeset patch # User wenzelm # Date 1667227813 -3600 # Node ID fac28b6c37e8c42a0a16511652672c5ee1e75922 # Parent 9d3b9e89455f937f311a0acfae21d7ebf10f4135 support for Dagstuhl LIPIcs style with demo document; diff -r 9d3b9e89455f -r fac28b6c37e8 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Mon Oct 31 11:04:54 2022 +0100 +++ b/Admin/components/components.sha1 Mon Oct 31 15:50:13 2022 +0100 @@ -279,6 +279,7 @@ 377e36efb8608e6c828c7718d890e97fde2006a4 linux_app-20131007.tar.gz 759848095e2ad506083d92b5646947e3c32f27a0 linux_app-20191223.tar.gz 1a449ce69ac874e21804595d16aaaf5a0d0d0c10 linux_app-20200110.tar.gz +5557b396f5a9aa22388d3e2171f9bc58e4bd6cd7 lipics-3.1.2.tar.gz 0aab4f73ff7f5e36f33276547e10897e1e56fb1d macos_app-20130716.tar.gz ad5d0e640ce3609a885cecab645389a2204e03bb macos_app-20150916.tar.gz 400af57ec5cd51f96928d9de00d077524a6fe316 macos_app-20181205.tar.gz diff -r 9d3b9e89455f -r fac28b6c37e8 Admin/components/main --- a/Admin/components/main Mon Oct 31 11:04:54 2022 +0100 +++ b/Admin/components/main Mon Oct 31 15:50:13 2022 +0100 @@ -15,6 +15,7 @@ jfreechart-1.5.3 jortho-1.0-2 kodkodi-1.5.7 +lipics-3.1.2 minisat-2.2.1-1 mlton-20210117-1 nunchaku-0.5 diff -r 9d3b9e89455f -r fac28b6c37e8 NEWS --- a/NEWS Mon Oct 31 11:04:54 2022 +0100 +++ b/NEWS Mon Oct 31 15:50:13 2022 +0100 @@ -7,6 +7,13 @@ New in this Isabelle version ---------------------------- +*** 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". + + *** HOL *** * Theory "HOL.Fun": diff -r 9d3b9e89455f -r fac28b6c37e8 doc/Contents --- a/doc/Contents Mon Oct 31 11:04:54 2022 +0100 +++ b/doc/Contents Mon Oct 31 15:50:13 2022 +0100 @@ -18,6 +18,9 @@ system The Isabelle System Manual jedit Isabelle/jEdit +Demo Documents + demo_lipics Demo for Dagstuhl LIPIcs style + Old Isabelle Manuals tutorial Tutorial on Isabelle/HOL intro Old Introduction to Isabelle diff -r 9d3b9e89455f -r fac28b6c37e8 etc/build.props --- a/etc/build.props Mon Oct 31 11:04:54 2022 +0100 +++ b/etc/build.props Mon Oct 31 15:50:13 2022 +0100 @@ -11,8 +11,8 @@ src/HOL/Tools/Mirabelle/mirabelle.scala \ src/HOL/Tools/Nitpick/kodkod.scala \ src/Pure/Admin/afp.scala \ + src/Pure/Admin/build_csdp.scala \ src/Pure/Admin/build_cvc5.scala \ - src/Pure/Admin/build_csdp.scala \ src/Pure/Admin/build_cygwin.scala \ src/Pure/Admin/build_doc.scala \ src/Pure/Admin/build_e.scala \ @@ -21,6 +21,7 @@ src/Pure/Admin/build_jcef.scala \ src/Pure/Admin/build_jdk.scala \ src/Pure/Admin/build_jedit.scala \ + src/Pure/Admin/build_lipics.scala \ src/Pure/Admin/build_log.scala \ src/Pure/Admin/build_minisat.scala \ src/Pure/Admin/build_pdfjs.scala \ diff -r 9d3b9e89455f -r fac28b6c37e8 src/Doc/Demo_LIPIcs/Document.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Demo_LIPIcs/Document.thy Mon Oct 31 15:50: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 9d3b9e89455f -r fac28b6c37e8 src/Doc/Demo_LIPIcs/document/root.bib --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Demo_LIPIcs/document/root.bib Mon Oct 31 15:50: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 9d3b9e89455f -r fac28b6c37e8 src/Doc/Demo_LIPIcs/document/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Demo_LIPIcs/document/root.tex Mon Oct 31 15:50:13 2022 +0100 @@ -0,0 +1,59 @@ +\documentclass[a4paper,UKenglish,cleveref,autoref]{lipics-v2021} + +\usepackage{isabelle,isabellesym} +\isabellestyle{it} + +\isadroptag{theory} +\isafoldtag{proof} + + +\bibliographystyle{plainurl}% the mandatory bibstyle (e.g. from texlive-bibtex-extra) + +\title{Isabelle document preparation with Dagstuhl LIPIcs style} + +\author{Makarius Wenzel}{Augsburg, Germany \and \url{https://sketis.net}}{}{https://orcid.org/0000-0002-3753-8280}{} +\authorrunning{M. Wenzel} + +\Copyright{} + +\ccsdesc[100]{General and reference~General literature} +\ccsdesc[100]{General and reference} + +\keywords{Document preparation} + +\category{} + +\nolinenumbers + +%\hideLIPIcs %uncomment to remove references to LIPIcs series (logo, DOI, ...), e.g. when preparing a pre-final version to be uploaded to arXiv or another public repository + +%Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\EventEditors{John Q. Open and Joan R. Access} +\EventNoEds{2} +\EventLongTitle{42nd Conference on Very Important Topics (CVIT 2016)} +\EventShortTitle{CVIT 2016} +\EventAcronym{CVIT} +\EventYear{2016} +\EventDate{December 24--27, 2016} +\EventLocation{Little Whinging, United Kingdom} +\EventLogo{} +\SeriesVolume{42} +\ArticleNo{23} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\begin{document} + +\maketitle + +\begin{abstract} +Isabelle is a formal document preparation system. This example shows how to +use it together with the Dagstuhl LIPIcs style. See +\url{https://www.dagstuhl.de/en/publications/lipics/instructions-for-authors} +for further information. +\end{abstract} + +\input{session} + +\bibliography{root} + +\end{document} diff -r 9d3b9e89455f -r fac28b6c37e8 src/Doc/ROOT --- a/src/Doc/ROOT Mon Oct 31 11:04:54 2022 +0100 +++ b/src/Doc/ROOT Mon Oct 31 15:50:13 2022 +0100 @@ -488,3 +488,16 @@ document_files "root.tex" "style.sty" + +session Demo_LIPIcs (doc) in "Demo_LIPIcs" = HOL + + options [document_variants = "demo_lipics", + document_build = "pdflatex", document_heading_prefix = "", document_comment_latex] + theories + Document + document_files (in "$ISABELLE_LIPICS_HOME") + "cc-by.pdf" + "lipics-logo-bw.pdf" + "lipics-v2021.cls" + document_files + "root.bib" + "root.tex" diff -r 9d3b9e89455f -r fac28b6c37e8 src/Pure/Admin/build_lipics.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Admin/build_lipics.scala Mon Oct 31 15:50:13 2022 +0100 @@ -0,0 +1,107 @@ +/* Title: Pure/Admin/build_lipics.scala + Author: Makarius + +Build Isabelle component for Dagstuhl LIPIcs style. + +See also: + + - https://github.com/dagstuhl-publishing/styles + - https://submission.dagstuhl.de/documentation/authors + - https://www.dagstuhl.de/en/publications/lipics +*/ + +package isabelle + + +object Build_LIPIcs { + /* build lipics component */ + + val default_url = "https://github.com/dagstuhl-publishing/styles/archive/refs/tags/v2021.1.2.tar.gz" + + def build_lipics( + download_url: String = default_url, + target_dir: Path = Path.current, + progress: Progress = new Progress + ): Unit = { + Isabelle_System.with_tmp_file("download", ext = "tar.gz") { download_file => + Isabelle_System.with_tmp_dir("download") { download_dir => + + /* download */ + + Isabelle_System.download_file(download_url, download_file, progress = progress) + Isabelle_System.gnutar("-xzf " + File.bash_path(download_file), + dir = download_dir, strip = 1).check + + val lipics_dir = download_dir + Path.explode("LIPIcs/authors") + + + /* component */ + + val version = { + val Version = """^*.* v(.*)$""".r + val changelog = Path.explode("CHANGELOG.md") + split_lines(File.read(lipics_dir + changelog)) + .collectFirst({ case Version(v) => v }) + .getOrElse(error("Failed to detect version in " + changelog)) + } + + val component = "lipics-" + version + val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component)) + progress.echo("Component " + component_dir) + + Isabelle_System.copy_dir(lipics_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_LIPICS_HOME="$COMPONENT/authors" +""") + + + /* README */ + + File.write(component_dir + Path.basic("README"), + """This is the Dagstuhl LIPIcs style for authors from +""" + download_url + """ + + + Makarius + """ + Date.Format.date(Date.now()) + "\n") + } + } + } + + + /* Isabelle tool wrapper */ + + val isabelle_tool = + Isabelle_Tool("build_lipics", "build component for Dagstuhl LIPIcs style", + Scala_Project.here, + { args => + var target_dir = Path.current + var download_url = default_url + + val getopts = Getopts(""" +Usage: isabelle build_lipics [OPTIONS] + + Options are: + -D DIR target directory (default ".") + -U URL download URL (default: """" + default_url + """") + + Build component for Dagstuhl LIPIcs 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_lipics(download_url = download_url, target_dir = target_dir, progress = progress) + }) +} diff -r 9d3b9e89455f -r fac28b6c37e8 src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala Mon Oct 31 11:04:54 2022 +0100 +++ b/src/Pure/System/isabelle_tool.scala Mon Oct 31 15:50:13 2022 +0100 @@ -163,6 +163,7 @@ Build_JCEF.isabelle_tool, Build_JDK.isabelle_tool, Build_JEdit.isabelle_tool, + Build_LIPIcs.isabelle_tool, Build_Minisat.isabelle_tool, Build_PDFjs.isabelle_tool, Build_PolyML.isabelle_tool1, diff -r 9d3b9e89455f -r fac28b6c37e8 src/Pure/Tools/build_docker.scala --- a/src/Pure/Tools/build_docker.scala Mon Oct 31 11:04:54 2022 +0100 +++ b/src/Pure/Tools/build_docker.scala Mon Oct 31 15:50:13 2022 +0100 @@ -20,7 +20,12 @@ val package_collections: Map[String, List[String]] = Map("X11" -> List("libx11-6", "libxext6", "libxrender1", "libxtst6", "libxi6"), "latex" -> - List("texlive-fonts-extra", "texlive-font-utils", "texlive-latex-extra", "texlive-science")) + List( + "texlive-bibtex-extra", + "texlive-fonts-extra", + "texlive-font-utils", + "texlive-latex-extra", + "texlive-science")) def all_packages: List[String] = packages ::: package_collections.valuesIterator.flatten.toList