--- a/Admin/components/components.sha1 Thu Jan 02 16:59:42 2025 +0100
+++ b/Admin/components/components.sha1 Fri Jan 03 22:35:28 2025 +0100
@@ -101,6 +101,7 @@
a3bebab5df4294dac2dd7fd2065a94df00e0b3ff e-2.6.tar.gz
8744880925dbc95c3977f58b7d6da64a3bd6de6a e-3.0.03-1.tar.gz
230d01c2c7274a17b6410535eb41665b16b41ae6 e-3.0.03.tar.gz
+e4a617aed36c32125aeeee3efea0eeff8c979481 e-3.1-1.tar.gz
4e436e450775bd971b3247c97d4bba7943ae4762 e-3.1.tar.gz
239e7b8bebbfc29a1c5151e8fb261ffad44877f1 easychair-3.5.tar.gz
4a3b4b4e0441c4498a0c71dc348f3538be589a15 eptcs-1.7.0.tar.gz
--- a/Admin/components/main Thu Jan 02 16:59:42 2025 +0100
+++ b/Admin/components/main Fri Jan 03 22:35:28 2025 +0100
@@ -4,7 +4,7 @@
bib2xhtml-20190409
csdp-6.1.1
cvc4-1.8
-e-3.1
+e-3.1-1
easychair-3.5
eptcs-1.7.0
flatlaf-2.6
--- a/NEWS Thu Jan 02 16:59:42 2025 +0100
+++ b/NEWS Fri Jan 03 22:35:28 2025 +0100
@@ -226,6 +226,8 @@
target languages, similar to 'code_printing'.
* Sledgehammer:
+ - Update of bundled provers:
+ . E 3.1 -- with patch on Windows/Cygwin for proper interrupts
- Added instantiations of facts using the "of" attribute
(e.g. "assms(1)[of x]"), which can be activated using the
Sledgehammer option "suggest_of" (default: smart, i.e. only if
--- a/src/Pure/Admin/component_e.scala Thu Jan 02 16:59:42 2025 +0100
+++ b/src/Pure/Admin/component_e.scala Fri Jan 03 22:35:28 2025 +0100
@@ -49,6 +49,13 @@
progress.echo("Building E prover for " + platform_name + " ...")
+ // adhoc patch wrt. https://github.com/eprover/eprover/commit/d40e1db7d786
+ if (Platform.is_windows) {
+ File.change_lines(source_dir + Path.explode("PROVER/eprover.c"), strict = true) {
+ _.map(line => if (line.containsSlice("setpgid(0, 0)")) "" else line)
+ }
+ }
+
val build_options = {
val result = Isabelle_System.bash("./configure --help", cwd = source_dir)
if (result.check.out.containsSlice("--enable-ho")) " --enable-ho" else ""
@@ -86,6 +93,9 @@
File.write(component_dir.README,
"This is E prover " + version + " from\n" + archive_url + """
+* On Windows/Cygwin, the sources have been patched to remove setpgid in
+ PROVER/eprover.c
+
* The distribution has been built like this:
cd src && """ + build_script + """