--- a/Admin/PLATFORMS Fri Apr 23 09:50:14 2021 +0000
+++ b/Admin/PLATFORMS Sun Apr 25 22:33:53 2021 +0200
@@ -33,7 +33,7 @@
Official (full support):
- x86_64-linux Ubuntu 14.04 LTS
+ x86_64-linux Ubuntu 16.04 LTS
x86_64-darwin macOS 10.13 High Sierra (lapbroy68 MacBookPro11,2)
macOS 10.14 Mojave (mini2 Macmini8,1)
--- a/Admin/bash_process/bash_process.c Fri Apr 23 09:50:14 2021 +0000
+++ b/Admin/bash_process/bash_process.c Sun Apr 25 22:33:53 2021 +0200
@@ -37,13 +37,12 @@
{
/* args */
- if (argc < 3) {
- fprintf(stderr, "Bad arguments: PID_FILE and TIMING_FILE required\n");
+ if (argc < 2) {
+ fprintf(stderr, "Bad arguments: missing TIMING_FILE\n");
fflush(stderr);
exit(1);
}
- char *pid_name = argv[1];
- char *timing_name = argv[2];
+ char *timing_name = argv[1];
/* potential fork */
@@ -101,26 +100,16 @@
/* report pid */
- if (strcmp(pid_name, "-") == 0) {
- fprintf(stdout, "%d\n", getpid());
- fflush(stdout);
- }
- else if (strlen(pid_name) > 0) {
- FILE *pid_file;
- pid_file = fopen(pid_name, "w");
- if (pid_file == NULL) fail("Cannot open pid file");
- fprintf(pid_file, "%d", getpid());
- fclose(pid_file);
- }
+ fprintf(stdout, "%d\n", getpid());
+ fflush(stdout);
/* shift command line */
int i;
- for (i = 3; i < argc; i++) {
- argv[i - 3] = argv[i];
+ for (i = 2; i < argc; i++) {
+ argv[i - 2] = argv[i];
}
- argv[argc - 3] = NULL;
argv[argc - 2] = NULL;
argv[argc - 1] = NULL;
--- a/Admin/bash_process/build Fri Apr 23 09:50:14 2021 +0000
+++ b/Admin/bash_process/build Sun Apr 25 22:33:53 2021 +0200
@@ -36,16 +36,16 @@
mkdir -p "$TARGET"
case "$TARGET" in
+ arm64-linux)
+ cc -Wall bash_process.c -o "$TARGET/bash_process"
+ ;;
x86_64-linux | x86_64-darwin)
cc -Wall -m64 bash_process.c -o "$TARGET/bash_process"
;;
- x86-linux | x86-darwin)
- cc -Wall -m32 bash_process.c -o "$TARGET/bash_process"
- ;;
- x86_64-cygwin | x86-cygwin)
+ x86_64-cygwin)
cc -Wall bash_process.c -o "$TARGET/bash_process.exe"
;;
*)
- cc -Wall bash_process.c -o "$TARGET/bash_process"
+ fail "Bad target platform: \"$TARGET\""
;;
esac
--- a/Admin/bash_process/etc/settings Fri Apr 23 09:50:14 2021 +0000
+++ b/Admin/bash_process/etc/settings Sun Apr 25 22:33:53 2021 +0200
@@ -1,3 +1,3 @@
# -*- shell-script -*- :mode=shellscript:
-ISABELLE_BASH_PROCESS="$COMPONENT/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}/bash_process"
+ISABELLE_BASH_PROCESS="$COMPONENT/$ISABELLE_PLATFORM64/bash_process"
--- a/Admin/components/components.sha1 Fri Apr 23 09:50:14 2021 +0000
+++ b/Admin/components/components.sha1 Sun Apr 25 22:33:53 2021 +0200
@@ -13,6 +13,8 @@
97b2491382130a841b3bbaebdcf8720c4d4fb227 bash_process-1.2.2.tar.gz
5c5b7c18cc1dc2a4d22b997dac196da09eaca868 bash_process-1.2.3-1.tar.gz
48b01bd9436e243ffcb7297f08b498d0c0875ed9 bash_process-1.2.3.tar.gz
+11815d5f3af0de9022e903ed8702c136591f06fe bash_process-1.2.4-1.tar.gz
+7ae9ec8aab2d8a811842d9dc67d8bf6c179e11ee bash_process-1.2.4.tar.gz
9e21f447bfa0431ae5097301d553dd6df3c58218 bash_process-1.2.tar.gz
a65ce644b6094d41e9f991ef851cf05eff5dd0a9 bib2xhtml-20171221.tar.gz
4085dd6060a32d7e0d2e3f874c463a9964fd409b bib2xhtml-20190409.tar.gz
--- a/Admin/components/main Fri Apr 23 09:50:14 2021 +0000
+++ b/Admin/components/main Sun Apr 25 22:33:53 2021 +0200
@@ -1,6 +1,6 @@
#main components for everyday use, without big impact on overall build time
gnu-utils-20210414
-bash_process-1.2.3-1
+bash_process-1.2.4-1
bib2xhtml-20190409
csdp-6.1.1
cvc4-1.8
--- a/NEWS Fri Apr 23 09:50:14 2021 +0000
+++ b/NEWS Sun Apr 25 22:33:53 2021 +0200
@@ -33,6 +33,10 @@
\guilsinglright. INCOMPATIBILITY, need to use \usepackage[T1]{fontenc}
(which is now also the default in "isabelle mkroot").
+* Simplified typesetting of \<guillemotleft>...\<guillemotright> using \guillemotleft ...
+\guillemotright from \usepackage[T1]{fontenc} --- \usepackage{babel} is
+no longer required.
+
*** HOL ***
--- a/lib/Tools/env Fri Apr 23 09:50:14 2021 +0000
+++ b/lib/Tools/env Sun Apr 25 22:33:53 2021 +0200
@@ -25,4 +25,4 @@
[ "$1" = "-?" ] && usage
-exec /usr/bin/env "$@"
+/usr/bin/env "$@"
--- a/lib/texinputs/isabellesym.sty Fri Apr 23 09:50:14 2021 +0000
+++ b/lib/texinputs/isabellesym.sty Sun Apr 25 22:33:53 2021 +0200
@@ -234,8 +234,8 @@
\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.3mu\rbrace}}}
\newcommand{\isasymlblot}{\isamath{{\langle}\mkern -3.5mu{|}}}
\newcommand{\isasymrblot}{\isamath{{|}\mkern -3.5mu{\rangle}}}
-\newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel
-\newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel
+\newcommand{\isasymguillemotleft}{\isatext{\guillemotleft}}
+\newcommand{\isasymguillemotright}{\isatext{\guillemotright}}
\newcommand{\isasymbottom}{\isamath{\bot}}
\newcommand{\isasymtop}{\isamath{\top}}
\newcommand{\isasymand}{\isamath{\wedge}}
--- a/src/Doc/Nitpick/document/root.tex Fri Apr 23 09:50:14 2021 +0000
+++ b/src/Doc/Nitpick/document/root.tex Sun Apr 25 22:33:53 2021 +0200
@@ -2,7 +2,6 @@
\usepackage[T1]{fontenc}
\usepackage{amsmath}
\usepackage{amssymb}
-\usepackage[english]{babel}
\usepackage{color}
\usepackage{footmisc}
\usepackage{graphicx}
@@ -32,7 +31,7 @@
\def\undef{(\lambda x.\; \_)}
%\def\unr{\textit{others}}
\def\unr{\ldots}
-\def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
+\def\Abs#1{\hbox{\rm{\guillemetleft}}{\,#1\,}\hbox{\rm{\guillemetright}}}
\def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
\hyphenation{Mini-Sat size-change First-Steps grand-parent nit-pick
--- a/src/Doc/Sledgehammer/document/root.tex Fri Apr 23 09:50:14 2021 +0000
+++ b/src/Doc/Sledgehammer/document/root.tex Sun Apr 25 22:33:53 2021 +0200
@@ -2,7 +2,6 @@
\usepackage[T1]{fontenc}
\usepackage{amsmath}
\usepackage{amssymb}
-\usepackage[english]{babel}
\usepackage{color}
\usepackage{footmisc}
\usepackage{graphicx}
@@ -40,7 +39,7 @@
\def\undef{(\lambda x.\; \unk)}
%\def\unr{\textit{others}}
\def\unr{\ldots}
-\def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
+\def\Abs#1{\hbox{\rm{\guillemetleft}}{\,#1\,}\hbox{\rm{\guillemetright}}}
\def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
\urlstyle{tt}
--- a/src/Doc/Tutorial/document/root.tex Fri Apr 23 09:50:14 2021 +0000
+++ b/src/Doc/Tutorial/document/root.tex Sun Apr 25 22:33:53 2021 +0200
@@ -3,7 +3,6 @@
\usepackage{proof,amsmath,amsfonts,amssymb}
\usepackage{wasysym,verbatim,graphicx,tutorial,ttbox,comment}
\usepackage{eurosym}
-\usepackage[english]{babel}
\usepackage{pdfsetup}
%last package!
--- a/src/HOL/Bali/document/root.tex Fri Apr 23 09:50:14 2021 +0000
+++ b/src/HOL/Bali/document/root.tex Sun Apr 25 22:33:53 2021 +0200
@@ -4,7 +4,6 @@
\usepackage{latexsym}
\usepackage{graphicx}
\usepackage{pdfsetup}
-\usepackage[english]{babel}
\usepackage{ifthen}
\urlstyle{rm}
--- a/src/HOL/Hoare/document/root.tex Fri Apr 23 09:50:14 2021 +0000
+++ b/src/HOL/Hoare/document/root.tex Sun Apr 25 22:33:53 2021 +0200
@@ -1,7 +1,7 @@
\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
+\usepackage[T1]{fontenc}
\usepackage{graphicx}
-\usepackage[english]{babel}
\usepackage{isabelle,isabellesym}
\usepackage{pdfsetup}
--- a/src/HOL/Hoare_Parallel/document/root.tex Fri Apr 23 09:50:14 2021 +0000
+++ b/src/HOL/Hoare_Parallel/document/root.tex Sun Apr 25 22:33:53 2021 +0200
@@ -1,6 +1,6 @@
\documentclass[11pt,a4paper]{report}
+\usepackage[T1]{fontenc}
\usepackage{graphicx}
-\usepackage[english]{babel}
\usepackage{isabelle,isabellesym}
\usepackage{pdfsetup}
--- a/src/HOL/Imperative_HOL/document/root.tex Fri Apr 23 09:50:14 2021 +0000
+++ b/src/HOL/Imperative_HOL/document/root.tex Sun Apr 25 22:33:53 2021 +0200
@@ -1,7 +1,6 @@
\documentclass[11pt,a4paper]{article}
\usepackage{graphicx,isabelle,isabellesym,latexsym}
\usepackage{amssymb}
-\usepackage[english]{babel}
\usepackage[only,bigsqcap]{stmaryrd}
\usepackage{pdfsetup}
\usepackage{ifthen}
--- a/src/HOL/Library/document/root.tex Fri Apr 23 09:50:14 2021 +0000
+++ b/src/HOL/Library/document/root.tex Sun Apr 25 22:33:53 2021 +0200
@@ -1,7 +1,6 @@
\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{ifthen}
-\usepackage[english]{babel}
\usepackage{amsmath,amssymb,stmaryrd,textcomp,wasysym}
\usepackage{isabelle,isabellesym}
\usepackage{pdfsetup}
--- a/src/HOL/Probability/document/root.tex Fri Apr 23 09:50:14 2021 +0000
+++ b/src/HOL/Probability/document/root.tex Sun Apr 25 22:33:53 2021 +0200
@@ -6,7 +6,6 @@
\usepackage{wasysym}
\usepackage[only,bigsqcap]{stmaryrd}
\usepackage{pdfsetup}
-\usepackage[english]{babel}
\urlstyle{rm}
\isabellestyle{it}
--- a/src/HOL/Proofs/Lambda/document/root.tex Fri Apr 23 09:50:14 2021 +0000
+++ b/src/HOL/Proofs/Lambda/document/root.tex Sun Apr 25 22:33:53 2021 +0200
@@ -1,7 +1,7 @@
\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
+\usepackage[T1]{fontenc}
\usepackage{graphicx}
-\usepackage[english]{babel}
\usepackage{amssymb}
\usepackage{textcomp}
\usepackage{isabelle,isabellesym,pdfsetup}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Apr 23 09:50:14 2021 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Sun Apr 25 22:33:53 2021 +0200
@@ -271,7 +271,7 @@
let val {output, timing} = SystemOnTPTP.run_system_encoded args
in (output, timing) end
else
- let val res = Isabelle_System.bash_process ("exec 2>&1; " ^ command)
+ let val res = Isabelle_System.bash_process_redirect command
in (Process_Result.out res, Process_Result.timing_elapsed res) end
val _ =
--- a/src/HOL/document/root.tex Fri Apr 23 09:50:14 2021 +0000
+++ b/src/HOL/document/root.tex Sun Apr 25 22:33:53 2021 +0200
@@ -4,7 +4,6 @@
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{textcomp}
-\usepackage[english]{babel}
\usepackage[only,bigsqcap]{stmaryrd}
\usepackage{pdfsetup}
--- a/src/Pure/ML/ml_process.scala Fri Apr 23 09:50:14 2021 +0000
+++ b/src/Pure/ML/ml_process.scala Sun Apr 25 22:33:53 2021 +0200
@@ -124,7 +124,7 @@
use_prelude.flatMap(List("--use", _)) ::: List("--eval", eval_process) ::: args
Bash.process(
- "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
+ options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
Bash.strings(bash_args),
cwd = cwd,
env = env ++ env_options ++ env_tmp ++ env_functions,
--- a/src/Pure/ML/ml_statistics.scala Fri Apr 23 09:50:14 2021 +0000
+++ b/src/Pure/ML/ml_statistics.scala Sun Apr 25 22:33:53 2021 +0200
@@ -70,7 +70,7 @@
val env_prefix =
if (stats_dir.isEmpty) "" else "export POLYSTATSDIR=" + Bash.string(stats_dir) + "\n"
- Bash.process(env_prefix + "exec \"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " +
+ Bash.process(env_prefix + "\"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " +
Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " +
ML_Syntax.print_double(delay.seconds)),
cwd = Path.ISABELLE_HOME.file)
--- a/src/Pure/System/bash.scala Fri Apr 23 09:50:14 2021 +0000
+++ b/src/Pure/System/bash.scala Sun Apr 25 22:33:53 2021 +0200
@@ -11,6 +11,7 @@
BufferedWriter, OutputStreamWriter}
import scala.annotation.tailrec
+import scala.jdk.OptionConverters._
object Bash
@@ -65,12 +66,22 @@
private val timing = Synchronized[Option[Timing]](None)
def get_timing: Timing = timing.value getOrElse Timing.zero
- private val script_file = Isabelle_System.tmp_file("bash_script")
- File.write(script_file, script)
+ private val winpid_file: Option[JFile] =
+ if (Platform.is_windows) Some(Isabelle_System.tmp_file("bash_winpid")) else None
+ private val winpid_script =
+ winpid_file match {
+ case None => script
+ case Some(file) =>
+ "read < /proc/self/winpid > /dev/null 2> /dev/null\n" +
+ """echo -n "$REPLY" > """ + File.bash_path(file) + "\n\n" + script
+ }
+
+ private val script_file: JFile = Isabelle_System.tmp_file("bash_script")
+ File.write(script_file, winpid_script)
private val proc =
Isabelle_System.process(
- List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-",
+ List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")),
File.standard_path(timing_file), "bash", File.standard_path(script_file)),
cwd = cwd, env = env, redirect = redirect)
@@ -89,17 +100,30 @@
// signals
- private val pid = stdout.readLine
+ private val group_pid = stdout.readLine
+
+ private def process_alive(pid: String): Boolean =
+ (for {
+ p <- Value.Long.unapply(pid)
+ handle <- ProcessHandle.of(p).toScala
+ } yield handle.isAlive) getOrElse false
- @tailrec private def kill(signal: String, count: Int = 1): Boolean =
+ private def root_process_alive(): Boolean =
+ winpid_file match {
+ case None => process_alive(group_pid)
+ case Some(file) =>
+ file.exists() && process_alive(Library.trim_line(File.read(file)))
+ }
+
+ @tailrec private def signal(s: String, count: Int = 1): Boolean =
{
count <= 0 ||
{
- Isabelle_System.kill(signal, pid)
- val running = Isabelle_System.kill("0", pid)._2 == 0
+ Isabelle_System.process_signal(group_pid, signal = s)
+ val running = root_process_alive() || Isabelle_System.process_signal(group_pid)
if (running) {
Time.seconds(0.1).sleep
- kill(signal, count - 1)
+ signal(s, count - 1)
}
else false
}
@@ -107,14 +131,14 @@
def terminate(): Unit = Isabelle_Thread.try_uninterruptible
{
- kill("INT", count = 7) && kill("TERM", count = 3) && kill("KILL")
+ signal("INT", count = 7) && signal("TERM", count = 3) && signal("KILL")
proc.destroy()
do_cleanup()
}
def interrupt(): Unit = Isabelle_Thread.try_uninterruptible
{
- Isabelle_System.kill("INT", pid)
+ Isabelle_System.process_signal(group_pid, "INT")
}
@@ -133,7 +157,8 @@
try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
catch { case _: IllegalStateException => }
- script_file.delete
+ script_file.delete()
+ winpid_file.foreach(_.delete())
timing.change {
case None =>
@@ -211,7 +236,12 @@
val here = Scala_Project.here
def apply(args: List[String]): List[String] =
{
- val result = Exn.capture { Isabelle_System.bash(cat_lines(args)) }
+ val result =
+ Exn.capture {
+ val redirect = args.head == "true"
+ val script = cat_lines(args.tail)
+ Isabelle_System.bash(script, redirect = redirect)
+ }
val is_interrupt =
result match {
--- a/src/Pure/System/isabelle_system.ML Fri Apr 23 09:50:14 2021 +0000
+++ b/src/Pure/System/isabelle_system.ML Sun Apr 25 22:33:53 2021 +0200
@@ -7,6 +7,7 @@
signature ISABELLE_SYSTEM =
sig
val bash_process: string -> Process_Result.T
+ val bash_process_redirect: string -> Process_Result.T
val bash_output: string -> string * int
val bash: string -> int
val bash_functions: unit -> string list
@@ -34,9 +35,9 @@
(* bash *)
-fun bash_process script =
+fun invoke_bash_process redirect script =
Scala.function "bash_process"
- ["export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP"), script]
+ [Value.print_bool redirect, "export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP"), script]
|> (fn [] => raise Exn.Interrupt
| [err] => error err
| a :: b :: c :: d :: lines =>
@@ -53,6 +54,9 @@
end
| _ => raise Fail "Malformed Isabelle/Scala result");
+val bash_process = invoke_bash_process false;
+val bash_process_redirect = invoke_bash_process true;
+
val bash = bash_process #> Process_Result.print #> Process_Result.rc;
fun bash_output s =
--- a/src/Pure/System/isabelle_system.scala Fri Apr 23 09:50:14 2021 +0000
+++ b/src/Pure/System/isabelle_system.scala Sun Apr 25 22:33:53 2021 +0200
@@ -13,6 +13,7 @@
StandardCopyOption, FileSystemException}
import java.nio.file.attribute.BasicFileAttributes
+import scala.jdk.CollectionConverters._
object Isabelle_System
@@ -465,7 +466,11 @@
redirect: Boolean = false): Process =
{
val proc = new ProcessBuilder
- proc.command(command_line:_*) // fragile on Windows
+
+ // fragile on Windows:
+ // see https://docs.microsoft.com/en-us/cpp/cpp/main-function-command-line-args?view=msvc-160
+ proc.command(command_line.asJava)
+
if (cwd != null) proc.directory(cwd)
if (env != null) {
proc.environment.clear()
@@ -491,12 +496,13 @@
(output, rc)
}
- def kill(signal: String, group_pid: String): (String, Int) =
+ def process_signal(group_pid: String, signal: String = "0"): Boolean =
{
val bash =
if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash.exe")
else List("/usr/bin/env", "bash")
- process_output(process(bash ::: List("-c", "kill -" + signal + " -" + group_pid)))
+ val (_, rc) = process_output(process(bash ::: List("-c", "kill -" + signal + " -" + group_pid)))
+ rc == 0
}
--- a/src/Pure/System/platform.scala Fri Apr 23 09:50:14 2021 +0000
+++ b/src/Pure/System/platform.scala Sun Apr 25 22:33:53 2021 +0200
@@ -14,6 +14,7 @@
val is_linux: Boolean = System.getProperty("os.name", "") == "Linux"
val is_macos: Boolean = System.getProperty("os.name", "") == "Mac OS X"
val is_windows: Boolean = System.getProperty("os.name", "").startsWith("Windows")
+ val is_unix: Boolean = is_linux || is_macos
def family: Family.Value =
if (is_linux) Family.linux
--- a/src/ZF/document/root.tex Fri Apr 23 09:50:14 2021 +0000
+++ b/src/ZF/document/root.tex Sun Apr 25 22:33:53 2021 +0200
@@ -2,7 +2,6 @@
\usepackage[T1]{fontenc}
\usepackage{graphicx,isabelle,isabellesym}
\usepackage{amssymb}
-\usepackage[english]{babel}
% this should be the last package used
\usepackage{pdfsetup}