merged
a999bb19ed1e
Actions

Description

merged

Details

Provenance

Authored on

Parents

rISABELLEdccfe13878a5: update for release;
rISABELLE25f16c356dae: avoid using FOOL syntax with older Vampire versions because of soundness bug…

Branches

Unknown

Tags

Unknown

Event Timeline

makarius committed rISABELLEa999bb19ed1e: merged.Sun, Aug 27, 7:14 PM

Merged Changes

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

dccfe13878a5 update for release;
Author
makarius
Browse Repository
No Builds
No Audits
d0053e582dd9 Added tag Isabelle2023-RC4 for changeset 12aac1489f3b
Author
makarius
Browse Repository
No Builds
No Audits
12aac1489f3b minimal documentation for build cluster support;
Author
makarius
Browse Repository
No Builds
No Audits
e92bbd5fd66f more robust access to local variables;
Author
makarius
Browse Repository
No Builds
No Audits
cf114894a5ed tuned messages: avoid duplicates;
Author
makarius
Browse Repository
No Builds
No Audits
92ef737f412c removed junk (following ab07d4cb7d1c, amending 8cd399b25dac);
Author
makarius
Browse Repository
No Builds
No Audits
8f11794211ef tuned error;
Author
makarius
Browse Repository
No Builds
No Audits
63f06b935a1f tuned messages (again);
Author
makarius
Browse Repository
No Builds
No Audits
1384593459b4 tuned: prefer explicit types;
Author
makarius
Browse Repository
No Builds
No Audits
c3a3db450c80 support for Host.dirs;
Author
makarius
Browse Repository
No Builds
No Audits
2dad5335cc57 tuned message: failure can happen towards the end, e.g. due to failed sessions…
Author
makarius
Browse Repository
No Builds
No Audits
5ccf921a2c3d support multiple host names;
Author
makarius
Browse Repository
No Builds
No Audits
a945b541efff clarified default options: SQLite build_database is unsupported for…
Author
makarius
Browse Repository
No Builds
No Audits
2baa77e37406 avoid using FOOL syntax with older Vampire versions because of soundness bug…
Author
blanchette
Browse Repository
No Builds
No Audits
ff86f10e54cd tuned message;
Author
makarius
Browse Repository
No Builds
No Audits
06e045375487 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
980f3cfcbc2c more accurate treatment of state vs. serial vs. db;
Author
makarius
Browse Repository
No Builds
No Audits
11cf77478d3e more explicit check;
Author
makarius
Browse Repository
No Builds
No Audits
ed07f0ebf31c proper numa_nodes for build_worker;
Author
makarius
Browse Repository
No Builds
No Audits
25c04910dcfa tuned message;
Author
makarius
Browse Repository
No Builds
No Audits
50675688c4df tuned;
Author
makarius
Browse Repository
No Builds
No Audits
a97d2b6b5c3e tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
db99a70f8531 support hosts with shared directory (e.g. NFS);
Author
makarius
Browse Repository
No Builds
No Audits
a04277e3b313 tuned message: failure may stem from build_cluster init;
Author
makarius
Browse Repository
No Builds
No Audits
05de3e068312 proper sync_database for receive timeout;
Author
makarius
Browse Repository
No Builds
No Audits
8ba186dc9bc8 clarified source structure;
Author
makarius
Browse Repository
No Builds
No Audits
1789ecbaf28b tuned whitespace;
Author
makarius
Browse Repository
No Builds
No Audits
53e3fa5e3720 clarified command-line tools;
Author
makarius
Browse Repository
No Builds
No Audits
c06a0396b09d tuned output;
Author
makarius
Browse Repository
No Builds
No Audits
39f6f180008d clarified signature;
Author
makarius
Browse Repository
No Builds
No Audits
020fecb4da0c tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
ca0fe2802123 tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
131e2a220c78 proper sequential evaluation;
Author
makarius
Browse Repository
No Builds
No Audits
20360824863a more robust command options;
Author
makarius
Browse Repository
No Builds
No Audits
754bfc558d21 performance tuning: avoid redundant db access;
Author
makarius
Browse Repository
No Builds
No Audits
54991440905e clarified signature: proper treatment of implicit state (amending d0c9d277620e);
Author
makarius
Browse Repository
No Builds
No Audits
66fc98b4557b performance tuning: avoid redundant db access;
Author
makarius
Browse Repository
No Builds
No Audits
384adc74e27d performance tuning: avoid multiple db roundtrips;
Author
makarius
Browse Repository
No Builds
No Audits
d0c9d277620e clarified signature: more robust treatment of implicit state;
Author
makarius
Browse Repository
No Builds
No Audits
d8cc0f625b52 proper sync_database for Database_Progress consumer;
Author
makarius
Browse Repository
No Builds
No Audits
1c5cbece77d2 tuned message;
Author
makarius
Browse Repository
No Builds
No Audits
6cdf9b00dc76 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
7f564f33172b tuned messages;
Author
makarius
Browse Repository
No Builds
No Audits
e3ae7293c5df tuned signature: removed unused arguments;
Author
makarius
Browse Repository
No Builds
No Audits
5f4ca329fde4 minor performance tuning: avoid multiple db roundtrips;
Author
makarius
Browse Repository
No Builds
No Audits
3be0437759cf more operations;
Author
makarius
Browse Repository
No Builds
No Audits
cfdb586adbbd tuned;
Author
makarius
Browse Repository
No Builds
No Audits
4ffc1933f5d9 limit size and complexity of bulk transactions;
Author
makarius
Browse Repository
No Builds
No Audits
d95497dcd9bc more scalable write_entries and Export.consumer via db.execute_batch_statement;
Author
makarius
Browse Repository
No Builds
No Audits
a6d079e0575d clarified signature: filter batch;
Author
makarius
Browse Repository
No Builds
No Audits

