Re: [isabelle-dev] Proposing extensions to the Isabelle library?
Hi Alessandro, Is there any plan to make things in the library more uniform (one way or the other)? Is there a preference for new type classes should be developed (purely syntactic or with assumptions)? well, there is no big masterplan. Usually things evolve: somebody thinks about an extended or more fine-grained hierarchy and thinks how to accomplish things without breaking more than necessary. Personally, I like syntactic classes because they are more modular. For example, in the library extensions that I sent the other day, the definition of type class finite_lattice_complete would be perhaps slightly cleaner if bot and top were syntactic classes like Inf and Sup. Just my 2 cents. I.e. something like class bot ~ class order_bot class top ~ class order_top class bot = fixes bot :: 'a class top = fixes top :: 'a Could make sense. The question is whether somebody is willing to undertake this change. If you would consider this, you find the first clues at http://isabelle.in.tum.de/repos/isabelle/file/c5e0073558f3/README_REPOSITORY. Get back here if questions remain. Note that currently we are heading towards a next release in January or February, and time might be too terse to polish and incorporate a change like the one sketched above. Hope this helps, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Max threads Sledgehammer
On 07/01/2013 17:49, Stefan Berghofer wrote: You could certainly hit limits on memory for stacks with a large number of threads particularly if the default stack size is large. What does ulimit -s say? You could try setting that smaller. ulimit -s says 102400 This is surprisingly large. That works out at 100Mbytes per thread, assuming that this is k as on my Debian machines. My machines show 8192 here. Poly/ML needs only a small space on the C stack so maybe it should set the stack size explicitly when the threads are created. David ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Semantics of hide (open)
Maybe there is some confusion what the semantics of hide (open) is exactly supposed to be. But since the current state of affairs gives no tool at hand to resolve situations as sketched above, this is a serious obstacle. The hide feature was added as a temporary workaround for the lack of proper scope management many years ago. In the meantime we managed to get a bit further with the naming + binding = name + accesses equation, but not with scoping of theories and contexts. I still would like to see that appear eventually, and hide become obsolete then. (It will mean that names behave uniformly, i.e. different categories like const and fact need to agree in their visibility.) That indeed would be the right thing. In the meantime I found out that I do not need function/primrec anywayin my particular situation, so the »serious obstacle« has disappeared. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Purpose of additional HOL images
Am 07.01.2013 13:06, schrieb Makarius: This is a left-over from the isabelle build reform from last summer: Do the additional HOL images still have a purpose? Notably: HOL-Base HOL-Plain HOL-Main If it is just for experimentation, these session can be easily provided by 1 line each in $ISABELLE_HOME_USER/ROOT I'm still using these, but with jedit getting better and better and $ISABELLE_HOME_USER/ROOT I can well live without. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Purpose of additional HOL images
This is a left-over from the isabelle build reform from last summer: Do the additional HOL images still have a purpose? Notably: HOL-Base HOL-Plain HOL-Main If HOL-Plain vanished, the same could apply to Plain.thy itself. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jedit: zoom with cmd++
The problem is still there on Mountain Lion with an American keyboard.
However, rebinding the kebyoard shortcut locally as you suggested does the
trick - thanks for the tip!
Here is an ugly hack (based on the KeyEventDemo you provided) that would solve
the problem:
KeyEvent e_ = null;
// pressing a key twice in 5 ms or less is probably impossible
final long eps = 5;
/** Handle the key pressed event from the text field. */
public void keyPressed(final KeyEvent e) {
final boolean process = e_ == null || e.getKeyCode() != e_.getKeyCode()
|| (e.getWhen() - e_.getWhen()) eps;
e_ = e;
if (process) {
displayInfo(e, KEY PRESSED: );
}
}
Steffen
On 07.01.2013, at 11:07, Makarius makar...@sketis.net wrote:
On Sat, 22 Dec 2012, Makarius wrote:
On Wed, 19 Dec 2012, Steffen Juilf Smolka wrote:
in a39250169636, it is possible to increase/decrease the font size in jedit
with cmd++/cmd+- on MacOS (probably ctrl++/ctrl+- on other
plattforms) (nice feature!). However, pressing cmd++ increases the font
size twice on my machine (cmd+- works fine).
That was one such convenience that I managed to get working after 20min
Windows and Linux, followed by 2 weeks of tinkering on Mac OS X. But that
is not finished yet, and there are remaining problems to treat CTRL, ALT,
COMMAND modifiers properly: it can cause duplication or triplication of key
events.
See also the mail thread on Mac OS X support on Oracle Java 7 that Fabian
Immler has started recently
http://sourceforge.net/mailarchive/message.php?msg_id=30165793
It touches some of the internal issues, including a slightly odd workaround
by myself to modify an older workaround to make it half-working again under
Java 7.
This needs more systematic investigation, by instrumenting the jEdit sources
to produce detailed traces for all critical points where the MacOSX specific
key handling happens. Then it needs to be compared for Java 6 vs. Java 7,
to reconstruct the ideas behind it, which nobody seems to remember on
jedit-devel.
I've spent yet more time on the Mac OS X keyboard problem, which resulted
in change 76ae4e6318fb so far -- you will need the jedit_build update from
the later e7b2cfcef94c to try it yourself.
This now works on all machines I had tried at that point: Windows + Linux +
Mac OS X Mountain Lion, all with German keyboard. Trying it again with Mac
OS X Snow Leopard and English keyboard, I still see the triplication of
COMMAND-EQUALS for the Meta + key, though. Testing that with the low-level
Java key handler that is attached here, it actually shows 3 KEY_PRESSED
events produced by jdk-7u9 on that machine.
So we should blame Oracle or Apple for that ...
If someone comes up with a workaround nonetheless, I will look at it once
more.
Note that by rebinding the keyboard shortcut yourself locally, it will turn
the 3 keystrokes happily into just one editor action.
MakariusKeyEventDemo.java
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
