# HG changeset patch # User paulson # Date 1633360278 -3600 # Node ID aca96bd12b12bcb658a8027c780de2b8198fab75 # Parent e1b5bf983de36a6d300df3cc385f8646bd05d450# Parent c278b186459227c79596a4be8028e283cd90badd merged diff -r c278b1864592 -r aca96bd12b12 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Mon Oct 04 16:10:55 2021 +0100 +++ b/Admin/components/components.sha1 Mon Oct 04 16:11:18 2021 +0100 @@ -124,6 +124,7 @@ b166b4bd583b6442a5d75eab06f7adbb66919d6d isabelle_fonts-20210319.tar.gz 9467ad54a9ac10a6e7e8db5458d8d2a5516eba96 isabelle_fonts-20210321.tar.gz 1f7a0b9829ecac6552b21e995ad0f0ac168634f3 isabelle_fonts-20210322.tar.gz +667000ce6dd6ea3c2d11601a41c206060468807d isabelle_fonts-20211004.tar.gz 916adccd2f40c55116b68b92ce1eccb24d4dd9a2 isabelle_setup-20210630.tar.gz c611e363287fcc9bdd93c33bef85fa4e66cd3f37 isabelle_setup-20210701.tar.gz a0e7527448ef0f7ce164a38a50dc26e98de3cad6 isabelle_setup-20210709.tar.gz diff -r c278b1864592 -r aca96bd12b12 Admin/components/main --- a/Admin/components/main Mon Oct 04 16:10:55 2021 +0100 +++ b/Admin/components/main Mon Oct 04 16:11:18 2021 +0100 @@ -7,7 +7,7 @@ e-2.6 flatlaf-1.6 idea-icons-20210508 -isabelle_fonts-20210322 +isabelle_fonts-20211004 isabelle_setup-20210922 jdk-17+35 jedit-20210802 diff -r c278b1864592 -r aca96bd12b12 Admin/isabelle_fonts/IsabelleSymbols.sfd --- a/Admin/isabelle_fonts/IsabelleSymbols.sfd Mon Oct 04 16:10:55 2021 +0100 +++ b/Admin/isabelle_fonts/IsabelleSymbols.sfd Mon Oct 04 16:11:18 2021 +0100 @@ -20,7 +20,7 @@ OS2_WeightWidthSlopeOnly: 0 OS2_UseTypoMetrics: 1 CreationTime: 1050361371 -ModificationTime: 1616429436 +ModificationTime: 1633346733 PfmFamily: 17 TTFWeight: 400 TTFWidth: 5 @@ -2242,11 +2242,11 @@ DisplaySize: -96 AntiAlias: 1 FitToEm: 1 -WinInfo: 10980 12 6 +WinInfo: 8196 12 6 BeginPrivate: 0 EndPrivate TeXData: 1 0 0 631296 315648 210432 572416 -1048576 210432 783286 444596 497025 792723 393216 433062 380633 303038 157286 324010 404750 52429 2506097 1059062 262144 -BeginChars: 1114189 1462 +BeginChars: 1114189 1463 StartChar: u10000 Encoding: 65536 65536 0 @@ -63624,5 +63624,44 @@ 1271 1288 1271 1288 1271 1280 c 0,0,1 EndSplineSet EndChar + +StartChar: uni2016 +Encoding: 8214 8214 1462 +Width: 1408 +VWidth: 3930 +Flags: W +VStem: 324.48 188.739<-502.563 1702.56> 912.78 188.739<-500.697 1716.06> +LayerCount: 2 +Fore +SplineSet +324.48046875 1636.74023438 m 2,0,1 + 324.48046875 1676.40625 324.48046875 1676.40625 352.905273438 1703.41015625 c 0,2,3 + 380.89453125 1730 380.89453125 1730 419.959960938 1730 c 0,4,5 + 438.3125 1730 438.3125 1730 454.934570312 1722.7734375 c 128,-1,6 + 471.557617188 1715.546875 471.557617188 1715.546875 485.162109375 1701.94238281 c 128,-1,7 + 498.767578125 1688.3359375 498.767578125 1688.3359375 505.994140625 1671.71582031 c 128,-1,8 + 513.219726562 1655.09667969 513.219726562 1655.09667969 513.219726562 1636.74023438 c 2,9,-1 + 513.219726562 -436.740234375 l 2,10,11 + 513.219726562 -473.883789062 513.219726562 -473.883789062 485.162109375 -501.94140625 c 128,-1,12 + 457.104492188 -530 457.104492188 -530 419.959960938 -530 c 0,13,14 + 380.89453125 -530 380.89453125 -530 352.904296875 -503.41015625 c 0,15,16 + 324.48046875 -476.40625 324.48046875 -476.40625 324.48046875 -436.740234375 c 2,17,-1 + 324.48046875 1636.74023438 l 2,0,1 +1101.51953125 -436.740234375 m 2,18,19 + 1101.51953125 -473.584960938 1101.51953125 -473.584960938 1074.9296875 -501.57421875 c 0,20,21 + 1047.92578125 -530 1047.92578125 -530 1008.25976562 -530 c 0,22,23 + 969.194335938 -530 969.194335938 -530 941.206054688 -503.41015625 c 0,24,25 + 912.780273438 -476.40625 912.780273438 -476.40625 912.780273438 -436.740234375 c 2,26,-1 + 912.780273438 1636.74023438 l 2,27,28 + 912.780273438 1656.08203125 912.780273438 1656.08203125 920.038085938 1673.13964844 c 128,-1,29 + 927.295898438 1690.19628906 927.295898438 1690.19628906 941.205078125 1703.41015625 c 0,30,31 + 969.194335938 1730 969.194335938 1730 1008.25976562 1730 c 0,32,33 + 1027.6015625 1730 1027.6015625 1730 1044.65917969 1722.7421875 c 128,-1,34 + 1061.71582031 1715.484375 1061.71582031 1715.484375 1074.9296875 1701.57421875 c 0,35,36 + 1087.87402344 1687.94921875 1087.87402344 1687.94921875 1094.69628906 1671.43066406 c 128,-1,37 + 1101.51953125 1654.91113281 1101.51953125 1654.91113281 1101.51953125 1636.74023438 c 2,38,-1 + 1101.51953125 -436.740234375 l 2,18,19 +EndSplineSet +EndChar EndChars EndSplineFont diff -r c278b1864592 -r aca96bd12b12 Admin/isabelle_fonts/IsabelleSymbolsBold.sfd --- a/Admin/isabelle_fonts/IsabelleSymbolsBold.sfd Mon Oct 04 16:10:55 2021 +0100 +++ b/Admin/isabelle_fonts/IsabelleSymbolsBold.sfd Mon Oct 04 16:11:18 2021 +0100 @@ -21,7 +21,7 @@ OS2_WeightWidthSlopeOnly: 0 OS2_UseTypoMetrics: 1 CreationTime: 1050374980 -ModificationTime: 1616429477 +ModificationTime: 1633346753 PfmFamily: 17 TTFWeight: 700 TTFWidth: 5 @@ -1679,10 +1679,10 @@ DisplaySize: -96 AntiAlias: 1 FitToEm: 1 -WinInfo: 10978 11 8 +WinInfo: 8195 11 8 BeginPrivate: 0 EndPrivate -BeginChars: 1114115 1450 +BeginChars: 1114115 1451 StartChar: .notdef Encoding: 1114112 -1 0 @@ -71737,5 +71737,63 @@ 1131.20656165 1403 1131.20656165 1403 1167.81653987 1380.08960467 c 1,0,1 EndSplineSet EndChar + +StartChar: uni2016 +Encoding: 8214 8214 1450 +Width: 1408 +VWidth: 3930 +Flags: W +LayerCount: 2 +Fore +SplineSet +273.48046875 1636.74023438 m 2 + 274.305963608 1698.42980182 274.305963608 1698.42980182 317.779016975 1740.38509515 c 0 + 331.5651659 1753.48196068 331.5651659 1753.48196068 348.024849563 1762.58337143 c 0 + 364.484533226 1771.68478217 364.484533226 1771.68478217 382.684388387 1776.34239109 c 0 + 400.884243548 1781 400.884243548 1781 419.959960938 1781 c 0 + 434.214451746 1781 434.214451746 1781 448.226135404 1778.10483503 c 0 + 462.237819061 1775.20967007 462.237819061 1775.20967007 475.267592525 1769.544884 c 0 + 500.772123393 1758.45726043 500.772123393 1758.45726043 521.225849377 1738.00353445 c 0 + 527.877534153 1731.35137223 527.877534153 1731.35137223 533.617741307 1724.04056682 c 0 + 539.357948462 1716.7297614 539.357948462 1716.7297614 544.207481245 1708.65391055 c 0 + 549.057014029 1700.5780597 549.057014029 1700.5780597 552.764844573 1692.05055051 c 0 + 564.219726562 1665.70385748 564.219726562 1665.70385748 564.219726562 1636.74023438 c 2 + 564.219726562 -436.740234375 l 2 + 564.219726562 -495.008680733 564.219726562 -495.008680733 521.225182787 -538.003224508 c 0 + 507.658300589 -551.57057891 507.658300589 -551.57057891 491.595678193 -561.145395835 c 0 + 475.533055797 -570.720212761 475.533055797 -570.720212761 457.267144636 -575.860106381 c 0 + 439.001233476 -581 439.001233476 -581 419.959960938 -581 c 0 + 391.253451691 -581 391.253451691 -581 364.896337999 -570.553783949 c 0 + 338.539224308 -560.107567898 338.539224308 -560.107567898 317.777206298 -540.384302725 c 0 + 296.387100388 -520.062746736 296.387100388 -520.062746736 284.933784569 -493.217738834 c 0 + 273.48046875 -466.372730933 273.48046875 -466.372730933 273.48046875 -436.740234375 c 2 + 273.48046875 1636.74023438 l 2 +1152.51953125 -436.740234375 m 2 + 1151.74952957 -494.144209416 1151.74952957 -494.144209416 1111.90503919 -536.700040691 c 0 + 1091.58360184 -558.091491525 1091.58360184 -558.091491525 1064.73824301 -569.545745762 c 0 + 1037.89288418 -581 1037.89288418 -581 1008.25976562 -581 c 0 + 979.553949558 -581 979.553949558 -581 953.196369328 -570.553430392 c 0 + 926.838789099 -560.106860784 926.838789099 -560.106860784 906.080232746 -540.385507945 c 0 + 861.780273438 -498.301459752 861.780273438 -498.301459752 861.780273438 -436.740234375 c 2 + 861.780273438 1636.74023438 l 2 + 861.780273438 1651.32239562 861.780273438 1651.32239562 864.624564811 1665.58641717 c 0 + 867.468856184 1679.85043872 867.468856184 1679.85043872 873.10986998 1693.10818737 c 0 + 878.772167602 1706.41519628 878.772167602 1706.41519628 887.133373164 1718.37257459 c 0 + 895.494578727 1730.3299529 895.494578727 1730.3299529 906.078821663 1740.38509515 c 0 + 948.831274571 1781 948.831274571 1781 1008.25976562 1781 c 0 + 1038.00042276 1781 1038.00042276 1781 1064.62771862 1769.67040346 c 0 + 1073.50484059 1765.89307777 1073.50484059 1765.89307777 1081.84644385 1760.86774412 c 0 + 1090.18804712 1755.84241046 1090.18804712 1755.84241046 1097.70707391 1749.78666415 c 0 + 1105.2261007 1743.73091784 1105.2261007 1743.73091784 1111.90386462 1736.70127707 c 0 + 1116.65951952 1731.69555114 1116.65951952 1731.69555114 1120.93180299 1726.3118946 c 0 + 1125.20408645 1720.92823807 1125.20408645 1720.92823807 1128.97353615 1715.18962916 c 0 + 1132.74298584 1709.45102026 1132.74298584 1709.45102026 1135.97975475 1703.34407818 c 0 + 1139.21652366 1697.2371361 1139.21652366 1697.2371361 1141.83366456 1690.90032844 c 0 + 1145.36294721 1682.35569623 1145.36294721 1682.35569623 1147.74798058 1673.36655214 c 0 + 1150.13301394 1664.37740804 1150.13301394 1664.37740804 1151.3262726 1655.19274645 c 0 + 1152.51953125 1646.00808487 1152.51953125 1646.00808487 1152.51953125 1636.74023438 c 2 + 1152.51953125 -436.740234375 l 2 +EndSplineSet +EndChar EndChars EndSplineFont diff -r c278b1864592 -r aca96bd12b12 CONTRIBUTORS --- a/CONTRIBUTORS Mon Oct 04 16:10:55 2021 +0100 +++ b/CONTRIBUTORS Mon Oct 04 16:11:18 2021 +0100 @@ -6,6 +6,9 @@ Contributions to Isabelle2021-1 ------------------------------- +* July .. September 2021: Makarius Wenzel + Significantly improved Isabelle/Haskell library. + * July 2021: Florian Haftmann Further consolidation of bit operations and word types. diff -r c278b1864592 -r aca96bd12b12 NEWS --- a/NEWS Mon Oct 04 16:10:55 2021 +0100 +++ b/NEWS Mon Oct 04 16:11:18 2021 +0100 @@ -4,8 +4,8 @@ (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.) -New in Isabelle2021 (December 2021) ------------------------------------ +New in Isabelle2021-1 (December 2021) +------------------------------------- *** General *** @@ -30,6 +30,13 @@ See also the group "Z Notation" in the Symbols dockable of Isabelle/jEdit. +* The Isabelle/Haskell library ($ISABELLE_HOME/src/Tools/Haskell) has +been significantly improved. In particular, module Isabelle.Bytes +provides type Bytes for light-weight byte strings (with optional UTF8 +interpretation), similar to type string in Isabelle/ML. Isabelle symbols +now work uniformly in Isabelle/Haskell vs. Isabelle/ML vs. +Isabelle/Scala/PIDE. + *** Isar *** @@ -59,8 +66,8 @@ *** Document preparation *** -* More predefined symbols: \ \ (package "stmaryrd"), \ \ (LaTeX package -"pifont"). +* More predefined symbols: \ \ \ (package "stmaryrd"), \ \ (LaTeX +package "pifont"). * High-quality blackboard-bold symbols from font "txmia" (LaTeX package "pxfonts"): \\\\\\\\\\\\\\\\\\\\\\\\\\. @@ -183,13 +190,20 @@ INCOMPATIBILITY. * Sledgehammer: - - Removed legacy "lam_lifting" (synonym for "lifting") from option - "lam_trans". Minor INCOMPATIBILITY. - - Renamed "hide_lams" to "opaque_lifting" in option "lam_trans". Minor - INCOMPATIBILITY. - - Added "opaque_combs" to option "lam_trans": lambda expressions are - rewritten using combinators, but the combinators are kept opaque, - i.e. without definitions. + - Update of bundled provers: + E 2.6 + Vampire 4.5.1 (with Open Source license) + veriT 2021.06-rmx + Zipperposition 2.1 + - Adjusted default provers: + cvc4 vampire verit e spass z3 zipperposition + - Removed legacy "lam_lifting" (synonym for "lifting") from option + "lam_trans". Minor INCOMPATIBILITY. + - Renamed "hide_lams" to "opaque_lifting" in option "lam_trans". Minor + INCOMPATIBILITY. + - Added "opaque_combs" to option "lam_trans": lambda expressions are + rewritten using combinators, but the combinators are kept opaque, + i.e. without definitions. * Metis: Renamed option "hide_lams" to "opaque_lifting". Minor INCOMPATIBILITY. @@ -329,8 +343,11 @@ The main Isabelle/ML interface is Isabelle_System.bash_process with result type Process_Result.T (resembling class Process_Result in Scala); derived operations Isabelle_System.bash and Isabelle_System.bash_output -provide similar functionality as before. Rare INCOMPATIBILITY due to -subtle semantic differences: +provide similar functionality as before. The underlying TCP/IP server +within Isabelle/Scala is available to other programming languages as +well, notably Isabelle/Haskell. + +Rare INCOMPATIBILITY due to subtle semantic differences: - Processes invoked from Isabelle/ML actually run in the context of the Java VM of Isabelle/Scala. The settings environment and current @@ -352,20 +369,19 @@ like Isabelle_System.with_tmp_file to create a file name and File.read to retrieve its content. - - Just like any other Scala function invoked from ML, - Isabelle_System.bash_process requires a proper PIDE session context. - This could be a regular batch session (e.g. "isabelle build"), a - PIDE editor session (e.g. "isabelle jedit"), or headless PIDE (e.g. - "isabelle dump" or "isabelle server"). Note that old "isabelle - console" or raw "isabelle process" don't have that. + - The Isabelle/Scala "bash_process" server requires a PIDE session + context. This could be a regular batch session (e.g. "isabelle + build"), a PIDE editor session (e.g. "isabelle jedit"), or headless + PIDE (e.g. "isabelle dump" or "isabelle server"). Note that old + "isabelle console" or raw "isabelle process" don't have that. New Process_Result.timing works as in Isabelle/Scala, based on direct measurements of the bash_process wrapper in C: elapsed time is always available, CPU time is only available on Linux and macOS, GC time is unavailable. -* Likewise, the following Isabelle/ML system operations are run in the -context of Isabelle/Scala: +* The following Isabelle/ML system operations are run in the context of +Isabelle/Scala, within a PIDE session context: - Isabelle_System.make_directory - Isabelle_System.copy_dir @@ -388,6 +404,8 @@ *** System *** +* Update to OpenJDK 17: the current long-term support version of Java. + * Each Isabelle component may specify a Scala/Java jar module declaratively via etc/build.props (file names are relative to the component directory). E.g. see $ISABELLE_HOME/etc/build.props with diff -r c278b1864592 -r aca96bd12b12 etc/symbols --- a/etc/symbols Mon Oct 04 16:10:55 2021 +0100 +++ b/etc/symbols Mon Oct 04 16:11:18 2021 +0100 @@ -301,6 +301,7 @@ \ code: 0x00227c group: relation \ code: 0x00227d group: relation \ code: 0x002225 group: relation abbrev: || +\ code: 0x002016 group: relation abbrev: || \ code: 0x002af4 group: relation abbrev: || \ code: 0x002afd group: relation abbrev: || \ code: 0x0000a6 group: punctuation abbrev: || diff -r c278b1864592 -r aca96bd12b12 lib/texinputs/isabellesym.sty --- a/lib/texinputs/isabellesym.sty Mon Oct 04 16:10:55 2021 +0100 +++ b/lib/texinputs/isabellesym.sty Mon Oct 04 16:11:18 2021 +0100 @@ -303,6 +303,7 @@ \newcommand{\isasympreceq}{\isamath{\preceq}} \newcommand{\isasymsucceq}{\isamath{\succeq}} \newcommand{\isasymparallel}{\isamath{\parallel}} +\newcommand{\isasymParallel}{\isamath{\bigparallel}} %requires stmaryrd \newcommand{\isasyminterleace}{\isamath{\interleave}} %requires stmaryrd \newcommand{\isasymsslash}{\isamath{\sslash}} %requires stmaryrd \newcommand{\isasymbar}{\isamath{\mid}} diff -r c278b1864592 -r aca96bd12b12 src/Doc/Isar_Ref/Symbols.thy --- a/src/Doc/Isar_Ref/Symbols.thy Mon Oct 04 16:10:55 2021 +0100 +++ b/src/Doc/Isar_Ref/Symbols.thy Mon Oct 04 16:11:18 2021 +0100 @@ -37,4 +37,6 @@ \end{center} \ +external_file %invisible \~~/lib/texinputs/isabellesym.sty\ + end diff -r c278b1864592 -r aca96bd12b12 src/Doc/Isar_Ref/document/root.tex --- a/src/Doc/Isar_Ref/document/root.tex Mon Oct 04 16:10:55 2021 +0100 +++ b/src/Doc/Isar_Ref/document/root.tex Mon Oct 04 16:11:18 2021 +0100 @@ -7,7 +7,7 @@ \usepackage{eurosym} \usepackage{pifont} \usepackage[english]{babel} -\usepackage[only,bigsqcap,fatsemi,interleave,sslash]{stmaryrd} +\usepackage[only,bigsqcap,fatsemi,bigparallel,interleave,sslash]{stmaryrd} \usepackage{graphicx} \let\intorig=\int %iman.sty redefines \int \usepackage{iman,extra,isar,proof} diff -r c278b1864592 -r aca96bd12b12 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Oct 04 16:10:55 2021 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Oct 04 16:11:18 2021 +0100 @@ -177,7 +177,7 @@ (* The first ATP of the list is used by Auto Sledgehammer. *) fun default_provers_param_value mode ctxt = - [cvc4N, vampireN, veritN, eN, spassN, z3N, zipperpositionN] + [cvc4N, vampireN, veritN, eN, spassN, z3N, zipperpositionN] \ \see also \<^system_option>\sledgehammer_provers\\ |> map_filter (remotify_prover_if_not_installed ctxt) (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *) |> take (Multithreading.max_threads () - (if mode = Try then 1 else 0)) diff -r c278b1864592 -r aca96bd12b12 src/Pure/Admin/build_fonts.scala --- a/src/Pure/Admin/build_fonts.scala Mon Oct 04 16:10:55 2021 +0100 +++ b/src/Pure/Admin/build_fonts.scala Mon Oct 04 16:11:18 2021 +0100 @@ -57,6 +57,7 @@ 0x2013, // dash 0x2014, // dash 0x2015, // dash + 0x2016, // big parallel 0x2020, // dagger 0x2021, // double dagger 0x2022, // bullet diff -r c278b1864592 -r aca96bd12b12 src/Pure/Tools/mkroot.scala --- a/src/Pure/Tools/mkroot.scala Mon Oct 04 16:10:55 2021 +0100 +++ b/src/Pure/Tools/mkroot.scala Mon Oct 04 16:11:18 2021 +0100 @@ -85,8 +85,8 @@ %\""" + """usepackage{eurosym} %for \ -%\""" + """usepackage[only,bigsqcap,fatsemi,interleave,sslash]{stmaryrd} - %for \, \ +%\""" + """usepackage[only,bigsqcap,bigparallel,fatsemi,interleave,sslash]{stmaryrd} + %for \, \, \, \, \ %\""" + """usepackage{eufrak} %for \ ... \, \ ... \ (also included in amssymb)