Changes (35)

Path

Size

src/

HOL/

Algebra/

Ring.thy

Analysis/

Abstract_Topological_Spaces.thy

Affine.thy

Borel_Space.thy

Complex_Analysis_Basics.thy

Convex_Euclidean_Space.thy

Elementary_Topology.thy

Equivalence_Lebesgue_Henstock_Integration.thy

Finite_Product_Measure.thy

Further_Topology.thy

Homotopy.thy

Path_Connected.thy

Complex_Analysis/

Cauchy_Integral_Formula.thy

Cauchy_Integral_Theorem.thy

Complex_Singularities.thy

Conformal_Mappings.thy

Contour_Integration.thy

Laurent_Convergence.thy

Number_Theory/

Probability/

Infinite_Product_Measure.thy

Information.thy

Levy.thy

SPMF.thy

Topological_Spaces.thy

Pure/

Admin/

isabelle_cronjob.scala

rISABELLEa999bb19ed1e

View Options

Admin/components/components.sha1

View Options

Admin/components/go

View Options

CONTRIBUTORS

View Options

NEWS

View Options

src/HOL/Algebra/Ring.thy

View Options

src/HOL/Analysis/Abstract_Topological_Spaces.thy

View Options

src/HOL/Analysis/Affine.thy

View Options

src/HOL/Analysis/Borel_Space.thy

View Options

src/HOL/Analysis/Complex_Analysis_Basics.thy

View Options

src/HOL/Analysis/Convex_Euclidean_Space.thy

View Options

src/HOL/Analysis/Elementary_Topology.thy

View Options

src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy

View Options

src/HOL/Analysis/Finite_Product_Measure.thy

View Options

src/HOL/Analysis/Further_Topology.thy

View Options

src/HOL/Analysis/Homotopy.thy

View Options

src/HOL/Analysis/Path_Connected.thy

View Options

src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy

View Options

src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy

View Options

src/HOL/Complex_Analysis/Complex_Singularities.thy

View Options

src/HOL/Complex_Analysis/Conformal_Mappings.thy

View Options

src/HOL/Complex_Analysis/Contour_Integration.thy

View Options

src/HOL/Complex_Analysis/Laurent_Convergence.thy

View Options

src/HOL/Complex_Analysis/Residue_Theorem.thy

View Options

src/HOL/Complex_Analysis/Riemann_Mapping.thy

View Options

src/HOL/Number_Theory/Eratosthenes.thy

View Options

src/HOL/Number_Theory/Residues.thy

View Options

src/HOL/Probability/Giry_Monad.thy

View Options

src/HOL/Probability/Infinite_Product_Measure.thy

View Options

src/HOL/Probability/Information.thy

View Options

src/HOL/Probability/Levy.thy

View Options

src/HOL/Probability/SPMF.thy

View Options

src/HOL/Topological_Spaces.thy

View Options

src/Pure/Admin/isabelle_cronjob.scala

mergeda999bb19ed1eActions

Description

Details

Event Timeline

Merged Changes

Changes (35)

rISABELLEa999bb19ed1e

Admin/components/components.sha1

Admin/components/go

CONTRIBUTORS

NEWS

src/HOL/Algebra/Ring.thy

src/HOL/Analysis/Abstract_Topological_Spaces.thy

src/HOL/Analysis/Affine.thy

src/HOL/Analysis/Borel_Space.thy

src/HOL/Analysis/Complex_Analysis_Basics.thy

src/HOL/Analysis/Convex_Euclidean_Space.thy

src/HOL/Analysis/Elementary_Topology.thy

src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy

src/HOL/Analysis/Finite_Product_Measure.thy

src/HOL/Analysis/Further_Topology.thy

src/HOL/Analysis/Homotopy.thy

src/HOL/Analysis/Path_Connected.thy

src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy

src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy

src/HOL/Complex_Analysis/Complex_Singularities.thy

src/HOL/Complex_Analysis/Conformal_Mappings.thy

src/HOL/Complex_Analysis/Contour_Integration.thy

src/HOL/Complex_Analysis/Laurent_Convergence.thy

src/HOL/Complex_Analysis/Residue_Theorem.thy

src/HOL/Complex_Analysis/Riemann_Mapping.thy

src/HOL/Number_Theory/Eratosthenes.thy

src/HOL/Number_Theory/Residues.thy

src/HOL/Probability/Giry_Monad.thy

src/HOL/Probability/Infinite_Product_Measure.thy

src/HOL/Probability/Information.thy

src/HOL/Probability/Levy.thy

src/HOL/Probability/SPMF.thy

src/HOL/Topological_Spaces.thy

src/Pure/Admin/isabelle_cronjob.scala

merged
a999bb19ed1e
Actions