Diffusion Isabelle b221d12978ee

merged
b221d12978ee
Actions

Description

merged

Details

Provenance

paulson

Authored on

Parents

rISABELLEe2a5c4117ff0: tidying a few proofs a bit more
rISABELLE7ecf0ee4ce9f: merged

Branches

Unknown

Tags

Unknown

Event Timeline

paulson committed rISABELLEb221d12978ee: merged.Jul 17 2023, 10:49 PM

Merged Changes

This commit merges a very large number of changes. Only the first 50 are shown.

127e4e952446 update for release;
Author
makarius
Browse Repository
No Builds
No Audits
47d5e8be39a9 back out 9d5e2a08ba1b, hoping the server room stays sufficiently cool;
Author
makarius
Browse Repository
No Builds
No Audits
3fdf3c5cfa9d performance tuning: prefer static simpset within functional closure of morphism…
Author
makarius
Browse Repository
No Builds
No Audits
14ceb9a51e97 clarified statistics;
Author
makarius
Browse Repository
No Builds
No Audits
c32b8d5a9e07 show more build history for AFP;
Author
makarius
Browse Repository
No Builds
No Audits
14219730e04f more statistics;
Author
makarius
Browse Repository
No Builds
No Audits
dfe60f5594bd proper base_thys;
Author
makarius
Browse Repository
No Builds
No Audits
573cc2ab69c5 more thorough context tracing;
Author
makarius
Browse Repository
No Builds
No Audits
43cbd96de418 proper check;
Author
makarius
Browse Repository
No Builds
No Audits
9067d8ac9c47 proper symbolic hostname, as provided via Build_Cluster.Host;
Author
makarius
Browse Repository
No Builds
No Audits
d70dc78c0d4e unused;
Author
makarius
Browse Repository
No Builds
No Audits
3d1746a716fa clarified signature: Build_Cluster.Session.build_context;
Author
makarius
Browse Repository
No Builds
No Audits
a8e1d9202dd9 clarified exception handling and return_code;
Author
makarius
Browse Repository
No Builds
No Audits
c38aebdf1a3d tuned signature: more operations;
Author
makarius
Browse Repository
No Builds
No Audits
3153311f0f6c more robust;
Author
makarius
Browse Repository
No Builds
No Audits
126a12483c67 support for Build_Cluster.Session.init (rsync + Admin/init);
Author
makarius
Browse Repository
No Builds
No Audits
001d423daf7c prefer Process_Result.RC.merge: strict treatment of interrupt;
Author
makarius
Browse Repository
No Builds
No Audits
d79eb2a6de0f clarified signature: more operations;
Author
makarius
Browse Repository
No Builds
No Audits
84471794b280 proper afp_root;
Author
makarius
Browse Repository
No Builds
No Audits
5f5f909206bb clarified signature: more "object-oriented" style;
Author
makarius
Browse Repository
No Builds
No Audits
a623cb346b4a more flexible Build.Engine.process_options: e.g. to manipulate "process_policy"…
Author
makarius
Browse Repository
No Builds
No Audits
b4ec7ea073da clarified signature: delegate policies to Build_Cluster implementation…
Author
makarius
Browse Repository
No Builds
No Audits
872f10c80810 tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
ee5d9ecc6a0a tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
1ab113f4db74 clarified option (see also b66b6cc1eb8c);
Author
makarius
Browse Repository
No Builds
No Audits
0461fc9d43e8 more build_cluster management: open SSH connections in parallel, but…
Author
makarius
Browse Repository
No Builds
No Audits
103a81e60126 tuned signature: more options;
Author
makarius
Browse Repository
No Builds
No Audits
48cbee2a6f2e clarified signature: more operations;
Author
makarius
Browse Repository
No Builds
No Audits
5b7d1cb073db tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
0be7e94fd243 more accurate print vs. parse;
Author
makarius
Browse Repository
No Builds
No Audits
62d7ef1da441 clarified signature;
Author
makarius
Browse Repository
No Builds
No Audits
e5908be41a36 clarified signature (again);
Author
makarius
Browse Repository
No Builds
No Audits
645b54f3244a tuned output;
Author
makarius
Browse Repository
No Builds
No Audits
dcaf6f33d94d tuned output;
Author
makarius
Browse Repository
No Builds
No Audits
fd24f380b588 clarified modules;
Author
makarius
Browse Repository
No Builds
No Audits
c157af5f346e more pro-forma support for afp_root;
Author
makarius
Browse Repository
No Builds
No Audits
dba39392d62e tuned NEWS: emphasize "isabelle build" add-ons;
Author
makarius
Browse Repository
No Builds
No Audits
bc62be4144e6 added option -A for AFP root, following "isabelle sync";
Author
makarius
Browse Repository
No Builds
No Audits
01f61cf796e0 clarified signature: more operations;
Author
makarius
Browse Repository
No Builds
No Audits
f26eba6281b1 tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
a4dee214dfcf clarified file location: to be used by regular Isabelle/Scala tools;
Author
makarius
Browse Repository
No Builds
No Audits
406d34a8a67a update headers;
Author
makarius
Browse Repository
No Builds
No Audits
6f3066a9b609 more pro-forma support for Build_Cluster;
Author
makarius
Browse Repository
No Builds
No Audits
eda362f85cbf tuned;
Author
makarius
Browse Repository
No Builds
No Audits
64e5abd3a3a7 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
c5170293d392 clarified options;
Author
makarius
Browse Repository
No Builds
No Audits
f2d67c78b689 clarified options;
Author
makarius
Browse Repository
No Builds
No Audits
092f1e435b3a proper Build_Cluster.Host.parse for parameters and system options;
Author
makarius
Browse Repository
No Builds
No Audits
b262ecc98319 more operations for independent "inline" options;
Author
makarius
Browse Repository
No Builds
No Audits
2ece6509ad6f clarified options: accommodate potentially slow database connection;
Author
makarius
Browse Repository
No Builds
No Audits

Changes (3)

Path

Size

src/

HOL/

Analysis/

Brouwer_Fixpoint.thy

Fashoda_Theorem.thy

Homotopy.thy

rISABELLEb221d12978ee

View Options

src/HOL/Analysis/Brouwer_Fixpoint.thy

View Options

src/HOL/Analysis/Fashoda_Theorem.thy

View Options

src/HOL/Analysis/Homotopy.thy

mergedb221d12978eeActions

Description

Details

Event Timeline

Merged Changes

Changes (3)

rISABELLEb221d12978ee

src/HOL/Analysis/Brouwer_Fixpoint.thy

src/HOL/Analysis/Fashoda_Theorem.thy

src/HOL/Analysis/Homotopy.thy

merged
b221d12978ee
Actions