Email Gateway (Aug 18 2022 at 18:35): Email Gateway (Aug 18 2022 at 18:35):From: James Frank <james.isa@gmx.com>
Hi,
I mentioned this to Makarius when I was building some HOL sessions with
usedir to get the PDFs, after which he pointed out that all the HOL
sessions are built and linked to at the bottom of
http://isabelle.in.tum.de/dist/library/HOL/index.html. There's no real
problem here.
However, I'll make a request here, and give some details below.
It would be nice if "~~/src/HOL/Probability/Borel_Space.thy" had the import
"~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis",
instead of simply "Multivariate_Analysis".
There's no problem for me, it's that if I tell someone to build
Probability using "usedir -b" and its ROOT.ML, then I also have to tell
them to edit Borel_Space.thy, and it seems bad principle to tell someone
to edit a distribution file in the installation folder.
I suppose there's a way to create an IsaMakeFile to specify the
dependencies, but I don't know how to do that yet, it's probably more
complicated, 9 out 10 other sessions I built with "usedir -b" don't
return errors, and there are other files in HOL/Probability that import
files from Multivariate_Analysis using a relative path.
Anyway, here's what led to this request.
I wanted to look at
HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy, which is about
5800 lines. It brought jEdit and i3p to their speedwise knees; both
became unresponsive, and I have an Intel i3 with 8Gbytes of ram.
Being in the infantile stages, I thought about abandoning Isabelle, then
I thought about buying an i7 notebook, and then I built the heap for
Multivariate_Analysis and used it as my logic, which solved my need for
practical speed.
In fact, in jEdit, I can now load two big files from
Multivariate_Analysis, and it'll work on proving both files in its spare
time without becoming unresponsive.
One thing leads to another.
I made a ROOT.ML composed of the ROOT.MLs from Library,
Old_Number_Theory, Algebra, Lattice, Matrix, Multivariate_Analysis, NSA,
Number_Theory, Probability, and ZF.
My ROOT.ML gets one error in the build using the command,
isabelle usedir -b HOL HOL_LibOntAlgLatMatMvNsaNtPrbZf.
To get it to build, I have to edit Borel_Space.thy as explained above.
Below, I've included the contents of my ROOT.ML.
Thanks,
James
(* From ~~/src/HOL/Library/ROOT.ML *)
use_thys [
"~~/src/HOL/Library/Library",
"~~/src/HOL/Library/List_Cset",
"~~/src/HOL/Library/List_Prefix",
"~~/src/HOL/Library/List_lexord",
"~~/src/HOL/Library/Sublist_Order",
"~~/src/HOL/Library/Product_Lattice",
"~~/src/HOL/Library/Code_Char_chr",
"~~/src/HOL/Library/Code_Char_ord",
"~~/src/HOL/Library/Code_Integer",
"~~/src/HOL/Library/Efficient_Nat",
"~~/src/HOL/Library/Executable_Set"(, "Code_Prolog")
];
(* From ~~/src/HOL/Old_Number_Theory/ROOT.ML *)
use_thys [
"~~/src/HOL/Old_Number_Theory/Fib",
"~~/src/HOL/Old_Number_Theory/Factorization",
"~~/src/HOL/Old_Number_Theory/Chinese",
"~~/src/HOL/Old_Number_Theory/WilsonRuss",
"~~/src/HOL/Old_Number_Theory/WilsonBij",
"~~/src/HOL/Old_Number_Theory/Quadratic_Reciprocity",
"~~/src/HOL/Old_Number_Theory/Primes",
"~~/src/HOL/Old_Number_Theory/Pocklington"
];
(* From ~~/src/HOL/Algebra/ROOT.ML *)
use_thys [
(* New development, based on explicit structures *)
(* Groups *)
"~~/src/HOL/Algebra/FiniteProduct", (* Product operator for
commutative groups *)
"~~/src/HOL/Algebra/Sylow", (* Sylow's theorem *)
"~~/src/HOL/Algebra/Bij", (* Automorphism Groups *)
(* Rings *)
"~~/src/HOL/Algebra/Divisibility", (* Rings *)
"~~/src/HOL/Algebra/IntRing", (* Ideals and residue
classes *)
"~~/src/HOL/Algebra/UnivPoly", (* Polynomials *)
(* Old development, based on axiomatic type classes *)
"~~/src/HOL/Algebra/abstract/Abstract", (The ring theory)
"~~/src/HOL/Algebra/poly/Polynomial" (The full theory)
];
(* From ~~/src/HOL/Lattice/ROOT.ML *)
use_thys [
"~~/src/HOL/Lattice/CompleteLattice"
];
(* From ~~/src/HOL/Matrix/ROOT.ML *)
use_thys [
"~~/src/HOL/Matrix/Cplex"
];
(* From ~~/src/HOL/Multivariate_Analysis/ROOT.ML *)
use_thys [
"~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis",
"~~/src/HOL/Multivariate_Analysis/Determinants"
];
(* From ~~/src/HOL/NSA/ROOT.ML *)
use_thys [
"~~/src/HOL/NSA/Hypercomplex"
];
(* From ~~/src/HOL/Number_Theory/ROOT.ML *)
use_thys [
"~~/src/HOL/Number_Theory/Number_Theory"
];
(* From ~~/src/HOL/Probability/ROOT.ML *)
use_thys [
"~~/src/HOL/Probability/Probability"
];
(* From ~~/src/HOL/ZF/ROOT.ML *)
use_thys [
"~~/src/HOL/ZF/MainZF",
"~~/src/HOL/ZF/Games"
];
Email Gateway (Aug 18 2022 at 18:36):From: Makarius <makarius@sketis.net>
On Thu, 27 Oct 2011, James Frank wrote:
I thought about buying an i7 notebook, and then I built the heap for
Multivariate_Analysis and used it as my logic, which solved my need for
practical speed.
Pre-built heaps generally improve the memory situation, because all
results are maximally shared in the end. So a heap of several GB will end
up as a few hundred MB that can then be used in interactive sessions.
I made a ROOT.ML composed of the ROOT.MLs from Library,
Old_Number_Theory, Algebra, Lattice, Matrix, Multivariate_Analysis, NSA,
Number_Theory, Probability, and ZF.
Two fine points here:
* A single simulatenous use_thys provides more opportinity for
parallelism in batch mode.
* Some sessions share certain popular theory names, and loading them
together will lead to surprises, due to the flat theory name space.
Makarius
Email Gateway (Aug 18 2022 at 18:36):From: Johannes Hölzl <hoelzl@in.tum.de>
Okay, I changed this. Now it should be possible to build
Multivariate_Analysis and Probability with one ROOT.ML
Email Gateway (Aug 18 2022 at 18:36):From: Makarius <makarius@sketis.net>
Just to perform the canonical running gag: "now" means version
fc3c7db5bb2f in the Isabelle repository, and to benefit from it you need
to wait for the next official release, or switch to alpha/beta testing of
development snapshots. The latter are discussed on isabelle-dev, not
isabelle-users.
Makarius
Email Gateway (Aug 18 2022 at 18:36):From: James Frank <james.isa@gmx.com>
Okay, I changed this. Now it should be possible to build
Multivariate_Analysis and Probability with one ROOT.ML
- Johannes
Thanks.
Two fine points here:
* A single simulatenous use_thys provides more opportinity for
parallelism in batch mode.* Some sessions share certain popular theory names, and loading them
together will lead to surprises, due to the flat theory name space.Makarius
Thanks for the tips.
Just to perform the canonical running gag: "now" means version
fc3c7db5bb2f in the Isabelle repository, and to benefit from it you
need to wait for the next official release, or switch to alpha/beta
testing of development snapshots. The latter are discussed on
isabelle-dev, not isabelle-users.Makarius
That's why I ask now, to try to get it in the next release.
I looked at the repository a few weeks back, and again now. I can't figure it out, and there's not much motivation; I don't want to try and build any sources for Cygwin, plus everything is working good anyway.
I'm on the dev mailing list. I saw the recent exchange on the "non-terminating function".
The law of the excluded middle, you gotta have it, and Isabelle has it, so I keep hanging around. If you can't know something's true, at least you can know sometimes that it's not true. Who wants to spend their life trying to prove something true when it's not true? And, I suppose, false, when it's not false. It's nice to know when it's useless to try and work out the details, because there are no details that can ever be worked out.
--James
Last updated: Apr 18 2024 at 01:05 UTC