On Tue, 4 Nov 2014, Makarius wrote:
Strange hacks that work around the absence of proper options encumber
the introduction of them eventually. It is the usual bootstrap problem
for reforms.
I actually did start some work in the vicinity of resolve_tac with
proper context recently
On Tue, 10 Feb 2015, Makarius wrote:
Sourceforge is presently in down due to serious technical problems. This is
relevant for afp-devel.
Here is my own clone of it: https://bitbucket.org/makarius/afp-devel
In particular afp-devel/2aa8b0c283eb corresponds to
Isabelle/59817f489ce3 with its
preds/succs within the graph dependencies).
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
out by Florian, although that would
have to treat cyclic graphs, which is presently not supported.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
symbols.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
of jedit itself.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
as
well), just to save a lot of time in the actual work.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
aggresively like Isabelle_System.with_tmp_dir with rm_tree.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
missing. I hope to wrap it up
eventually for the coming release (this Spring) -- like various other
things that are still in the pipeline and got delayed as usual (e.g.
important reforms for Eisbach).
Makarius
___
isabelle-dev mailing list
tested?
Probably not. The log.gz files should contain some information what
really happened -- it might actually provide further clues about the above
crash.
As a quick workaround it might also help to use ML_OPTIONS=-H 1500 or
even ML_OPTIONS=-H 2000.
Makarius
?
Maybe there is some conflict of new vs. old properties and keymaps.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
belong to normal Isabelle user space.)
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
.
Makarius
http://stop-ttip.org 1,235,896 Participants
___
isabelle-dev mailing
generated types, to eliminate this potential
of surprise.
Makarius
http://stop-ttip.org 1,235,909 Participants
On Tue, 30 Dec 2014, Makarius wrote:
So far this is just an intermediate outline of some reforms that came
about spontaneously. We are right in the middle between two releases,
so more is likely to happen.
Another reason why more parallelism is likely to happen is my new (very
modest
to get confused by that as can be seen here:
http://lists.inf.ed.ac.uk/pipermail/polyml/2014-December/001497.html
Makarius
http://stop-ttip.org 1,151,632 people so far
packages
etc.) to use type Input.source instead of string, such that funny YXML
markup in those strings may be discontinued. That would be a rather
drastic change of ML signatures, though.
Makarius
On Wed, 10 Dec 2014, Tobias Nipkow wrote:
On 09/12/2014 21:50, Makarius wrote:
On Wed, 10 Dec 2014, Gerwin Klein wrote:
“build -a” is still going to miss document preparation errors in the
AFP,
though, so it’s still not really the right command to run for testing
it.
We've had
can remove that and use option preferences instead, e.g. see
Isabelle/jEdit plugin properties: Isabelle / General / Miscellaneous Tools
/ Z3 Non Commercial.
Makarius
http://stop-ttip.org
, but without any add-on features such as -g AFP.
Makarius
https://stop-ttip.org/signatures-member-states
.
Makarius
https://stop-ttip.org/1,120,204 people so far
___
isabelle-dev
the session itself by auxliary theories with suitable
imports. Another way is to make an auxiliary ROOT that resides in some
subdirectory of AFP/thys/AODV and is only included by the few people need
them occasionally (using -d DIR in isabelle build or isabelle jedit).
Makarius
and completion etc. of the underlying editor buffer.
This reform has required countless years, but after the recent deletion of
the TTY loop it became feasible. If anything has been forgotten or causes
surprises, please report observations here.
Makarius
name space problems preventing that.
Makarius
http://stop-ttip.org 946,179 people so far
and what not.)
Makarius
http://stop-ttip.org 927,552 people so far
On Mon, 3 Nov 2014, Timothy Bourke wrote:
* Makarius makar...@sketis.net [2014-11-02 20:24 +0100]:
*** Document preparation ***
* Document headings work uniformly via the commands 'chapter',
'section', 'subsection', 'subsubsection' -- in any context, even
before the initial 'theory' command
context recently, but it will require more time to revisit really ancient
parts of the system, not to say ancient habits.
Makarius
http://stop-ttip.org 787,957 people so far
some decades ago. How do
you feel about it being called ap2 or apply2?
Makarius
http://stop-ttip.org 777,356 people so far
On Mon, 3 Nov 2014, Timothy Bourke wrote:
* Makarius makar...@sketis.net [2014-11-02 20:24 +0100]:
*** Document preparation ***
* Document headings work uniformly via the commands 'chapter',
'section', 'subsection', 'subsubsection' -- in any context, even
before the initial 'theory' command
/ML is not yet an Isabelle development
activity, so it can be discussed on isabelle-users -- unless you want to
propose concrete changes to ongoing repository versions.
Makarius
http://stop
encumbered us long enough. Now the popular keyword ; has become free as
literal token in the outer syntax.
It is presently unused, but the Eisbach proof method language could use it
as notation for THEN_ALL_NEW, for example.
Makarius
odd LaTeX
tricks to turn it into other personalities. Direct use of 'chapter' etc.
now works without further ado, also in the Sidekick document overview.
Makarius
http://stop-ttip.org 774,989
to it. On the other
hand, commands may be built on top of each other, and I did not want to
add further complexity for some inheritance system of plugins.)
Makarius
http://stop-ttip.org 738,307 people
On Wed, 8 Oct 2014, Makarius wrote:
*** ML ***
* Basic combinators map, fold, fold_map, split_list are available as
parameterized antiquotations, e.g. @{map 4} for lists of quadruples.
There was an off-list proposal by René Thiemann to define the following
antiquotation:
@{map_tuple n
perl in the PATH needs to provide LWP::Simple, e.g. for
isabelle components or remote Sledgehammer.
This is one of the rare situations where we still have the IKEA principle:
users need to make sure that they have a proper perl installation.
Makarius
On Tue, 16 Sep 2014, Makarius wrote:
On Fri, 5 Sep 2014, Jasmin Christian Blanchette wrote:
I would like to propose either replacing the old mechanism by the new one
or having both live in parallel in Pure. It is certainly not perfect,
but it is IMO an improvement over the statu quo. What
of such an
external tool integration, according to the routine approach of Isabelle
today.
Makarius
http://stop-ttip.org
and for all. The changset also eliminates
some clones that have accumulated over the years.
Isabelle/ML has antiquotations as some kind of macro language. It can do
certain things better than the C preprocessor, although one always needs
to be careful to stay within reason.
Makarius
).
Both Isabelle/ML and Isabelle/Scala have become quite able system
programming languages in recent years, so the need for funny scripting
languages is more and more diminished.
Makarius
to delete Proof
General and the TTY loop?
Makarius
http://stop-ttip.org
to see anything -- too much blue
underlining in irrelevant places.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
introduced new mistakes beyond the old Emacs mode, I would like to
see sample .bib files. The easychair.bib file has already served well to
drive various bibtex modes to their limits.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
On Thu, 25 Sep 2014, Makarius wrote:
HOL-Proofs is important in various ways: theoretically it opens the
possibility for independent checking of proofs by a different system,
and thus raising the level of confidence in Isabelle results;
practically it indicates how close we are to the next
.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
message, but such file-systems are
common-place on Windows and Mac OS X, i.e. the majority of user platforms.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
waste our time in the maintenance, but
also time of potential users.
So the NEOS/CSDP server setup looks like a canonical candidate for
deletion. That would also allow to remove Python from the Windows/Cygwin
app bundle and save many MBs of disk space.
Makarius
On Mon, 22 Sep 2014, Tobias Nipkow wrote:
On 22/09/2014 16:52, Makarius wrote:
On Thu, 11 Sep 2014, Lawrence Paulson wrote:
I have installed a copy of the software locally. Would be worth making this a
component?
This canonical question has come up each time, after someone spent
soon become a changeset to remove
the xnum token syntax from Pure.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On Mon, 22 Sep 2014, Makarius wrote:
Looking once again at ZF xnum syntax, I think it can be expressed
without the xnum token, and without any syntax change for now -- that
may be reconsidered independently.
See now:
changeset: 58420:37cbbd8eb460
user:wenzelm
date:Mon Sep
On Mon, 22 Sep 2014, Makarius wrote:
I have the component already -- it was much easier to make than the
cumulative mail traffic about this topic. I merely need to test it a
bit more, before it becomes a standard component for everybody.
See also Isabelle/00bf84d3f526.
So far
with this important thread, but I am presently
not well-connected. I will come back later, when I have studied the
situation carefully.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu
On Thu, 7 Aug 2014, Makarius wrote:
This is an update on the ongoing release / testing process:
* The next release candidate (Isabelle2014-RC3) will probably appear at
the 1 week distance that we've had so far, i.e. next Sunday or Monday.
* I will merge back the isabelle-release
according to the semantics of the mailing list.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On Tue, 22 Jul 2014, Makarius wrote:
Notes to the webmaster:
* The Isabelle website repository is already for Isabelle2014.
* I have made some totally adhoc changes to the current website to
insert the snippet for VSL 2014 with Isabelle2014-RC0.
The still official website is back
.
Their might be other snags that are not documented, so it is important to
keep two eyes on it as usual.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On Fri, 25 Jul 2014, Gerwin Klein wrote:
On 25 Jul 2014, at 10:23 am, Makarius makar...@sketis.net wrote:
Oddly, people are still seen using 'find_theorems' etc. inlined into the source
text. That was an intermediate approach from several years ago. If it is still
used today, what
to trigger
the completion popup.
I changed that again, see 0f708666eb7c and ff31aad27661 with many more
history references in the changelog.
That means: symbol completion works within a word context, but keyword
completion not.
Makarius
before Isabelle2014-RC1.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On Thu, 24 Jul 2014, Makarius wrote:
On Mon, 10 Mar 2014, Ondřej Kunčar wrote:
This refers to 682bba24e474.
If I have a theory file that contains a method that loops (use for example
lemma False by (intro FalseE)) and if I close this file in JEdit, the
method presumably still loops
to the current website to
insert the snippet for VSL 2014 with Isabelle2014-RC0.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
now. I have myself a long list of minor items, which are cumulatively
quite some substance to digest.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
is something for the next release.
I can't say anything myself how it would impact the bootstrap of Main HOL.
As long as this question does not arise for the Isabelle2014 release, I
would say: go ahead and renovate it.
Makarius
___
isabelle-dev
.
This use is no counter example yet, and very rare in practice.
IIRC, Florian Haftmann made the overloading target to include such
boundary cases, or rather he did not do anything specific to exclude them.
Makarius
___
isabelle-dev mailing
:
lemma x = x by smt
The SMT solver Z3 is not activated. To activate it, set the Isabelle
system option z3_non_commercial to yes
(e.g. via the Isabelle/jEdit menu Plugin Options / Isabelle / General).
See also http://z3.codeplex.com/license
Makarius
On Fri, 4 Jul 2014, Makarius wrote:
On Tue, 1 Jul 2014, Makarius wrote:
I am about to update the website, such that Isabelle2014-RC0 can be
published with an approximation of the one for the coming release.
I will tag Isabelle2014-RC0 today or tomorrow, shooting blindly at the
repository
could mark 'defs' as legacy now, and remove it eventually.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On Sat, 5 Jul 2014, Makarius wrote:
On Fri, 4 Jul 2014, Makarius wrote:
On Tue, 1 Jul 2014, Makarius wrote:
I am about to update the website, such that Isabelle2014-RC0 can be
published with an approximation of the one for the coming release.
I will tag Isabelle2014-RC0 today
On Thu, 12 Jun 2014, Florian Haftmann wrote:
This is an offspring from
http://fa.isabelle.narkive.com/QI1dxXvo/isabelle-quotient-type-command-fails
I do not recommend white space in theory names: over the years proper
naming conventions have been increasingly enforced for logical entities
like
ways to achieve that today, e.g. via theory begin/end hooks).
Actual use of extend is rare and usually somewhat exotic, but also happens
to be in important kernel modules. Since there is no true
counterindication against it, we should keep things as is.
Makarius
On Tue, 1 Jul 2014, Makarius wrote:
I am about to update the website, such that Isabelle2014-RC0 can be
published with an approximation of the one for the coming release.
I will tag Isabelle2014-RC0 today or tomorrow, shooting blindly at the
repository. This is not a regular release
/rev/fa14d60a8cca
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On Thu, 3 Jul 2014, Johannes Hölzl wrote:
However this happened at the Scala level. Nitpick produced a huge number
in Suc representation, which the output panel was only possible to
display when the Java stack size was 16MB.
This is a shit happens instance on the JVM, which has a lot of
d8d16bd1a839 is semantically meant for Isabelle2014.
Accidental updates of the still current website for Isabelle2013-2 need to
be avoided! From now on, it is de-facto in frozen state.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
. Please provide your input.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On Tue, 25 Mar 2014, Makarius wrote:
* pointer_eq is not part of SML and requires extra reasoning that it is
correct whenever it is used (normally in certain hot-spots of kernel
operations). See also the surprise caused by some optimizations of
the Poly/ML runtime system
theory_target.ML).
Direct comparison of the files is probably difficult, but I have followed
most of the individual changesets. So far it looks formally OK for the
release.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https
:25 2014 +0200
summary: fixed soundness bug in monotonicity-based type encodings --
the helper facts must be considered too
In contrast, the point where Johannes applied some changes to HOL/Library
seems to be OK: 2baecef3207f.
Makarius
that
myself, though, but use the Prover IDE directly for debugging and
tinkering.)
Are there any remaining uses of the Isar toplevel? Otherwise it is
something to be scheduled for eventual removal -- it complicates many
aspects of the system.
Makarius
it into the Isabelle distribution many years
ago.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On Sun, 29 Jun 2014, Cezary Kaliszyk wrote:
Hi Makarius,
On Thu, Jun 26, 2014 at 11:08 PM, Makarius makar...@sketis.net wrote:
At the moment (06599233e54e) there are no remaining uses of Proof General to
the best of my knowledge. If anybody has counter-examples they should be
put
are relevant?
I don't have any special expertise in this area, but merely want to make
sure that we can move on towards the release.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman
shell to run the Build_Doc.build_doc jobs. Apple
full-screen mode now also works nicely, if the icon in the window corner
is used, not the jEdit menu entry.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https
the mira setup.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On Sat, 28 Jun 2014, Makarius wrote:
On Sat, 28 Jun 2014, Florian Haftmann wrote:
suggests that something is bad with $JEDIT_HOME in the mira build
environment.
JEDIT_HOME is a normal Isabelle setting, provided by the etc/settings of that
component within Isabelle. So it should normally
is the lack of positions for type errors in
plain terms within formal specifications of the theory.
I take this report as a reminder and refreshment of the priority of this
non-PIDE compliant part of the system, but it won't be addressed for the
coming release.
Makarius
week for Isabelle2014-RC0 where a broader audience can participte.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
, but in different ways.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
data: hardware parameters, Poly/ML memory options, JVM
memory options, concrete examples etc.
It does not make sense to use Isabelle/jEdit in a way that PG was used 10
years ago, concerning these important side-conditions.
Makarius
___
isabelle
PIDE idioms.
If the latter is missing, their might be a problem with the tool that
emitted the error message.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle
.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
approach in jEdit; it just needs more practice to discover the wealth
jEdit features.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
.
I don't see any show-stoppers here. Just more potential for refinements,
when PG is discarded.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
proper
reports on your hardware and system parameters.
In Isabelle2014 the Sledgehammer integration is in its third generation.
It is supposed to work without problems.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https
, and it will remain in the theory panel
(with an error marker) until you quit jEdit.
You can in principle switch off the continous checking, e.g. in the
Theories panel.
Slight inconveniences and potential for improvements remain, but this is
no show stopper as far as I can tell.
Makarius
* and *read* the original jEdit
user's guide, e.g. see http://www.jedit.org/index.php?page=docs. It is a
very powerful editor, and Emacs looks really awkward compared to it.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https
).
Note that the Theories panel is the main point to look over a whole
project, to see its status -- assuming that the basic project structure is
right.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu
years, but
I am biased, since I know many fine-points of how it really works.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
. This is also the reason, why I
have started to spend signigicant time to make a clear slate, and
eliminate the remaining uses of Proof General first.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu
801 - 900 of 2162 matches
Mail list logo
