, a theory that does not depend on any unnecessarily strong
axioms
also seems to be more appealing from a foundational point of view.
I agree with this.
Makarius
* ML basics: just one true type int, which coincides with IntInf.int
(even on SML/NJ).
* Pure/Isar: unified syntax for new-style specification mechanisms (e.g.
'definition', 'abbreviation', or 'inductive' in HOL) admits full type
inference and dummy patterns (_). For example:
definition K x _ = x
* ML/Isar: simplified interfaces for outer syntax. Renamed
OuterSyntax.add_keywords to OuterSyntax.keywords. Removed
OuterSyntax.add_parsers -- this functionality is now included in
OuterSyntax.command etc. INCOMPATIBILITY.
* System: polyml-platform script now identifies x86_64-linux with
x86-linux, which is usually more efficient. INCOMPATIBILITY, requires
manual settings if x86_64-linux is really intended (e.g. for 2GB heap
or 64MB stack).
installation (homegrown Linux kernel, exotic Emacs version etc.), using
the official binaries provided from the website.
Makarius
On Sun, 6 Jan 2008, Makarius wrote:
* Rudimentary Isabelle plugin for jEdit (see Isabelle/lib/jedit), based on
Isabelle/JVM process wrapper (see Isabelle/lib/classes). Note that the
precompiled jars are only available in a proper distribution, but not in
the internal CVS (cf. Admin
* Theory loader: use_thy (and similar operations) no longer set the
implicit ML context, which was occasionally hard to predict and in
conflict with concurrency. INCOMPATIBILITY, use ML within Isar which
provides a proper context already.
.
Makarius
* Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
INCOMPATIBILITY, object-logics depending on former Pure require
additional setup PureThy.old_appl_syntax_setup; object-logics
depending on former CPure need to refer to Pure.
* ML: rules and tactics that read instantiations (read_instantiate,
res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof
context, which is required for parsing and type-checking. Moreover,
the variables are specified as plain indexnames, not string encodings
thereof.
* ML: Disposed old term read functions (Sign.read_def_terms,
Sign.read_term, Thm.read_def_cterms, Thm.read_cterm etc.).
INCOMPATIBILITY, should use regular Syntax.read_term,
Syntax.read_term_global etc.; see also OldGoals.read_term as last
resort for legacy applications.
that there is no particular
advantage in the NSA part anymore, unless you are specifically interested
in the non-standard thing?
Makarius
* @{lemma} in latex and ML: allow initial and terminal method expressions,
as in the Isar command 'by'.
* @{lemma} in ML now closes the derivation, unless @{lemma (open) ...} is
specified.
the parent directory of
that URL. Note that this is a readonly copy of the official ProofGeneral
CVS from Edinburgh.
As usual, early adopters of PG pre-3.7.1 should post problem reports to
http://proofgeneral.inf.ed.ac.uk/trac/ (you can just create your own
account).
Makarius
On Sun, 24 Aug 2008, Tobias Nipkow wrote:
I don't have a lib subdirectory and cvs does not know about one.
The NEWS are always in terms of a proper distributions, for users out
there. The CVS layout is a bit mangled, and lib is in Distribution/lib.
Makarius
to be on the right track
already: keep with the separate process model. Apart from stability it
also allows to run the prover and GUI an separate machines. (``Modern''
GUIs do need 1 or 2 cores for themselves, just to display things to the
user.)
Makarius
emerging) server infrastructure, I would be happy
to assist them.
Makarius
to put them back
into the CVS.
We are still working on getting more Isabelle people aquainted with
Mercurial, so that we can get rid of CVS eventually.
Makarius
to be de-centralized.)
Makarius
input methods and proper display (without the
flashing of x-symbol for \^sub for example).
Makarius
* Name bindings in higher specification mechanisms (notably
LocalTheory.define, LocalTheory.note, and derived packages) are now
formalized as type Name.binding, replacing old bstring.
INCOMPATIBILITY, need to wrap strings via Name.binding function, see
also Name.name_of. Packages should pass name
On Wed, 3 Sep 2008, Makarius wrote:
Within the next few hours http://isabelle.in.tum.de/repos/isabelle will
recover to the present state of the CVS. Since this is a fresh
Mercurial repository, local clones probably need to be recreated from
scratch.
In the mean tome it might be helpful
.
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 Proof
the magicians ;-)
And the wizards ...
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
* 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 regular
* 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
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 Sourceforge page
http
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,
, 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
of the 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
, implementation) I have already used the @{file} document
antiquotation to get a statically checked references to the Isabelle file
space.
Makarius
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 more explicit, see also
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-systems, or when working
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 commits less likely.
It is already
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 the file is part
. 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
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
~/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
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
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). [Poly/ML 5.2.1
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
On Sat, 28 Feb 2009, Brian Huffman wrote:
Quoting Makarius makarius at sketis.net:
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 here in the past, now
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 that excessively long merge edges
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 makarius at sketis.net:
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, you can do a lot more damage?
Yes
*** 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
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
General.)
Makarius
?
Makarius
with Plain.
Makarius
of the component in question (usually
the original author or main maintainer), it is usually introducing more
problems than are resolved.
Makarius
.
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
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
quite
bulky and taking rather long to build.)
Makarius
combinators will do it
properly.
Such misinterpreted interrupts might cause strange behaviour, but
editor/toplevel state synchronization should not be lost.
Makarius
-English keyboard: the alt-graph key is remapped
by default, but something like this will help:
(custom-set-variables '(ns-alternate-modifier 'none))
Makarius
by giving official changeset ids. The repository version is
not a defined thing, and can change every minute.
Makarius
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
their own components in
$ISABELLE_HOME_USER/etc/components, without having to edit central
defaults.
Makarius
anymore.)
Makarius
files.).
Makarius
, and the use of
it by Isar, facilitated the genericity natural deduction-style
reasoning. Generic proof tools can be written that work across logics.
Makarius, if I understood correctly, was saying that these meta-level
logical mechanisms have a utility even when just within one logic, but I
On Tue, 17 Nov 2009, Tjark Weber wrote:
On Tue, 2009-11-17 at 15:18 +0100, Makarius wrote:
A repository clone is not a proper distribution, and various parts are
missing. The Admin/build script helps to fill these gaps, notably
Admin/build browser
Clemens used to maintain a web page
On Fri, 16 Oct 2009, Makarius wrote:
Dear Isabelle contributors,
we need to approach the next official Isabelle release. The basic plan
is to get things done this fall, which means there are only 2-3 weeks
left for substantial changes. After that there will be a few more weeks
of the official AFP release for Isabelle2009-1 that happens in
parallel.
Makarius
omissions.
Makarius
that would not be possible in Coq, for example.
Makarius
will probably produce the official Isabelle2009-1 snapshot tomorrow.
Makarius
. There
seem to be several things intermingled, and many surprises will show up
when trying to sort things out. Larry is probably closest to
understanding the general outline.
Also note that the ATP linkup is particularly tricky, because there are no
formalized regression tests.
Makarius
.
This state has not yet been achieved for nitpick, where Jasmin *is* fully
responsible right now.
Makarius
On Thu, 14 Jan 2010, Alexander Krauss wrote:
Makarius wrote:
On Wed, 13 Jan 2010, Jasmin Blanchette wrote:
2. Generalize atp_manager.ML so that it can manage arbitrary
assistants, which are tools that take a goal and produce a message --
not just ATPs -- and rename it HOL/Tools
On Tue, 9 Feb 2010, Thomas Sewell wrote:
Thanks Makarius, Syntax.parse_term and Syntax.check_term do indeed seem
to be my friends.
In fact, I sort of wish I'd known about them earlier. I remember in one
of the record package proofs it was annoying me that I had to construct
the types
not invoke the script directly:
the browser already takes care of recompiling the required jars on demand.
Makarius
example for now, you can use Logic.varify
(although that does not work in general local situations, where parts are
fixed and parts are arbitrary).
Makarius
On Wed, 3 Mar 2010, Brian Huffman wrote:
On Wed, Mar 3, 2010 at 8:54 AM, Makarius makarius at sketis.net wrote:
* For longer projects the timespan of staying in splendid isolation
is limited to 1-3 days (3 is already quite long, and personally I
usually try to stay within the 0.5-1.5
* Pure: local theory specifications may depend on extra type variables
that are not present in the result type -- arguments TYPE('a) :: 'a itself
are added internally. For example:
definition unitary :: bool where unitary = (ALL (x::'a) y. x = y)
.
Makarius
___
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
operations to initialize a
certain context.
Tools and packages that have already been localized, and fixrec appears to
be one of them, should never refer to global stuff from the raw
background theory.
Makarius
___
Isabelle-dev mailing list
of the current image size.
How is the timing for your theories? Is there an impact on AFP, for
example. The latter can be taken as an indication how it will affect
other users out there.
Makarius
___
Isabelle-dev mailing list
Isabelle-dev
things will cause many surprises when changed too quickly, i.e. it is
something to do after the release.
Makarius
___
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman
(like
Aquamacs 2.0), because PG 3.7.1.1 will no longer work. I reckon that the
serious problems we already have will escalate within the next 12 months
or so.
Makarius
___
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu
to Aquamacs failing to configure fonts for the buffer. The
other was PG trac item #314 (Duplication of some special messages).
These mysterious message problems might be also related to the general
danger of loosing synchronisation, which have never been isolated to far.
Makarius
4 / Aquamacs 2.0 oddities that
are not really critical, though.
Makarius
___
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On Mon, 17 May 2010, Makarius wrote:
Right now I am bisecting our repository as David suggested, which is an
interesting experience because last year's Isabelle/HOL builds really
fast (factor 2 compared to today). I am close to get to the point,
about 4 more bisections.
The result
On Mon, 17 May 2010, Brian Huffman wrote:
On Mon, May 17, 2010 at 7:43 AM, Makarius makar...@sketis.net wrote:
Right now I am bisecting our repository as David suggested, which is an
interesting experience because last year's Isabelle/HOL builds really
fast (factor 2 compared to today
of weeks,
with great success. I.e. it is faster, and it runs both 32bit and 64bit
applications as before. (Platform identification is quite delicate on Mac
OS though -- forget plain old uname.)
Makarius
___
Isabelle-dev mailing list
Isabelle
On Wed, 19 May 2010, Johannes Hölzl wrote:
Am Montag, den 17.05.2010, 09:41 -0700 schrieb Brian Huffman:
[..]
build times slower by a similar factor? I don't think users would be
very pleased if the new version of Isabelle takes twice as long to
process their old theories.
Today I discoverd
1 - 100 of 2162 matches
Mail list logo
