e some
generic UI projects for all kinds of version systems. It will probably
take a few more years until everybody's editor will be ready.
See also http://www.selenic.com/mercurial/wiki/index.cgi/GUIClients for
more information. There are also a few Mac tools, although I have not
tried any of them yet.
Makarius
muesste da der
> > passend abgekuerzte Name rauskommen.
> >
> > Tobias
It is a bit hard to follow this fragmentary stuff, nevertheless I managed
to find the source of the presumed problem.
Concerning "my version", "your version" of the sources, we can do this
properly once we have switched to Mercurial, because it provides unique
version identifiers which other people can use to look up the very version
precisely.
Makarius
* The Isabelle "emacs" tool provides a specific interface to invoke
Proof General / Emacs, with more explicit failure if that is not
installed (the old isabelle-interface script silently falls back on
isabelle-process). The PROOFGENERAL_HOME setting determines the
installation location of the Proo
* Multithreading for Poly/ML 5.1 is no longer supported, only for
Poly/ML 5.2 or later.
* ML bindings produced via Isar commands are stored within the Isar
context (theory or proof). Consequently, commands like 'use' and 'ML'
become thread-safe and work with undo as expected (concerning
top-level bindings, not side-effects on global references).
INCOMPATIBILITY, need to provide prope
* Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm
to 'a -> thm, while results are always tagged with an authentic oracle
name. The Isar command 'oracle' is now polymorphic, no argument type
is specified. INCOMPATIBILITY, need to simplify existing oracle code
accordingly. Note
ally.
>
> Thanks to all the magicians ;-)
And the wizards ...
Makarius
P to Mercurial before the main Isabelle repository would have
another benefit, giving Isabelle developers some practice in working with
the new environment. (Mercurial is much more powerful than CVS/SVN, and
there is more potential to do things wrong for inexperienced users.)
Makarius
On Wed, 1 Oct 2008, Lawrence Paulson wrote:
> In fact, all the links to logics in the theory library section are
> broken.
I have fixed this problem of Isabelle2008 already, and said so recently in
an answer to somebody on isabelle-users.
Makarius
* Wrapper script for remote SystemOnTPTP service allows to use
sledgehammer without local ATP installation (Vampire etc.). See also
ISABELLE_HOME/contrib/SystemOnTPTP and the VAMPIRE_HOME setting
variable. (By Fabian Immler, TUM)
(CVS note: need to move Distribution/contrib/ out of the way, if it
* Simplified main Isabelle executables, with less surprises on
case-insensitive file-systems (such as Mac OS).
- The main Isabelle tool wrapper is now called "isabelle" instead of
"isatool."
- The former "isabelle" alias for "isabelle-process" has been
removed (should rarely occur to
* Goal-directed proof now enforces strict proof irrelevance wrt. sort
hypotheses. Sorts required in the course of reasoning need to be
covered by the constraints in the initial statement, completed by the
type instance information of the background theory. Non-trivial sort
hypotheses, which rarel
struggle to get rid of legacy stuff will continue ...
Makarius
On Tue, 21 Oct 2008, Stefan Berghofer wrote:
> Makarius wrote:
> > You will need the latest Poly/ML 5.2.1 version to prevent a strange GC
> > deadlock problem in 5.1/5.2.
>
> Where can I get the latest version? The latest version offered for download
> on the Sourcef
Our usual packages for use with Isabelle are available here:
http://isabelle.in.tum.de/polyml-5.2.1/
For any serious use of multithreading in recent development snapshots
Poly/ML 5.2.1 is really required, but there is no immediate need to
recompile the official Isabelle2008.
Makarius
* Multithreading for Poly/ML 5.1/5.2 is no longer supported, only for
Poly/ML 5.2.1 or later.
* The default for ISABELLE_HOME_USER is now ~/.isabelle instead of the
old ~/isabelle, which was slightly non-standard and apt cause
surprises on case-insensitive file-systems, or when working with local
copies of the Isabelle repository.
INCOMPATIBILITY, need to move existing ~/isabelle/etc,
~/i
* Simplified main Isabelle executables, with less surprises on
case-insensitive file-systems (such as Mac OS).
- The main Isabelle tool wrapper is now called "isabelle" instead of
"isatool."
- The former "isabelle" alias for "isabelle-process" has been
removed (should rarely occur to
o now. In principle, one could have both
repositories active for a few days, and merge later using means of
Mercurial, but things should be kept as simple as possible.
Makarius
official Netbeans
repository yet, but see here
http://blogtrader.net/page/dcaoyuan/entry/new_scala_plugin_for_netbeans
This description is for 6.5 RC2 and works for 6.5 final unchanged. The
plugin uses the current Scala 2.7.2.final.
Makarius
lso 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
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
On Tue, 2 Dec 2008, Tjark Weber wrote:
> On Sun, 2008-11-30 at 14:08 +0100, Makarius wrote:
> > The old isabelle-interface wrapper could react in confusing ways if
> > the interface was uninstalled or changed otherwise. Individual
> > interface tool configuration is now mo
On Tue, 2 Dec 2008, Tjark Weber wrote:
> On Sun, 2008-11-30 at 13:03 +0100, Makarius wrote:
> > * The default for ISABELLE_HOME_USER is now ~/.isabelle instead of the
> > old ~/isabelle, which was slightly non-standard and apt cause
> > surprises on case-insensitive file-sys
On Wed, 3 Dec 2008, Gerwin Klein wrote:
> Makarius wrote:
> > Of course, heaps produced inside the repository file space like that must
> > not be committed.
>
> We might want to add an .hgignore file and put ^heaps/ in it. This should at
> least make accidental com
about the old $Id$ artifacts is to remove them gradually,
or just ignore them for now.
Makarius
should
be done with great care.
Makarius
On Tue, 2 Dec 2008, Tjark Weber wrote:
> On Tue, 2008-12-02 at 22:09 +0100, Makarius wrote:
> > With Mercurial you have the whole history always around, and there is no
> > need to encode (tiny) parts of it in the file.
>
> Certainly $Id$ keys are rather useless as long as
re using. For the
development snapshot the release name is the id of the changeset that
makedist encountered as "tip".
If anybody uses the repository directly, not a release, then "hg tip" will
provide that information.
Makarius
semantic conflict was resolved.
Makarius
===
3.3 Simplifying the pull-merge-commit sequence
The process of merging changes as outlined above is straightforward, but
requires running three commands in sequence.
hg pull
hg merge
7 version.
>
> I am using
> Linux 64-bitIsabelle2007?polyml-5.2
> ProofGeneral-3.7.1
Normally there is no need to use the 64 bit version, unless you have
something like 8 GB of real memory. The 32 bit version is a bit faster.
Makarius
lle/polyml
~/isabelle/ProofGeneral
~/isabelle/E
...
With this layout there is no need to edit ~/.isabelle/etc/settings or
create symlink etc.
Makarius
://tortoisehg.wiki.sourceforge.net/hgtk
For example, the "hgtk log" tool is similar to the old "hg view" (which
was a bit ugly due to Tcl/Tk).
Makarius
* HOL: command 'atp_messages' displays recent messages issued by automated
theorem provers. This allows to examine results that might have got
lost due to the asynchronous nature of default 'sledgehammer' output.
(This acknowledges the fact that sledghammer occasionally breaks the
Pro
or in Isabelle.app/../Isabelle
Likewise for Emacs, but it is also found in
/Applications/Emacs.app/Contents/MacOS/Emacs if available.
The Mac OS application bundle is meant to become part of the next official
Isabelle release, which is due within the next 2 months or so.
Makarius
* Proofs of fully specified statements are run in parallel on multi-core
systems. A speedup factor of 2-3 can be expected on a regular 4-core
machine, if the initial heap space is made reasonably large (cf. Poly/ML
option -H). [Poly/ML 5.2.1 or later]
* High-level support for concurrent
On Tue, 23 Dec 2008, Makarius wrote:
> * Proofs of fully specified statements are run in parallel on multi-core
> systems. A speedup factor of 2-3 can be expected on a regular 4-core
> machine, if the initial heap space is made reasonably large (cf. Poly/ML
> option -H). [P
On Sun, 30 Nov 2008, Makarius wrote:
> After several months of getting acquainted with "distributed version
> control" in general, we should be finally ready to switch the official
> Isabelle repository to Mercurial.
> After pressing the red button, the conversion j
ise, try the newest polyml 5.2.1, or even the
> cvs head.
Poly/ML did not change yet after the 5.2.1 release, so trying just the
version from http://isabelle.in.tum.de/polyml-5.2.1/ should be fine.
Makarius
about Mercurial not trusting the default hgrc of the
central pull/push area can be disabled like this:
[trusted]
users = wenzelm
This needs to be added to ~/.hgrc on the server side within the broy
network at TUM.
Makarius
", so anything new that is
also user relevant should be entered there; if it is not user relevant, it
is probably a condidate for deletion.
Concerning the CONTRIBUTORS file: if you are too shy to add yourself, you
can also tell me and I will do it.
Makarius
On Wed, 11 Feb 2009, Florian Haftmann wrote:
> Concerning the number of merges, it is just - as far as I know - an
> observation that in presence of parallel proofs less merges increase
> speed. But perhaps Makarius can tell further details regarding this.
In principle you do not hav
On Sat, 28 Feb 2009, Brian Huffman wrote:
> Quoting Makarius :
>
> >In particular, merging
> >ATP_Linkup is a bit critical: if it is done via several unrelated paths,
> >then some internal derivations are duplicated unnecessarily. (In fact, it
> >used to crash
; that have accumulated over time.
Making syntax subject to name spaces is even more difficult --
interestingly the Scala people have given up on that idea altogether.
Nonetheless, I could imagine to have at least infixes managed in a more
systematic way, not just collections of grammar productions.
Makarius
On Mon, 2 Feb 2009, Makarius wrote:
> * Merges can be simplified by doing "hg fetch" frequently, especially
>just before starting to perform local edits. Also do not forget to
>push eventually, to give others a chance to pick up the changes.
>
>Note th
I've found some nice illustrations on the web ...
Mercurial: http://tinyurl.com/cxrbjt
CVS:http://tinyurl.com/dk3gsz
Makarius
On Wed, 4 Mar 2009, Brian Huffman wrote:
> Quoting Makarius :
>
> >I've found some nice illustrations on the web ...
> >
> >Mercurial: http://tinyurl.com/cxrbjt
> >CVS:http://tinyurl.com/dk3gsz
>
> So, you're saying that with Mercurial, y
d
diff.extended = cyan bold
diff.file_a = red
diff.file_b = green
diff.hunk = magenta
diff.deleted = red
diff.inserted = green
diff.changed = white
diff.trailingwhitespace = bold red_background
Note that the "less" pager requires option -R (e.g. via env LESS) to
interpret color codes properly.
Makarius
*** ML ***
* More systematic treatment of long names, abstract name bindings, and
name space operations. Basic operations on qualified names have been
move from structure NameSpace to Long_Name, e.g. Long_Name.base_name,
Long_Name.append. Old type bstring has been mostly replaced by abs
nonical HHF form. Many Isabelle tools will choke on
that, and are perfectly right to do so.
Whenever you need to produce propositions in non-standard ways, you can
apply explicit norm_hhf operations to "repair" them before passing on to
user-space tools. E.g. like this:
lemma "False ==> (!!uu m n x. P x --> Suc(2 *m) ~= 2 *n)"
apply (tactic {* Goal.norm_hhf_tac 1 *})
apply (tactic {* blast_tac HOL_cs 1 *})
done
Makarius
s]
fetch = -m "merged" -v
Makarius
end
*}
Above @{const_name UNIV} should be @{const_syntax UNIV} -- this
corresponds to the CONST marker in the 'translations' specification.
BTW, these markers are smart enough to handle both old and authentic
syntax as expected.
The former @{const_name UNIV} happened to coincide with @{const_syntax
UNIV}, because the constant was both global and non-authentic.
Makarius
-world" images is
taken for granted, although these days few people might remember that this
was quite commonplace in the past (notably in the Lisp community). Our
SML platforms are in the same tradition: no separate loading of modules,
but persistent heap images.
Makarius
*** ML ***
* Simplified ML attribute and method setup, cf. functions Attrib.setup
and Method.setup, as well as commands 'attribute_setup' and
'method_setup'. INCOMPATIBILITY for 'method_setup', need to simplify
existing code accordingly, or use plain 'setup' together with old
Method.add_method.
hy) and for the
> future I will think of a better example to illustrate
> this function.
BTW, you can get Poly/ML 5.2.1 from
http://isabelle.in.tum.de/polyml-5.2.1/
Makarius
ions. It appears to work if you make the binding of "init"
explicit in locale r1, using the 'for' in postfix notation:
locale r1 =
r0 "init :: 'buffer => ('buffer \ 'value) set => 'value" for init
+ fixes d2i :: "('buffer \ 'buffer) => 'buffer"
begin
...
Makarius
n) const".
There are many problems like this with old-style syntax, but switching
everything to authentic syntax in one big swoop will cause much greater
trouble. In the past 2 years we have already eliminated a fair amount of
old syntax, and this will continue, but requires great care.
Makarius
* Complete re-implementation of locales ...
- More flexible mechanisms to qualify names generated by locale
expressions. Qualifiers (prefixes) may be specified in locale
expressions, and can be marked as mandatory (syntax: "name!:") or optional
(syntax "name?:"). The default depends for plain
NEWS,
CONTRIBUTORS etc., but one needs to desist the temptation for last-minute
"fixes" that usually break things.
Makarius
e Isabelle / Proof General
session:
ML {* getenv "ISABELLE_HOME" *}
This should point to your Isabelle snapshot, and the
contrib/SystemOnTPTP/remote should be in there, unless it got lost
somehow.
Makarius
(homegrown Linux kernel, exotic Emacs version etc.) against the official
packages provided from the website.
Makarius
).
* No change of Proof General, so it will be just 3.7.1 for the release.
Makarius
for x86-darwin, but ppc-darwin
could be included as well, if there are still users for that platform.
Please try Isabelle.app and tell me how it works for you.
Makarius
On Wed, 15 Apr 2009, Makarius wrote:
> see http://www4.in.tum.de/~wenzelm/test/website/dist/Isabelle.dmg.gz
I have ironed out a few minor issues and updated that file. Main changes:
* Use Aquamacs instead of Carbon Emacs. Aquamacs appears to be
better maintained and works m
tform combinations.
Makarius
drive/c/Documents and Settings/chris
This should work in general, because Unixish tools do not expand symlinks
under normal circumstances.
Makarius
belle
packages probably still depends on this feature internally. IIRC, it was
introduced to accomodate old-style type names such as "*" which will still
be with us for some time. In newer developments, those that are less than
10 years old, plain identifiers are used uniformly of course.
Makarius
ularly bad as a permanent tracing facility, because it will
interfere with any debugging that users attempt out there. (The Metis
linkup is particularly verbose, and many people have already asked about
these odd messages that usually occur without context. In the worst case
there will be even a denial-of-service in Proof General.)
Makarius
AFP
tests can come a bit later (hours or days, but not weeks).
* Any "user-relevant changes" should be documented in NEWS (say within
1-2 weeks after a push, afterwards it is usually forgotton).
* Any relevant contribution should get an entry in CONTRIBUTORS.
Makarius
On Thu, 18 Jun 2009, Brian Huffman wrote:
> On Thu, Jun 18, 2009 at 10:55 AM, Makarius wrote:
>> ?* The main Isabelle repository http://isabelle.in.tum.de/repos/isabelle
>> ? ?always needs to be in a state where
>>
>> ? ? ?isabelle makeall all
>>
>> ? ?fini
BELLE_TOOLS setting (which is a colon
separated list of directories, and can be configure in your
~/.isabelle/etc/settings).
Makarius
ot; by simp
>> qed
>>
>
> I have nothing against proofs like this one, but I agree that it is a
> matter of taste.
Do you mean you want to be able to prove False unconditionally?
Makarius
ess a theory contributes
to Main, it must include Main. Otherwise all kinds of strange effects can
occur, even with Plain.
Makarius
"fixing" problems: unless this is done by
someone with a deep understanding of the component in question (usually
the original author or main maintainer), it is usually introducing more
problems than are resolved.
Makarius
gt;> problems than are resolved.
>
> If this is a plea for more maintainable code, one can hardly disagree.
> Documentation might help, as might unit tests.
No, this refers to deep understanding what is really going on, not any
superficial poking around with "modern" things that come and go every few
years.
Makarius
roper log entries are mainly meant to describe changes
semantically to enable understanding of the history of sources many months
or years later. Log entries of the form "now we have finished this" or
"now we have fixed that" would be usually wrong anyway.
Makarius
might have changed a bit in
recent internal versions. Which one did you use?
Makarius
quite
bulky and taking rather long to build.)
Makarius
ww.aip.org/stixfonts/
Their struggle probably shows how difficult mathematical font design
actually is. Or maybe these guys are just clueless?
Makarius
On Wed, 29 Jul 2009, Alexander Krauss wrote:
> Makarius wrote:
>> I am still hoping that the STIX project will deliver something after all
>> these years, see http://www.aip.org/stixfonts/
>
> I like the website:
>
> The target date for final release of this produ
view on Webkit).
* Maybe an updated version of Sun's JVM-based PDF viewer -- seems to be
part of some Fx stuff coming a bit later.
In the mean time we have our own problems of getting robust Isabelle/Scala
integration, with all the gory details done right, so that in the end
there will be a usable system.
Makarius
usually caused by the infamous "handle _" which should
never occur in user code; the "try" and "can" combinators will do it
properly.
Such misinterpreted interrupts might cause strange behaviour, but
editor/toplevel state synchronization should not be lost.
Makarius
romising so far.
One minor problem with non-English keyboard: the alt-graph key is remapped
by default, but something like this will help:
(custom-set-variables '(ns-alternate-modifier 'none))
Makarius
*** ML ***
* Structure Synchronized (cf. src/Pure/Concurrent/synchronized.ML)
provides a high-level programming interface to synchronized state
variables with atomic update. This works via pure function
application within a critical section -- its runtime should be as
short as possible; beware of
bout repository
versions by giving official changeset ids. "The repository version" is
not a defined thing, and can change every minute.
Makarius
y this:
thm_deps test
If you open the tree folds of "HOL" you will see a list of theorems -- the
graph view is not so nice in this case.
Makarius
longer and longer as the
system gets more complex.
Now is the time to finish things and put them into a state for end-users
out there. If there are still major things waiting in your pipeline,
please say so.
Makarius
On Tue, 20 Oct 2009, Lawrence Paulson wrote:
> HOL is not building, see attached. Don't ask for the change set identifier
> because I couldn't tell you even to save my life.
How about "hg id" then?
It works again in 60a098883d81
Makarius
n "framework" with proper
stoppers etc. is a bit tricky.
Applying combinator expressions directly to input tends to expose
certain internals that might make you wonder if it really works
correctly. (One weakness of the framework is in its non-abstracted
types. This was done that way many years ago, because there are
actually several variants rolled into one.)
Makarius
Since Scala is becoming more and more important for Isabelle system
programming, some of you might be interested in the new book from
O'Reilly:
http://oreilly.com/catalog/9780596155957/index.html
http://programming-scala.labs.oreilly.com/
Makarius
sionally causing
confusion in the past, and had to dissappear altogether when precise
counting of source positions was introduced.)
This means that ML sources with Isabelle symbols cannot be pasted into the
raw ML loop. In practive you need a proper context anyway (for
antiquotations etc.) so it is best to work trough Isar/ML all the time,
unless you do really low-level work on the ML system itself.
Makarius
;use" function from the raw ML toplevel should coincide
>> with that.
Now I understand that with "ML" in the table you mean the raw Poly/ML
toplevel. This is not under our control, so it will be the same
independently of the Isabelle version.
Makarius
ion 1.1.3. In particular, users can add their own components in
"$ISABELLE_HOME_USER/etc/components", without having to edit central
defaults.
Makarius
was a Spontaneous Massive
Existence Failure of PG 3.7.1 and PG pre-4 on Ubuntu 9.10, concerning
Emacs 22 and 23 (Gtk). (Those who are not following the Ubuntu or PG
issue tracker, can use plain old emacs22-x until things are sorted out.)
IIRC, you are also using Ubuntu 9.10. Which version of Emacs works for
you?
Makarius
tion of PG + Emacs that works
on Mac OS. GNU Emacs 23 somehow fails -- tickets will come when I've
managed to pin down the problems.
Makarius
problem #300.
My general impression is that PG-4 prefers Emacs 23, but this usually
requires to upgrade to newer Linux installations, which is apt to cause
other problems, as we have seen.
Makarius
t;logical framework", and not use term "meta logic" anymore.)
Makarius
al classical rule
without equality?
Moreover, see src/HOL/Hilber_Classical.thy for proofs of tertium-non-datur
derived from Hilbert Choice.
Makarius
tification and implication", but now it
has only one version and the other layer expresses pure ND outlines.
BTW, the mechanism for calculational reasoning in Isar can serve as a
simple example fto study the benefits of "declarative" ND rules in Pure.
People have occasionally tried to implement calculational reasoning in
other systems, but it came out more complicated and less general.
Makarius
ving the lambda.
Plain old HOL will have a hard time imitating Isar without Pure ND rules.
One would either have to reinvent it, or rethink the whole thing from the
ground up.
Again: look at example of Isar calculations, to see where the rule
framework of Pure comes into place.
Makarius
101 - 200 of 2785 matches
Mail list logo
