[isabelle] "usedir -b" on Probability: I have to add a relative path in Borel_Space.thy



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"
];









This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.