<html>
<head>
<meta content="text/html; charset=windows-1252"
http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
Hi Florian, I followed the instructions and things seems to be
working fine in my clone of the repo.<br>
<br>
Before I start trying out the change outlined in your email, I'd
like to double-check a few things:<br>
<ul>
<li>In order to modify Orderings and other theories that are part
of Main, I should start Isabelle with the '-l Pure' option and
load/change the files manually, correct?<br>
</li>
<li>Once Main runs fine, I should check/change any files under the
src/HOL tree that may depend on Orderings. Does any file under
the other src/... trees depend on anything under the src/HOL
tree?</li>
<li>Is the successful completion of 'isabelle build -a' the final
criterion for determining that everything has been modified
correctly? I didn't see any separate test suites in the repo.</li>
<li>Should the AFP (which I didn't see in the repo) be
checked/changed as well? Or is it updated only when there is a
release?<br>
</li>
</ul>
Thanks!<br>
<br>
<br>
<br>
<div class="moz-cite-prefix">On 12/22/12 4:01 AM, Alessandro Coglio
wrote:<br>
</div>
<blockquote cite="mid:50D52298.2050209@kestrel.edu" type="cite">Hi
Florian, I'd be happy to contribute, so I'll look into that. I
don't have a lot of spare time, so it may take me a while. The Jan
or Feb release is "safe" :)
<br>
<br>
<br>
<br>
On 12/18/12 12:18 PM, Florian Haftmann wrote:
<br>
<blockquote type="cite">Hi Alessandro,
<br>
<br>
<blockquote type="cite">Is there any plan to make things in the
library more uniform (one way or
<br>
the other)? Is there a preference for new type classes should
be
<br>
developed (purely syntactic or with assumptions)?
<br>
</blockquote>
well, there is no big masterplan. Usually things evolve:
somebody
<br>
thinks about an extended or more fine-grained hierarchy and
thinks how
<br>
to accomplish things without breaking more than necessary.
<br>
<br>
<blockquote type="cite">Personally, I like syntactic classes
because they are more modular. For
<br>
example, in the library extensions that I sent the other day,
the
<br>
definition of type class finite_lattice_complete would be
perhaps
<br>
slightly cleaner if bot and top were syntactic classes like
Inf and Sup.
<br>
Just my 2 cents.
<br>
</blockquote>
I.e. something like
<br>
<br>
class bot ~> class order_bot
<br>
class top ~> class order_top
<br>
class bot = fixes bot :: "'a"
<br>
class top = fixes top :: "'a"
<br>
<br>
Could make sense. The question is whether somebody is willing
to
<br>
undertake this change. If you would consider this, you find the
first
<br>
clues at
<br>
<a class="moz-txt-link-freetext" href="http://isabelle.in.tum.de/repos/isabelle/file/c5e0073558f3/README_REPOSITORY">http://isabelle.in.tum.de/repos/isabelle/file/c5e0073558f3/README_REPOSITORY</a>.
<br>
Get back here if questions remain.
<br>
<br>
Note that currently we are heading towards a next release in
January or
<br>
February, and time might be too terse to polish and incorporate
a change
<br>
like the one sketched above.
<br>
<br>
Hope this helps,
<br>
Florian
<br>
<br>
</blockquote>
<br>
<br>
</blockquote>
<br>
</body>
</html>