[isabelle] "usedir -b" on Probability: I have to add a relative path in Borel_Space.thy
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: [isabelle] "usedir -b" on Probability: I have to add a relative path in Borel_Space.thy
- From: James Frank <james.isa at gmx.com>
- Date: Thu, 27 Oct 2011 10:49:32 -0500
- User-agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:6.0.2) Gecko/20110902 Thunderbird/6.0.2
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
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
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
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.
(* From ~~/src/HOL/Library/ROOT.ML *)
(* From ~~/src/HOL/Old_Number_Theory/ROOT.ML *)
(* From ~~/src/HOL/Algebra/ROOT.ML *)
(*** 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
"~~/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 *)
(* From ~~/src/HOL/Matrix/ROOT.ML *)
(* From ~~/src/HOL/Multivariate_Analysis/ROOT.ML *)
(* From ~~/src/HOL/NSA/ROOT.ML *)
(* From ~~/src/HOL/Number_Theory/ROOT.ML *)
(* From ~~/src/HOL/Probability/ROOT.ML *)
(* From ~~/src/HOL/ZF/ROOT.ML *)
This archive was generated by a fusion of
Pipermail (Mailman edition) and