[isabelle-dev] Directory layout
The switch to hg makes it possible to adapt some file locations (file names) in the Isabelle distribution which have evolved over time but do not fit to the logical structure of the distribution any longer, according to the following table: src/Provers/* ~ src/Tools/* src/Pure/Tools/* ~ src/Tools/* src/HOL/arith_data.ML ~ src/HOL/Tools src/HOL/hologic.ML ~ src/HOL/Tools src/HOL/simpdata.ML ~ src/HOL/Tools src/HOL/int_arith1.ML ~ src/HOL/Tools/int_arith.ML src/HOL/int_factor_simprocs.ML ~ src/HOL/Tools src/HOL/nat_simprocs.ML ~ src/HOL/Tools src/HOL/Real/float_syntax.ML ~ src/HOL/Tools src/HOL/Real/rat_arith.ML ~ src/HOL/Tools src/HOL/Real/real_arith.ML ~ src/HOL/Tools src/HOL/Library/RType.thy ~ src/HOL/Typerep.thy src/HOL/Library/Code_Message.thy ~ src/HOL/ src/HOL/Library/Dense_Linear_Order.thy ~ src/HOL src/HOL/Library/GCD.thy ~ src/HOL src/HOL/Library/Order_Relation.thy ~ src/HOL src/HOL/Library/Parity.thy ~ src/HOL src/HOL/Library/Univ_Poly.thy ~ src/HOL src/HOL/Real/ContNotDenum.thy ~ src/HOL src/HOL/Real/Lubs.thy ~ src/HOL src/HOL/Real/PReal.thy ~ src/HOL src/HOL/Real/Rational.thy ~ src/HOL src/HOL/Real/RComplete.thy ~ src/HOL src/HOL/Real/RealDef.thy ~ src/HOL src/HOL/Real/RealPow.thy ~ src/HOL src/HOL/Real/Real.thy ~ src/HOL src/HOL/Real/RealVector.thy ~ src/HOL src/HOL/Complex/Complex_Main.thy ~ src/HOL src/HOL/Complex/Complex.thy ~ src/HOL src/HOL/Complex/Fundamental_Theorem_Algebra.thy ~ src/HOL src/HOL/Hyperreal/Deriv.thy ~ src/HOL src/HOL/Hyperreal/Fact.thy ~ src/HOL src/HOL/Hyperreal/Integration.thy ~ src/HOL src/HOL/Hyperreal/Lim.thy ~ src/HOL src/HOL/Hyperreal/Ln.thy ~ src/HOL src/HOL/Hyperreal/Log.thy ~ src/HOL src/HOL/Hyperreal/MacLaurin.thy ~ src/HOL src/HOL/Hyperreal/NthRoot.thy ~ src/HOL src/HOL/Hyperreal/SEQ.thy ~ src/HOL src/HOL/Hyperreal/Series.thy ~ src/HOL src/HOL/Hyperreal/Taylor.thy ~ src/HOL src/HOL/Hyperreal/Transcendental.thy ~ src/HOL src/HOL/Complex/ex/BigO_Complex.thy ~ src/HOL/ex src/HOL/Complex/ex/BinEx.thy ~ src/HOL/ex src/HOL/Complex/ex/Sqrt.thy ~ src/HOL/ex src/HOL/Complex/ex/Sqrt_Script.thy ~ src/HOL/ex src/HOL/Complex/ex/MIR.thy ~ src/HOL/ex src/HOL/Complex/ex/mirtac.ML ~ src/HOL/ex src/HOL/Complex/ex/ReflectedFerrack.thy ~ src/HOL/ex src/HOL/Complex/ex/linrtac.ML ~ src/HOL/ex If there are no objections, I would carry out these movements this Wednesday. A further step will consider HOL/Library and HOL/ex; the ideas are to split off larger library blocks into separate directories, move re-usable examples from HOL/ex to HOL/Library and split off pure test examples (e.g. code generator coverage test) from HOL/ex into a separate session. Florian -- Home: http://wwwbroy.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de -- next part -- A non-text attachment was scrubbed... Name: signature.asc Type: application/pgp-signature Size: 252 bytes Desc: OpenPGP digital signature URL: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20081201/fef5ca18/attachment.pgp
[isabelle-dev] Directory layout
On Mon, 1 Dec 2008, Florian Haftmann wrote:
The switch to hg makes it possible to adapt some file locations (file
names) in the Isabelle distribution which have evolved over time but do
not fit to the logical structure of the distribution any longer,
according to the following table:
src/Provers/* ~ src/Tools/*
src/Pure/Tools/* ~ src/Tools/*
src/HOL/arith_data.ML ~ src/HOL/Tools
src/HOL/hologic.ML ~ src/HOL/Tools
src/HOL/simpdata.ML ~ src/HOL/Tools
I cannot really say much about HOL, you know better about its logical
structure.
Concerning src/Provers, src/Tools, src/Pure/Tools:
* The distinction of src/Provers and src/Tools is mostly nostalgic, so
Provers should go into Tools. For quite some time, we have already
followed the convention of putting new things in src/Tools.
* The role of src/Pure/Tools is still unclear. The difference is that
these are actually loaded into the Pure image, and all its
contributing sources should be in src/Pure. I would say we leave
src/Pure/Tools unchanged for now until we get a better idea.
BTW, moving files will also affect manuals. In the newer ones (isar-ref,
system, implementation) I have already used the @{file} document
antiquotation to get a statically checked references to the Isabelle file
space.
Makarius
[isabelle-dev] Isabelle on Mercurial
A few more tips on getting started in a safe way, and avoiding surprises: * Use hg outgoing to see beforehand what hg push would do; the same works for hg incoming and hg pull. There is a real danger of messing up our central push area by merging it with my earlier attempt of the CVS - hg conversion, which I had to discontinue some months ago. If you still happen to have a clone around on your machine, delete it now! * An easy way to protect against gross mistakes is to install the following hook in your ~/.hgrc on the home directory at TUM: [hooks] pretxnchangegroup = /home/isabelle-repository/repos/sanity-check The sanity check prevents pushes that are unusually big, or consist of a large number of changesets -- as in the above case of merging with the bogus version of the old Isabelle repository. This hook is installed in /home/isabelle-repository/repos/.hg/hgrc already, but the Mercurial security model prevents its execution if you are not wenzelm. This is what the warning Not trusting file ... refers to. Makarius
