packages provide the 32-bit
C/C++ standard libraries mentioned above.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
ll questions are answered, especially concerning
"arguments" in some cases.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
t the moment. The internal model is a
bit simplistic.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On Tue, 28 Apr 2015, Gerwin Klein wrote:
Have also kicked off a full test on afp-2015 now and if all goes well,
I’ll switch it to automated once a day until the release.
Looks like another bit of infrastructure overhaul is needed in my
scripts for running afp-test in parallel for an upcoming
On Tue, 28 Apr 2015, Larry Paulson wrote:
Today I added some material about complex transcendental functions, and
then tested as usual. Two things didn’t work: HOL-Hoare_Parallel and
HOL-Proofs-ex. I fixed the former myself. No idea what’s wrong with the
latter.
I am presently not on the isa
On Tue, 28 Apr 2015, Gerwin Klein wrote:
You’re right, it is currently not tested automatically. I was going to
set this up on the weekend, but didn’t manage to.
As far as I’m aware, there weren’t any commits to afp-2015 after the
fork apart from one update that was a leaf node that I checked
, Separation_Logic_Imperative_HOL,
UpDown_Scheme
That is without the "slow" sessions.
Is afp-2015 actually tested anywhere?
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On Mon, 13 Apr 2015, Johannes Hölzl wrote:
BTW, can the predicate_compiler setup s.t. typedefs are ignored
automatically?
Is there anybody who understands that aspect of the predicate compiler?
Makarius
___
isabelle-dev mailing list
ars. This also applies to the
relatively new "co" versions.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
pile them for a long time.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On Fri, 17 Apr 2015, Makarius wrote:
After the announcement of Isabelle2015-RC1 there are 48 more hours on the
main Isabelle repository, before the critical fork to
https: //bitbucket.org/isabelle_project/isabelle-release happens.
The fork will happen in 1-2h.
To make clear which changesets
file $ISABELLE_HOME_USER/jedit/activity.log
but it only contains messages of higher priority. (There might be ways to
configure that in jEdit.)
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
and potentially
non-terminating tasks in the IDE.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
of the release branch, until everything
is merged again at the end of May or start of June.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Just for the historical record: in Isabelle/caf2637a28a9 all of
AFP/a44a0c9e17ef works.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
official releases or release candidates is for isabelle-users.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
ople sticking to old hardware, and expecting that things are
still fast. Moore's Law means that hardware is continously updated by
cheaper and faster machines.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.
more days to sort out reported
problems directly in the main Isabelle repository.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
or this release, though.
Hopefully the main corner cases are already covered with the above
robustification.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
this is just the normal behaviour of the JVM under low-memory
conditions. I routinely have local settings like this:
ISABELLE_BUILD_JAVA_OPTIONS="-Xms1024m -Xmx4096m -Xss4m"
This can't be as aggressive by default, because it means it won&#
In Isabelle/f5c4b49c8c9a and AFP/420dac7d9446 from today the situation of
various AFP sessions is as bad as some days ago:
Promela FAILED
(see also
/home/makarius/.isabelle/heaps/polyml-5.5.3_x86-linux/log/Promela)
*** At command "by" (line 1082 of
"~/isabelle/afp-dev
ledgehammer panel?)
BTW, the Sledgehammer manual still describes a situation before the
Sledgehammer panel came into existance in 2013. (It mentions the earlier
Auto Sledgehammer in PIDE, though.)
Makarius
___
isabelle-dev mailing lis
On Sun, 12 Apr 2015, Larry Paulson wrote:
You should always have success by unfolding powr_def. And I’m told that
the necessary changes to “approximation” are not difficult.
Does that mean there will be further changes, to make it fully work in the
coming release?
It would be nice to see th
store;
That is all about BNF, and Dmitriy has already said that he will continue
work there after the relase. Eliminating Local_Theory.restore will make
it possible to use "private datatype" for example, and get the expected
effect on the name space en
On Thu, 9 Apr 2015, Makarius wrote:
Back to the actual topic of this thread: If you want to change the
syntax for the release, there are a very few days left until the first
release candidate is published
Is there still anything coming for the release on this thread?
Makarius
ck" (line 145 of
"~~/src/HOL/Quickcheck_Examples/Hotel_Example.thy")
Since there is no way around a full "isabelle build -a" before pushing
anything, such incidents can't happen, at least in theory.
Makarius
___
opportunity to update NEWS and CONTRIBUTORS,
or to point out missing bits.
As a blind shot at ongoing changes, I will make a pre-test snapshot
Isabelle2015-RC0, so that more people can get an impression what is
coming, and hopefully more reports on remaining problems.
Makarius
oth the defined const and its defining fact.
There is no particularly need to update anything right now. Starting the
release process has priority over fine-tuning of existing theories.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
, e.g. odd problems
with binaries on Linux or Windows.
Great. I have seen this in the vicinity of 1e3383a5204b.
Can you explain the status of Old_SMT? Is there anything that isatest
still needs to run here?
Makarius
___
isabelle-dev ma
yword clashes still left to address, "concl" is one of
them.)
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On Tue, 7 Apr 2015, Makarius wrote:
On Tue, 7 Apr 2015, Tobias Nipkow wrote:
On 07/04/2015 14:37, Christian Sternagel wrote:
> (b) qualified
That gets my vote because it expresses clearly the description Makarius
gave: "name space entry that is only accessible by qualified nam
the BNF guys to say if they intend to do something for the
Isabelle2015 release, or just leave the status quo. It is unlikely that
anybody will notice fine points of private datatype definitions before the
next release after Isabelle2015.
Makarius
___
On Tue, 7 Apr 2015, Tobias Nipkow wrote:
On 07/04/2015 14:37, Christian Sternagel wrote:
(b) qualified
That gets my vote because it expresses clearly the description Makarius
gave: "name space entry that is only accessible by qualified names"
It is definitely good to colle
ws to access inaccessible names, after some tweaking of the
name space, e.g. via aliases. This could justify the use of 'private' for
what is now 'restricted', or it might be just too confusing to users.
Note that it is now releatively easy to test feasibility of ne
;
It is immediately clear what it does, and that there is no problem with
it. This mail thread could have been shortened by posting the ML
definition earlier. But the main thing is not the kernel here, it is user
ML code that is a bit outdated concerning proper use of context.
Makarius
On Thu, 2 Apr 2015, Peter Lammich wrote:
On Do, 2015-04-02 at 00:16 +0200, Makarius wrote:
* The main operations to certify logical entities are Thm.ctyp_of and
Thm.cterm_of with a local context;
Does this mean that you added functionality concerning the local context
to the Isabelle kernel
On http://isabelle.in.tum.de/reports/Isabelle there is very little to see.
This is occasionally important to investigate timing problems, or to see
how Isabelle vs. AFP works out.
Makarius
___
isabelle-dev mailing list
isabelle
the ECB, people don't seem to
invest money for anything useful, like more cores ...
My own home machine has 12 real cores (24 hardware threads), and was quite
cheap, too.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.d
belle code base.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
discontinued, so that the keyword ";" was
again free for this important combinator.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
ious steps forward, probably next
week.)
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On Sun, 29 Mar 2015, Makarius wrote:
* Configuration option "rule_insts_schematic" determines whether proof
methods like "rule_tac" may refer to undeclared schematic variables
implicitly, instead of using proper 'for' declarations. This historic
behaviour is s
is legacy mode just now, but the complete conversion
in AFP/aa0bd0c0cbb6 turned out rather small, indicating rare use of such
undeclared schematic variables in rule_tac etc.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On Thu, 19 Mar 2015, Larry Paulson wrote:
Within HOL-SPARK. Example attached.
Larry
On 19 Mar 2015, at 15:21, Makarius wrote:
I've never seen such *.prv files. Where are they coming from?
In Isabelle/e749a0f2f401 there is now a system option spark_prv, which is
off for the HOL-
&& cmd.span
== span =>
-chop_common(cmds, rest)
+ case (cmd :: cmds, (blobs_info, span) :: rest)
+ if cmd.blobs_info == blobs_info && cmd.span == span => chop_common(cmds,
rest)
case _ => (cmds, blobs_spans)
There are very few AFP tests on http://isabelle.in.tum.de/reports/Isabelle
in recent weeks/months.
Is there anybody who understands how that works, to look what is the
situation?
Makarius
___
isabelle-dev mailing list
isabelle
On Wed, 18 Mar 2015, Larry Paulson wrote:
Sorry, I overlooked this due to the many untracked files of the form
*.prv. Wouldn’t it make sense to add this pattern to our .hgignore file?
I've never seen such *.prv files. Where are they coming from?
Normally the Isabelle source space is consider
On Mon, 16 Mar 2015, Makarius wrote:
On Mon, 16 Mar 2015, Makarius wrote:
I have reworked this substantially in various changesets leading up to
5d0c539537c9. It is surprising how much time can be spent on such
details.
Now there is even some semantic completion, to propose a theory
On Tue, 17 Mar 2015, Larry Paulson wrote:
I’ve pushed a correction to that particular problem.
That version f41a2f77ab1b looks fine.
I’ve no time to verify that there are no further problems. Sorry again.
New further problems emerge in 5b762cd73a8e: total existence failure due
to missing
blem might be an untested merge by Larry, but I did not make more
detailed tests to prove that hypothesis.
What is also odd: http://isabelle.in.tum.de/reports/Isabelle does not show
any activity nor results of testing. Maybe the mira service is down?
Makarius
On Mon, 16 Mar 2015, Makarius wrote:
I have reworked this substantially in various changesets leading up to
5d0c539537c9. It is surprising how much time can be spent on such details.
Now there is even some semantic completion, to propose a theory name that
fits to the file name, in the
On Thu, 5 Mar 2015, Makarius wrote:
I will try to pick up this old thread soon for the coming release. The
problem is a consequence of various "improvements" done elsewhere. I did
not make any attempt to change that yet, since I have already a better
idea to handle the file
description:
more type class instances
The error message of the NSA "transfer" proof method is a bit obscure.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinf
mprovement of that aspect in the
coming release. As we are moving towards it in Apr/May 2015, it will need
extra sharp eyes watching out for such fine points.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tu
her mailing list, but there might be
other experts over there.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
it once more.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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
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 changes on resolve_tac
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, but it
with Dan Matichuk to have a first public appearance of
Eisbach that admits users outside the original research group (i.e.
the critical move from "publication quality" to "production quality").
Makarius
___
isabe
d that. Proper locale_deps
visualisation has already been pointed 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://mailmanbr
the name
space, or all 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
s Isabelle symbols.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
update
of jedit itself.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
lize the semicolon style (and other styles 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
On Sat, 17 Jan 2015, Makarius wrote:
Attentive readers of incoming changesets might have noticed the recent
improvements of the Graphview component, which was a not-quite-working
student project from some years ago.
As of Isabelle/32b162d1d9b5 it is already quite usable, although a few
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
execution times: have those theories really been 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&quo
E_HOME_USER/jedit directory?
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
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
of locally generated types, to eliminate this potential
of surprise.
Makarius
http://stop-ttip.org 1,235,909 Pa
ry version.
Makarius
http://stop-ttip.org 1,235,896 Participants
___
is
ince there is now IDE support for the latter,
and people tend to get confused by that as can be seen here:
http://lists.inf.ed.ac.uk/pipermail/polyml/2014-December/001497.html
Makarius
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
I’ll have a look at changing the ROOT file, the development mode for the
AODV entry is mostly over anyway, so I might just remove the additional
sessions.
Thanks. I am looking forward to run again at full speed. I am also about
to get some more cores within the next few days.
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
>
ost update on shutdown.
Makarius
https://stop-ttip.org/1,120,204 people so far
___
ally become a certain mode of using
PIDE, but without any add-on features such as -g AFP.
Makarius
https://sto
n".
Z3_NON_COMMERCIAL="yes"
You can remove that and use option preferences instead, e.g. see
Isabelle/jEdit plugin properties: Isabelle / General / Miscellaneous Tools
/ Z3 Non Commercial.
Makarius
---
is more difficult than it
seems at first sight --- depending on the application and its ambition.
In Isabelle/jEdit there is Token_Markup.edit_control_style to apply
\<^sub> or \<^sup> or \<^bold> to some text selection, taking into a
ple need
them occasionally (using -d DIR in "isabelle build" or "isabelle jedit").
Makarius
http://stop-ttip.org 1,063,743 people so far
-
hting
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.
in map2 --
these ML combinators for 2-case are relevant for the Pure bootstrap
process, but remain in use for other tools and packages.
Makarius
http://stop-ttip.org 9
heory name space problems preventing that.
Makarius
http://stop-ttip.org 946,179 people s
and what not.)
Makarius
http://stop-ttip.org 927,552 people so far
On Mon, 3 Nov 2014, Timothy Bourke wrote:
* Makarius [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 init
the vicinity of resolve_tac with proper
context recently, but it will require more time to revisit really ancient
parts of the system, not to say ancient habits.
Makarius
htt
Isabelle/ML. Using Isabelle/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
On Mon, 3 Nov 2014, Timothy Bourke wrote:
* Makarius [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 init
eforms that are in the
pipeline for a long time by keeping your sources in a more up-to-date
state.
Makarius
http://stop-ttip.org 777,443 pe
rself" name some decades ago. How do
you feel about it being called "ap2" or "apply2"?
Makarius
http://stop-t
5e1cce7ace3 with follow-up changes until
5b7a9633cfa8.
The old header command has a very long history, which demanded 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.
the TTY loop and has
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, fo
On Sat, 18 Oct 2014, Makarius wrote:
Back to the canonical question about "remainig uses of Proof General". After
talking to many people at VSL 2014 Vienna (July 2014) and in the months
afterwards, my conclusion is that nothing is left to hold us back.
So I am leaving a time win
. 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 p
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.
no longer retricted to
applications in $ISABELLE_HOME/src/Doc/.
In ac4f764c5be1, I have already reverted your change 3094b0edd6b5.
Makarius
801 - 900 of 2785 matches
Mail list logo
