[isabelle-dev] Smallest contribution ever (trace_mul_sym generalization)

[Makarius]

On Tue, 25 Jun 2013, Stephen Nuchia wrote:

> I did not do the full battery of recommended pre-commitment tests 
> because I haven't yet figured out how to switch my Cygwin environment to 
> point at the local mercurial repository but I was able to build the 
> relevant session in the HOL directory with the change replicated there. 
> I'm thinking I should spin up a VM or work under Linux for preparing 
> changesets and keep my real work on the official release on my primary 
> workstation.

In principle the quick start notes here 
http://isabelle.in.tum.de/repos/isabelle/file/92ae850a9bfd/README_REPOSITORY#l4
should also work for Windows with Cygwin.

There might be a challange getting the Cygwin installation right, also due 
to the "sliding updates" of that project.  What I usually do these days is 
to re-use the bundled Cygwin from the latest official Isabelle release, 
and augment that by additional packages as required for experimental work.

I think the regular build should work with the default packages, although 
there is a single latex breakdown build the "prog-prove" manual, which you 
normally don't need for testing.


> The documentation for this change now outweighs the change itself by 
> three orders of magnitude :-)

In this particular case it is indeed all below the lowest measureable 
energy level.  Changes outside main HOL or HOL-Library don't affect so 
many other things.


 	Makarius