--- a/Admin/components/components.sha1 Fri Jan 31 17:01:27 2025 +0100
+++ b/Admin/components/components.sha1 Fri Jan 31 17:01:52 2025 +0100
@@ -254,6 +254,7 @@
5117b7d0283adf31cf2bde17a9912eb775a0822f jedit-20241101.tar.gz
a8b11ddf7f6838ea53868e46cb4555b7fa60e776 jedit-20241115.tar.gz
6a5d78867dc6f692f8f3ab758e3ac1b86fabd3bf jedit-20250129.tar.gz
+011d322d4ae1f8c57112bd695f5e812e48e1d953 jedit-20250130.tar.gz
44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
--- a/Admin/components/main Fri Jan 31 17:01:27 2025 +0100
+++ b/Admin/components/main Fri Jan 31 17:01:52 2025 +0100
@@ -3,7 +3,7 @@
bash_process-20240326
bib2xhtml-20190409
csdp-6.1.1
-cvc4-1.8
+cvc5-1.2.0-1
e-3.1-1
elm-0.19.1
easychair-3.5
@@ -15,7 +15,7 @@
isabelle_setup-20240327
javamail-20250122
jdk-21.0.6
-jedit-20250129
+jedit-20250130
jfreechart-1.5.3
jortho-1.0-2
jsoup-1.18.3
--- a/NEWS Fri Jan 31 17:01:27 2025 +0100
+++ b/NEWS Fri Jan 31 17:01:52 2025 +0100
@@ -245,6 +245,7 @@
* Sledgehammer:
- Update of bundled provers:
. E 3.1 -- with patch on Windows/Cygwin for proper interrupts
+ . cvc5 1.2.0 -- with support for arm64-linux
- Added instantiations of facts using the "of" attribute
(e.g. "assms(1)[of x]"), which can be activated using the
Sledgehammer option "instantiate" (default: smart, i.e. only if
@@ -262,8 +263,6 @@
* Code generator: command 'code_reserved' now uses parentheses for
target languages, similar to 'code_printing'.
-* Theory HOL.List: overloaded power operator (^^) on type list.
-
* Theory "HOL.Wellfounded":
- Removed lemma wellorder.wfP_less. Use wellorder.wfp_on_less instead.
Minor INCOMPATIBILITY.
--- a/src/HOL/Nunchaku.thy Fri Jan 31 17:01:27 2025 +0100
+++ b/src/HOL/Nunchaku.thy Fri Jan 31 17:01:52 2025 +0100
@@ -11,7 +11,7 @@
The "$NUNCHAKU_HOME" environment variable must be set to the absolute path to
the directory containing the "nunchaku" executable. The Isabelle components
-for CVC4, Kodkodi, and SMBC are necessary to use these backend solvers.
+for cvc5, Kodkodi, and SMBC are necessary to use these backend solvers.
*)
theory Nunchaku
--- a/src/HOL/TPTP/atp_problem_import.ML Fri Jan 31 17:01:27 2025 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML Fri Jan 31 17:01:52 2025 +0100
@@ -239,7 +239,7 @@
(auto_tac lthy THEN ALLGOALS (atp_tac lthy 0 [] (timeout div 5) assms ATP_Proof.spassN))
ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac lthy i)
ORELSE SOLVE_TIMEOUT (timeout div 20) "z3" (smt_solver_tac "z3" lthy i)
- ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc4" (smt_solver_tac "cvc4" lthy i)
+ ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc5" (smt_solver_tac "cvc5" lthy i)
ORELSE SOLVE_TIMEOUT (timeout div 20) "best" (best_tac lthy i)
ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac lthy i)
ORELSE SOLVE_TIMEOUT (timeout div 10) "meson" (Meson.meson_tac lthy [] i)
--- a/src/HOL/Tools/ATP/atp_proof.ML Fri Jan 31 17:01:27 2025 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Fri Jan 31 17:01:52 2025 +0100
@@ -43,7 +43,7 @@
val agsyholN : string
val alt_ergoN : string
- val cvc4N : string
+ val cvc5N : string
val eN : string
val iproverN : string
val leo2N : string
@@ -111,7 +111,7 @@
val agsyholN = "agsyhol"
val alt_ergoN = "alt_ergo"
-val cvc4N = "cvc4"
+val cvc5N = "cvc5"
val eN = "e"
val iproverN = "iprover"
val leo2N = "leo2"
--- a/src/HOL/Tools/Nunchaku/nunchaku_commands.ML Fri Jan 31 17:01:27 2025 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_commands.ML Fri Jan 31 17:01:52 2025 +0100
@@ -30,7 +30,7 @@
("max_genuine", "1"),
("max_potential", "1"),
("overlord", "false"),
- ("solvers", "cvc4 kodkod paradox smbc"),
+ ("solvers", "cvc5 kodkod paradox smbc"),
("specialize", "true"),
("spy", "false"),
("timeout", "30"),
--- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML Fri Jan 31 17:01:27 2025 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML Fri Jan 31 17:01:52 2025 +0100
@@ -86,7 +86,7 @@
else
let
val bash_cmd =
- "PATH=\"$CVC4_HOME:$KODKODI/bin:$SMBC_HOME:$PATH\" \"$" ^
+ "PATH=\"$CVC5_HOME:$KODKODI/bin:$SMBC_HOME:$PATH\" \"$" ^
nunchaku_home_env_var ^ "\"/nunchaku --skolems-in-model --no-color " ^
(if specialize then "" else "--no-specialize ") ^
"--solvers \"" ^ space_implode "," (map Bash.string solvers) ^ "\" " ^
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Jan 31 17:01:27 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Jan 31 17:01:52 2025 +0100
@@ -388,10 +388,10 @@
val default_slice_schedule =
(* FUDGE (loosely inspired by Seventeen evaluation) *)
- [cvc4N, zipperpositionN, vampireN, veritN, spassN, zipperpositionN, eN, cvc4N, zipperpositionN,
- cvc4N, eN, zipperpositionN, vampireN, cvc4N, cvc4N, vampireN, cvc4N, iproverN, zipperpositionN,
+ [cvc5N, zipperpositionN, vampireN, veritN, spassN, zipperpositionN, eN, cvc5N, zipperpositionN,
+ cvc5N, eN, zipperpositionN, vampireN, cvc5N, cvc5N, vampireN, cvc5N, iproverN, zipperpositionN,
spassN, vampireN, zipperpositionN, vampireN, zipperpositionN, z3N, zipperpositionN, vampireN,
- iproverN, spassN, zipperpositionN, vampireN, cvc4N, zipperpositionN, z3N, z3N, cvc4N,
+ iproverN, spassN, zipperpositionN, vampireN, cvc5N, zipperpositionN, z3N, z3N, cvc5N,
zipperpositionN]
fun schedule_of_provers provers num_slices =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Fri Jan 31 17:01:27 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Fri Jan 31 17:01:52 2025 +0100
@@ -315,7 +315,7 @@
val leo3_config : atp_config =
{exec = (["LEO3_HOME"], ["leo3"]),
arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn problem =>
- [File.bash_path problem ^ " " ^ "--atp cvc=\"$CVC4_SOLVER\" --atp e=\"$E_HOME\"/eprover \
+ [File.bash_path problem ^ " " ^ "--atp cvc=\"$CVC5_SOLVER\" --atp e=\"$E_HOME\"/eprover \
\-p -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^
(if full_proofs then "--nleq --naeq " else "")],
proof_delims = tstp_proof_delims,
--- a/src/HOL/Tools/etc/options Fri Jan 31 17:01:27 2025 +0100
+++ b/src/HOL/Tools/etc/options Fri Jan 31 17:01:52 2025 +0100
@@ -26,7 +26,7 @@
section "Miscellaneous Tools"
-public option sledgehammer_provers : string = "cvc4 verit z3 e spass vampire zipperposition"
+public option sledgehammer_provers : string = "cvc5 verit z3 e spass vampire zipperposition"
-- "provers for Sledgehammer (separated by blanks)"
public option sledgehammer_timeout : int = 30
--- a/src/Pure/Admin/build_release.scala Fri Jan 31 17:01:27 2025 +0100
+++ b/src/Pure/Admin/build_release.scala Fri Jan 31 17:01:52 2025 +0100
@@ -420,7 +420,10 @@
def build_release_archive(
context: Release_Context,
version: String,
- parallel_jobs: Int = 1
+ parallel_jobs: Int = 1,
+ build_library: Boolean = false,
+ include_library: Boolean = false,
+ include_find_facts: Boolean = false
): Unit = {
val progress = context.progress
@@ -457,10 +460,13 @@
record_bundled_components(context.isabelle_dir)
- /* build tools and documentation */
+ /* build documentation and internal HTML library */
val other_isabelle = context.other_isabelle(context.dist_dir)
+ def other_isabelle_purge(name: String): Unit =
+ Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.basic(name))
+
other_isabelle.init(echo = true)
try {
@@ -471,11 +477,47 @@
make_news(other_isabelle)
- for (name <- List("Admin", "browser_info", "heaps")) {
- Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name))
+ other_isabelle_purge("browser_info")
+
+ if (build_library || include_library || include_find_facts) {
+ require(Platform.is_unix, "Linux or macOS platform required")
+
+ val opt_dirs = "-d '~~/src/Benchmarks' "
+ other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs +
+ " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
+ " -o system_heaps -a " + opt_dirs, echo = true).check
+
+ if (include_find_facts) {
+ val database_name = "isabelle"
+ val database_dir =
+ other_isabelle.expand_path(
+ Path.explode("$FIND_FACTS_HOME_USER/solr") + Path.basic(database_name))
+ val database_target_dir =
+ other_isabelle.expand_path(
+ Path.explode("$FIND_FACTS_HOME/lib/find_facts-" + database_name))
+
+ val sessions =
+ other_isabelle.bash("bin/isabelle sessions -a " + opt_dirs).check.out_lines
+ other_isabelle.bash(
+ "bin/isabelle find_facts_index -o find_facts_database_name=" +
+ Bash.string(database_name) + " -n " + opt_dirs +
+ Bash.strings(sessions), echo = true).check
+ Isabelle_System.make_directory(database_target_dir)
+ Isabelle_System.copy_dir(database_dir, database_target_dir, direct = true)
+
+ Isabelle_System.rm_tree(database_dir)
+ database_dir.dir.file.delete // "$FIND_FACTS_HOME_USER/solr"
+ database_dir.dir.dir.file.delete // "$FIND_FACTS_HOME_USER"
+ }
+
+ if (!include_library) other_isabelle_purge("browser_info")
}
+ other_isabelle_purge("Admin")
+ other_isabelle_purge("heaps")
+
other_isabelle.cleanup()
+ other_isabelle.isabelle_home_user.file.delete
progress.echo_warning("Creating release archive " + context.isabelle_archive + " ...")
@@ -485,6 +527,12 @@
"""find . -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w""")
execute_tar(context.dist_dir, "-czf " +
File.bash_path(context.isabelle_archive) + " " + Bash.string(context.dist_name))
+
+ if (build_library) {
+ progress.echo_warning("Creating library archive " + context.isabelle_library_archive + " ...")
+ execute_tar(context.dist_dir, "-czf " + File.bash_path(context.isabelle_library_archive) +
+ " " + Bash.string(context.dist_name + "/browser_info"))
+ }
}
}
@@ -498,7 +546,6 @@
more_components: List[Path] = Nil,
website: Option[Path] = None,
build_sessions: List[String] = Nil,
- build_library: Boolean = false,
parallel_jobs: Int = 1
): Unit = {
val progress = context.progress
@@ -828,37 +875,6 @@
Isabelle_System.copy_file(context.dist_dir + Path.explode(bundle), dir)
}
}
-
-
- /* HTML library */
-
- if (build_library) {
- if (context.isabelle_library_archive.is_file) {
- progress.echo_warning("Library archive already exists: " + context.isabelle_library_archive)
- }
- else {
- require(Platform.is_unix, "Linux or macOS platform required")
- Isabelle_System.with_tmp_dir("build_release") { tmp_dir =>
- val bundle = context.dist_name + "_" + Platform.family + ".tar.gz"
- val bundle_path = context.dist_dir + Path.basic(bundle)
- execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle_path))
-
- val other_isabelle = context.other_isabelle(tmp_dir)
-
- Isabelle_System.make_directory(other_isabelle.etc)
- File.write(other_isabelle.etc_settings, "ML_OPTIONS=\"--minheap 1000 --maxheap 4000\"\n")
-
- other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs +
- " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
- " -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check
- other_isabelle.isabelle_home_user.file.delete
-
- execute(tmp_dir, "chmod -R a+r,g=o " + Bash.string(context.dist_name))
- execute_tar(tmp_dir, "-czf " + File.bash_path(context.isabelle_library_archive) +
- " " + Bash.string(context.dist_name + "/browser_info"))
- }
- }
- }
}
@@ -869,6 +885,8 @@
Command_Line.tool {
var afp_rev = ""
var target_dir = Path.current
+ var include_find_facts = false
+ var include_library = false
var release_name = ""
var source_archive = ""
var website: Option[Path] = None
@@ -886,13 +904,15 @@
Options are:
-A REV corresponding AFP changeset id
-D DIR target directory (default ".")
+ -F include library: Find_Facts data
+ -L include library: HTML presentation
-R RELEASE explicit release name
-S ARCHIVE use existing source archive (file or URL)
-W WEBSITE produce minimal website in given directory
-b SESSIONS build platform-specific session images (separated by commas)
-c ARCHIVE clean bundling with additional component .tar.gz archive
-j INT maximum number of parallel jobs (default 1)
- -l build library
+ -l build library archive
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-p NAMES platform families (default: """ + quote(default_platform_families.mkString(",")) + """)
-r REV Mercurial changeset id (default: ARCHIVE or RELEASE or tip)
@@ -901,6 +921,8 @@
""",
"A:" -> (arg => afp_rev = arg),
"D:" -> (arg => target_dir = Path.explode(arg)),
+ "F" -> (_ => include_find_facts = true),
+ "L" -> (_ => include_library = true),
"R:" -> (arg => release_name = arg),
"S:" -> (arg => source_archive = arg),
"W:" -> (arg => website = Some(Path.explode(arg))),
@@ -931,7 +953,9 @@
if (source_archive.isEmpty) {
val context = make_context(release_name)
val version = proper_string(rev) orElse proper_string(release_name) getOrElse "tip"
- build_release_archive(context, version, parallel_jobs = parallel_jobs)
+ build_release_archive(context, version, parallel_jobs = parallel_jobs,
+ build_library = build_library, include_library = include_library,
+ include_find_facts = include_find_facts)
context
}
else {
@@ -945,7 +969,7 @@
build_release(options, context, afp_rev = afp_rev, platform_families = platform_families,
more_components = more_components, build_sessions = build_sessions,
- build_library = build_library, parallel_jobs = parallel_jobs, website = website)
+ parallel_jobs = parallel_jobs, website = website)
}
}
}
--- a/src/Pure/Admin/component_jedit.scala Fri Jan 31 17:01:27 2025 +0100
+++ b/src/Pure/Admin/component_jedit.scala Fri Jan 31 17:01:52 2025 +0100
@@ -197,6 +197,8 @@
Isabelle_System.download_file(url, jars_dir + Path.basic(name), progress = progress)
}
+ (jars_dir + Path.basic("MacOS.jar")).file.delete
+
for { (name, vers) <- download_plugins } {
Isabelle_System.with_tmp_file("tmp", ext = "zip") { zip_path =>
val url =
--- a/src/Pure/Build/browser_info.scala Fri Jan 31 17:01:27 2025 +0100
+++ b/src/Pure/Build/browser_info.scala Fri Jan 31 17:01:52 2025 +0100
@@ -51,8 +51,8 @@
}
}
- def init_directory(dir: Path): Path = {
- check_directory(dir)
+ def init_directory(dir: Path, permissive: Boolean = false): Path = {
+ if (!permissive) check_directory(dir)
Isabelle_System.make_directory(dir + PATH)
dir
}
@@ -285,7 +285,7 @@
/* maintain presentation structure */
def update_chapter(session_name: String, session_description: String): Unit = synchronized {
- val dir = Meta_Info.init_directory(chapter_dir(session_name))
+ val dir = Meta_Info.init_directory(chapter_dir(session_name), permissive = true)
Meta_Info.change(dir, Meta_Info.INDEX) { text =>
val index0 = Meta_Info.Index.parse(text, "chapter")
val item = Meta_Info.Item(session_name, description = session_description)
@@ -312,7 +312,7 @@
}
def update_root(): Unit = synchronized {
- Meta_Info.init_directory(root_dir)
+ Meta_Info.init_directory(root_dir, permissive = true)
HTML.init_fonts(root_dir)
Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle.gif"),
root_dir + Path.explode("isabelle.gif"))
--- a/src/Pure/System/other_isabelle.scala Fri Jan 31 17:01:27 2025 +0100
+++ b/src/Pure/System/other_isabelle.scala Fri Jan 31 17:01:52 2025 +0100
@@ -187,6 +187,7 @@
def cleanup(): Unit = {
clean_settings()
+ ssh.delete(expand_path(Host.private_data.database))
ssh.delete(etc, isabelle_home_user)
}
}
--- a/src/Tools/Find_Facts/Tools/find_facts_index Fri Jan 31 17:01:27 2025 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-#!/usr/bin/env bash
-#
-# DESCRIPTION: index sessions for Find_Facts
-
-isabelle scala_build || exit $?
-
-eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)"
-
-classpath "$SOLR_JARS"
-
-exec isabelle java "${JAVA_ARGS[@]}" --enable-native-access=ALL-UNNAMED isabelle.find_facts.Find_Facts_Index_Tool "$@"
--- a/src/Tools/Find_Facts/Tools/find_facts_server Fri Jan 31 17:01:27 2025 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-#!/usr/bin/env bash
-#
-# DESCRIPTION: run server for Find_Facts
-
-isabelle scala_build || exit $?
-
-eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)"
-
-classpath "$SOLR_JARS"
-
-exec isabelle java "${JAVA_ARGS[@]}" --enable-native-access=ALL-UNNAMED isabelle.find_facts.Find_Facts_Server_Tool "$@"
--- a/src/Tools/Find_Facts/etc/settings Fri Jan 31 17:01:27 2025 +0100
+++ b/src/Tools/Find_Facts/etc/settings Fri Jan 31 17:01:52 2025 +0100
@@ -2,6 +2,11 @@
FIND_FACTS_HOME="$COMPONENT"
FIND_FACTS_HOME_USER="$ISABELLE_HOME_USER/find_facts"
-FIND_FACTS_INDEXES=""
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$FIND_FACTS_HOME/Tools"
+if [ -d "$FIND_FACTS_HOME/lib/find_facts-isabelle" ]; then
+ FIND_FACTS_INDEXES="$FIND_FACTS_HOME/lib/find_facts-isabelle"
+else
+ FIND_FACTS_INDEXES=""
+fi
+
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$FIND_FACTS_HOME/lib/Tools"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Find_Facts/lib/Tools/find_facts_index Fri Jan 31 17:01:52 2025 +0100
@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+#
+# DESCRIPTION: index sessions for Find_Facts
+
+isabelle scala_build || exit $?
+
+eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)"
+
+classpath "$SOLR_JARS"
+
+exec isabelle java "${JAVA_ARGS[@]}" --enable-native-access=ALL-UNNAMED isabelle.find_facts.Find_Facts_Index_Tool "$@"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Find_Facts/lib/Tools/find_facts_server Fri Jan 31 17:01:52 2025 +0100
@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+#
+# DESCRIPTION: run server for Find_Facts
+
+isabelle scala_build || exit $?
+
+eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)"
+
+classpath "$SOLR_JARS"
+
+exec isabelle java "${JAVA_ARGS[@]}" --enable-native-access=ALL-UNNAMED isabelle.find_facts.Find_Facts_Server_Tool "$@"
--- a/src/Tools/Find_Facts/src/find_facts.scala Fri Jan 31 17:01:27 2025 +0100
+++ b/src/Tools/Find_Facts/src/find_facts.scala Fri Jan 31 17:01:52 2025 +0100
@@ -748,7 +748,7 @@
Isabelle_System.copy_dir(solr.database_dir(database), component_dir.path)
component_dir.write_settings(
- "FIND_FACTS_INDEXES=\"$FIND_FACTS_INDEXES:$COMPONENT/" + database + "\"")
+ "\nFIND_FACTS_INDEXES=\"$FIND_FACTS_INDEXES:$COMPONENT/" + database + "\"")
}