some dummy data item is retrofitted to
typedefs that are not full quotient types. Couldn't the Quotient_Info
lookup do this on the spot as a fall-back? Or is there anything special
with full declarations and morphisms here?
Makarius
On Tue, 29 Nov 2011, Ondřej Kunčar wrote:
It seems that the compilation of IsarRef is broken. I've got the following
error with the 45669:06e259492f6b changeset:
~/tmp/isabelle-dev/doc-src/IsarRef ../../bin/isabelle make
Running HOL-IsarRef ...
HOL-IsarRef FAILED
It should work after
switched my default Scala version to 2.8.2,
although 2.8.1 and 2.9.1 should work as well (2.9.x still has a few minor
problems notably with the Console).
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https
/
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
):
example
begin
datatype foo = Foo | Bar foo
definition ...
lemma ...
end
This would merely manage the name spaces, to keep the typical many
variants of similar examples disjoint. Currently one needs workarounds
like foo, foo', foo'', foo\zeta etc.
Makarius
attached to the local context before printing.
There are more ways to do it, if slightly different functionality is
required. E.g. see the more advanced Proof_Syntax.proof_syntax or
Nitpick_Model.add_wacky_syntax, although this is heavy gear.
Makarius
On Wed, 30 Nov 2011, Makarius wrote:
This concerns Isabelle/3d6ee9c7d7ef:
Adding a global constant Quickcheck_Exhaustive.unknown with rather generic
notation ? to main HOL is a bit dangerous. The name unknown is also a
candidate for hide_const (open).
It appears to be used only for output
On Tue, 29 Nov 2011, Lukas Bulwahn wrote:
On 11/28/2011 10:41 PM, Makarius wrote:
On Mon, 28 Nov 2011, Lukas Bulwahn wrote:
many recent requests for adjusting the user-space behavior of
typedef
would then rather apply to quotient_type.
Also, I do not see the clear advantage how
* Renamed inner syntax categories num to num_token and xnum to
xnum_token, in accordance to existing float_token. Minor
INCOMPATIBILITY. Note that in practice num_const etc. are mainly
used instead.
This refers to Isabelle/c7a13ce60161.
Makarius
On Thu, 1 Dec 2011, Jasmin Christian Blanchette wrote:
Hi all,
I just pulled and updated (hg pull -u) from the main repository and got these
strange warnings:
Fügte 118 Änderungssätze mit 572 Änderungen zu 411 Dateien hinzu
warning: detected divergent renames of src/Pure/General/markup.ML
.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
The following update of the jedit_build component is not essential, but it
makes things work for Java 1.7:
http://www4.in.tum.de/~wenzelm/test/jedit_build-20111217.tar.gz
See also
http://isabelle.in.tum.de/repos/isabelle/file/3d0416135efb/src/Tools/jEdit/README_BUILD
Makarius
).
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Due to the re-introduction of 'a set as proper type constructor, change
4c629115e3ab in src/HOL/Tools/Meson/meson.ML makes unfold_set_const_simps
vacuous.
A brief inspection suggests that the corresponding unfold_set_consts
configuration option is now also obsolete.
Makarius
'...'
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
:
Replaced + and * on sets by \oplus and \otimes, to avoid clash with
definitions of + and * on functions.
This is a result from inspection of hg log -u berghofe -r
Isabelle2007:Isabelle2008. I have already reverted a few more obvious
things in c296c75f4cf4.
Makarius
production quality releases and arbitrary snapshots diluted. Some users
might even think that a snapshot is always the latest and greatest thing,
while in reality it ages much faster than proper releases.
Makarius
___
isabelle-dev mailing list
. How about the many
variations on Predicate_Compile, code generator etc?
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On Wed, 4 Jan 2012, Makarius wrote:
On Wed, 4 Jan 2012, Lawrence Paulson wrote:
It seems to me that we owe users an announcement on the mailing list so
that they know that this is coming. They can then download a development
snapshot to see what it will look like.
Coping
this would be not very informative.
I've started this thread merely to point out that the NEWS should tell
more explicitly how to do the porting, and avoid the known pitfalls.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https
to simplify
deployment. I am not sure how much priority to apply to this painful
non-free stuff right now.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
)
That is probably a bit too exotic to expect NEWS to say what needs to be
done. Nonetheless I am curious about the reason of this failure.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman
/f363e5a2f8e8/src/HOL/HOLCF/IsaMakefile
but the old HOLCF version probably has diverged from the HOL one already.
(Makefiles are hard to maintain anyway.)
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https
On Wed, 11 Jan 2012, Makarius wrote:
On Wed, 11 Jan 2012, Lukas Bulwahn wrote:
I bisected the failure further on my local machine and it turns out it is
related to the changeset
changeset: 46143:463b594e186a
user:wenzelm
date:Fri Jan 06 20:18:49 2012 +0100
summary
. x : ?A) (%x. x : ?B)) =
inf (%x. x : lists ?A) (%x. x : lists ?B)
The recent change 1898e61e89c4 (berghofe) might be related. Stefan should
know what he had in mind.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https
On Wed, 11 Jan 2012, Stefan Berghofer wrote:
If you look at the version of the tutorial available on the Isabelle
web page (p. 141)
http://isabelle.in.tum.de/dist/Isabelle2011-1/doc/tutorial.pdf
you will see that it has already been broken for some time, the only
difference being that set
language out
there is or has to be canonical in that sense, although it would do them
good.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
. pred thing stemming from coinductive_set
deadlocked further above.
An expert of having a set-back should know what to do here.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de
whatever oddities they observe. This is how
things can get ironed out eventually.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On Fri, 13 Jan 2012, Makarius wrote:
But there is another problem with JinjaThreads right now:
Isabelle/d43ddad41d81
AFP/3dcc6b9eae2b
thys/JinjaThreads/Framework/FWDeadlock.thy line 251:
blast does not terminate and fills up memory
It looks like another set vs. pred thing stemming from
, and make it
easier to get into a problem than usual.
Anyway, I am on travel in the next 3 weeks ...
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
the reason why it is less accessible in the Prover IDE --
due to lack of Isabelle/Isar transaction context.
Isabelle/jEdit provides a Raw Output panel for such physical process
output, which is a bit awkward but not more than going back to TTY.
Makarius
On Thu, 12 Jan 2012, Johannes Hölzl wrote:
The pages faq.html, community.html and projects.html are moved to the
wiki.
The community.html used to have the important information about the
Isabelle mailing lists. Since users of wikis and mailing lists are often
disjoint, having that now on
On Fri, 17 Feb 2012, Christian Sternagel wrote:
Dear Developers,
I find it slightly odd to get warnings like
### Legacy feature! Old 'axioms' command -- use 'axiomatization' instead
in places like HOL.thy. The reason is that (at least for me) this theory is
the first place to look how
versions explicitly on
isabelle-dev.)
Looking a bit in the history ofJinjaThreads the french option is
fluctuating a little back and forth, without any explanations.
Here is another interesting changeset:
changeset: 663:11e88e5f18d4
user:makarius
date:Tue Sep 09 18:19:23 2008
occasional races when
switching to another editor buffer quickly.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
context is avoided.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On Fri, 24 Feb 2012, Makarius wrote:
It is also possible to have .hg/hgrc specific to individual repository
clones. So if testboard users are instructed to augment only that hgrc
with the evil option once and for all, the problem of getting used to
evil command lines in a different context
in a way
that big mistakes don't happen (which we managed very well in recent
years).
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
of Mercurial the hgrc is a local thing,
which is never cloned. (Never versions might have introduced other
solutions more recently.)
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de
for many years.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
is unreliable), I realized again that one could
somehow make non-local sockets part of the game by default. This is
particularly relevant for Swing applications, because X11 display
forwarding does not really work here.
Makarius
___
isabelle
).
After 3.4 weeks vacation in Marokko in Jan/Feb and 2 weeks working through
my mail folders like crazy, I still have issues in the pipeline that need
to be reanimated. I also need to figure out which essential things of the
Prover IDE can make it into the release ...
Makarius
of ~~/doc-src/TutorialI/CTL/CTL.thy)
This might be related to some recent complete_lattice changes that I've
seen passing by.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman
problem.
Theory imports are managed by the editor front-end, but uses by the
prover. To get this really right eventually, tools need to load auxiliary
files relatively to the master theory source, e.g. via
Thy_Load.load_file, but some details are still to be settled.
Makarius
On Sun, 4 Mar 2012, Cezary Kaliszyk wrote:
Makarius once suggested an antiquotation, that does something like
'print_theorems'. I have not investigated how to implement one?
Pretty printing into latex source is not a big deal, if you are satisfied
with regular multiline output in the display
On 6 Mar 2012, at 12:00, Lawrence Paulson wrote:
I remember when you could build a logic by typing “isabelle make, and
if an error occurred somewhere, it would terminate with an error
message.
I am trying to make textual changes now, and I find that “isabelle
make simply hangs. if I
. Nonetheless, I've already had some success in
disentangling concurrent changes on latex sources, where several people
were messing around (not on the Isabelle repository :-).
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https
). I did not see any of the teething problems
from 3 years ago (Mercurial 1.0) on Mac OS recently. (I using both Mac
OS X Snow Leopard and Ubuntu 10.04 LTS regularly).
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https
Google provides this mirror of the isabelle-users mailing list:
http://groups.google.com/group/fa.isabelle/about
Does anybody understand how this works? Google says This is a Usenet
group.
Also interesting: the rough statistics about traffic since 2000.
Makarius
-1, and JRE/JDK
1.6 or 1.7 from Oracle, probably also OpenJDK 1.7 (not 1.6!).
isatest uses jedit_build-20120313 and scala-2.8.2.final to produce the
development snapshot http://isabelle.in.tum.de/devel/
Makarius
___
isabelle-dev mailing list
On Mon, 12 Mar 2012, Makarius wrote:
There is still no proper support for redefining Isar commands in the
running session. So I would say the above is the normal consequence of
redefining 'function' in one theory while another one already reparses
an older version of it. Thus the resulting
, you can now also use Isabelle/jEdit for ZF ...
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
a casualty of recent changes with 'a set, lattice,
inductive_set, numerals or similar.
This part of the session can be checked easily with only 2 cores and a few
GB of memory. So maybe someone who feels responsible for recent changes
in main HOL could take a look at it.
Makarius
that mainly
addresses the Isabelle development process.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
in this respect, without any reforms yet.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
is
Hypersearch in the regular Find dialog, or the Firefox-style search bar.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
love to see theory sources being loaded via ssh or
http at some point ...
In the example above, do you have a literal ~ or its expansion by the
operating system shell? It is more robust to use $HOME in shell
scripts if you mean home.
Makarius
On Wed, 21 Mar 2012, Christian Sternagel wrote:
Is it just me or is Isabelle/jEdit really much faster than
ProofGeneral/emacs when loading theories? (Maybe this is due to some
other difference between Isabelle2011-1 and the repo version; I only use
emacs if I have to stick to Isabelle2011-1.)
On Fri, 16 Mar 2012, Florian Haftmann wrote:
* The set story:
https://isabelle.in.tum.de/community/Having_%27a_set_back Not everything
mentioned there is an ultimate need, but we should strive to pick as
many fruits as we can from the set type constructor – the more likely
this will
build system (based on Isabelle/Scala), the user can refer to sessions
robustly without tinkering IsaMakefiles or funny search paths.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de
On Sat, 24 Mar 2012, Ondřej Kunčar wrote:
The constant is now hidden.
Just two more things:
* Now means Isabelle/e64ffc96a49f -- The issue of proper references to
changesets is a running gag on isabelle-dev already. If you want, you can
make it the discriminating aspect between the two
component yet).
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
. The critical spot might
be a definition of datatype or datatype realizer.
This needs further investigation. Do you have any ideas on the spot?
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de
-Imported (cf. 9f82058567ce)
HOL-Quickcheck_Examples (cf. 879f5c76ffb6)
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
in the Linux bundle. Here you need to set
JAVA_HOME *outside* of the Isabelle environment or ISABELLE_JDK_HOME
*inside* as settings.
I am in the course of refining that again soon ...
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https
/Numbers.thy)
Brian should know what to do here.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
.x release candidates. Both should also work quite well already.
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 Wed, 28 Mar 2012, Ondřej Kunčar wrote:
After a long discussion during a lunch break we decided to use
.rep_eq. I will also change _rsp to .rsp. What about _def?
Should I change it to .def as well? _def seems to be a
inconsistency, I guess because of historical reasons. Should new
packages
have done via the Isabelle repos some years ago.
This does not mean that I have any concrete proposals in the pocket, let's
say about using a really really good issue tracker service on some open
source hosting platform -- if it exists at all.
Makarius
?
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
desaster.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On Fri, 30 Mar 2012, Lukas Bulwahn wrote:
On 03/30/2012 11:24 AM, Makarius wrote:
On Fri, 30 Mar 2012, Lukas Bulwahn wrote:
The webpage on the Isabelle (community) wiki,
https://isabelle.in.tum.de/community/Administration_of_the_isatest_facilities,
summarizes the agreement of this thread
it.
See also http://isabelle.in.tum.de/repos/isabelle/rev/dd04c8173bb2
for the traditional isatest cron jobs.
I did not touch Admin/mira.py yet, because I don't understand the
implications. It would also require another restart of the main mira
server process.
Makarius
hours.
I've tried to reproduce it by hand, loading
Codegenerator_Test/Generate.thy into HOL-Library. It works for
polyml-5.4.1_x86_64-darwin and polyml-5.4.1_x86-darwin, but
polyml-5.3.0_x86-darwin does not seem to terminate.
Any ideas?
Makarius
messages are old-school TTY technology, and
in Proof General the channel for that gets easily overloaded so that the
user is switching into SPAM mode.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https
of GB are required, most notably AFP/JinjaThreads.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On Fri, 6 Apr 2012, Christian Sternagel wrote:
it seems as if a recent change (in the repo version; within the last 2
weeks, but I do not know exactly when) fixed the naming of type
variables inside instantiations.
There are various ongoing reforms (e.g. see changes leading up to
of this situation in Isabelle2011-1? Renaming
one of the theory files is an acceptable solution in this case?
Renaming one of the theory files (on your private copy) is the only
solution in contemporary Isabelle. It is acceptable, because it is just
one file here.
Makarius
On Thu, 29 Mar 2012, Gerwin Klein wrote:
On 29/03/2012, at 6:11 AM, Makarius wrote:
Who is the main responsible for isatest anyway? According to the
received customs it would be Gerwin, since he started the service many
years ago. (His shell scripts still mention SunOS.)
I still feel
Isabelle/a380515ed7e4 and AFP/53124641c94b produce the following error:
*** No code equations for one_word_inst.one_word
*** At command by (line 174 of afp-devel/thys/JinjaThreads/Common/BinOp.thy)
What needs to be done here?
Makarius
, and update
manuals to cover new things. (I am speaking to myself here as well.)
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
the years, I had occasionally
spent several hours or days (or rather nights) trying to disentangle
unclear situations for particularly odd changesets.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https
tool to Scala. Conceptually, the old graph
browser can still compete with newer things on the market, but with its
use of AWT from Java 1.1 that is hard to explain to end-users. (It is also
technically hard to integrate into contemporary Swing components.)
Makarius
is syntactically incorrect
and ill-typed.
At least I've managed to excite some jEdit experts for the \A Unicode
problem. Another one even started looking into proper right-to-left
type-setting, say for Arabic, but it is not going to happen soon.
Makarius
not the only
one who keeps an eye on incoming changes; there are often small issues
that need to be discussed.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle
smoothly.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On Fri, 13 Apr 2012, Makarius wrote:
On AFP I've also seen a machine default for fetch merges. This is the
canonical configuration for it:
[extensions]
hgext.fetch =
[defaults]
fetch = -m merged
I won't argue about the exact spelling of the merged, but it should not be
the machine
of the approach. That is object Graph part only.
How would a Java person solve the private constructor problem?
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle
had our joint discussion on the
browser projects: join the efforts of Stefan from 1996 and Markus Kaiser
from 2011.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo
to national
debts.
There might be some rough edges still in the implementation, which are
hopefully ironed out until the release.
Please report your experience with it.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https
to
many. The style of Isabelle/Scala is that of Isabelle, i.e. the best from
many decades of Isbelle/ML transferred to Scala in a reasonable way.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu
quite popular early for Isabelle/Mercurial experts. So
far I've never tried it myself.
I wonder if the more recent rebase extension would do similar things in a
more basic way. Are there any users of it?
Makarius
___
isabelle-dev mailing list
On Mon, 16 Apr 2012, Brian Huffman wrote:
Finally we have a mechanism similar to Section in Coq, a more
lightweight alternative to locales.
This is what Larry Paulson and Florian Kammüller actually started in
1998/1999 and eventually became the fully-featured locale + interpretation
system
is expected to increase a little,
without becoming too prominent. It is a useful add-on solution in the
backhand of package implementors.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu
On Tue, 17 Apr 2012, Lawrence Paulson wrote:
I look forward to seeing some documentation on these increasingly
mysterious constructs… :-)
It is pretty close to the original concept of section that you've
introduced with Florian Kammüller in 1998/1999, so it is much more basic
than locales +
-algebra system. This would mean a
conceptual advance, not just a variation of old conventions. I.e. we
could overcome alternative syntax tables eventually.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https
applications they don't, as far as I can see. So
it looks like a candidate for garbage collection on the sources.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle
~ relcomp_unfold
In the time immediately before the relase (which is now) the NEWS should
reflect the perspective for end-users of the official stable system that
is delivered.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https
301 - 400 of 2162 matches
Mail list logo
