[isabelle-dev] Smallest contribution ever (trace_mul_sym generalization)
makarius at sketis.net
Thu Jun 27 11:28:29 CEST 2013
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
In principle the quick start notes here
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.
More information about the isabelle-dev