Re: [isabelle-dev] jEdit: tooltips don't have proper size
On Wed, 24 Oct 2012, Steffen Juilf Smolka wrote: It seems there is a little (but annoying) issue with the new tooltips in Isabelle/jEdit when using a font other than IsabelleText. I'm using the Source Code Pro font and the tooltips are always just a little too small so that part of the text is hidden/cut off. Of course an easy fix would be to go back to using IsabelleText... First the running gag on isabelle-dev: the new ... or the latest ... is ill-defined. You have to refer to *the* changeset of the repository version you are presently testing. Nonetheless, I can guess what you mean and to which version range it might refer: something close to my own latest version of my laptop, which is 8b50286c36d3. (This reference here is important for the mail archive of the list, because in some weeks or months nobody remembers what was current in the past.) These fine points of sizing the Rich_Text_Area are not fully worked out yet, and the next release is still many weeks ahead. I will take your observation is a slight increase of the priority to address it before the release, but this is not sure since many really important things still need to happen elsewhere. Concerning Source Code Pro font: I tried it some weeks ago when there was an announcement somewhere, but dismissed it rather quickly. On JVM/Linux its rendering quality appeared quite weak, and too many of our standard Isabelle symbols are missing. (This can be checked by opening $ISABELLE_HOME_USER/etc/symbols with UTF-8-Isabelle encoding.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] priority queues
On Wed, 24 Oct 2012, Steffen Juilf Smolka wrote: is there an implementation of priority queues in the isabelle library? This is off-topic for this mailing list, which is for things happening around the Isabelle development process. Unless you refer to a particularly emerging module in some inter-release repository version -- lets say you are build some add-ons as very early adopter -- everything concerning Isabelle/ML programming can be discussed on the main isabelle-users mailing list. To avoid further complication, here are some hints as if this would be isabelle-users (so I refer to the latest official release): http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2012/src/Pure/General/heap.ML http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2012/src/Pure/General/table.ML http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2012/src/Pure/General/graph.ML The (rarely used) Heap module gives you direct access to the minimum element of an ordered collection, which is maintained efficiently. The Table module is *the* workhorse for efficient organisation of ordered values (sets, maps etc.). Its derivative Graph is equally popular: it introduces additional dependencies over a table, often acyclic ones, but cyclic graphs are also supported. For example, in the Task_Queue implementation that underlies the Future library in Isabelle/ML, a graph with a suitable order on tasks is used as a priority queue with dependencies. You then take out the smallest element that does not have any dependencies. See also http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2012/src/Pure/Concurrent/task_queue.ML#l147 http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2012/src/Pure/Concurrent/task_queue.ML#l324 Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] priority queues
On Wed, 24 Oct 2012, Lukas Bulwahn wrote: I think priority queues are roughly ordered lists (the priority is the ordering). So, you could have a look at Pure/General/ord_list.ML The main virtue of Ord_List is that insert and merge are of the same complexity: linear. This is important in special applications like maintaining the hyps field of a thm efficiently, but in most other applications the linearity of insert is a performance trap. The balanced tree structure underlying module Table works better in general. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] priority queues
Am 27/10/2012 16:55, schrieb Makarius: On Wed, 24 Oct 2012, Steffen Juilf Smolka wrote: is there an implementation of priority queues in the isabelle library? This is off-topic for this mailing list, which is for things happening around the Isabelle development process. Unless you refer to a particularly emerging module in some inter-release repository version -- lets say you are build some add-ons as very early adopter -- everything concerning Isabelle/ML programming can be discussed on the main isabelle-users mailing list. Steffen is a sledgehammer code developer with Jasmin and this question is not appropriate for isabelle-users. Tobias To avoid further complication, here are some hints as if this would be isabelle-users (so I refer to the latest official release): http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2012/src/Pure/General/heap.ML http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2012/src/Pure/General/table.ML http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2012/src/Pure/General/graph.ML The (rarely used) Heap module gives you direct access to the minimum element of an ordered collection, which is maintained efficiently. The Table module is *the* workhorse for efficient organisation of ordered values (sets, maps etc.). Its derivative Graph is equally popular: it introduces additional dependencies over a table, often acyclic ones, but cyclic graphs are also supported. For example, in the Task_Queue implementation that underlies the Future library in Isabelle/ML, a graph with a suitable order on tasks is used as a priority queue with dependencies. You then take out the smallest element that does not have any dependencies. See also http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2012/src/Pure/Concurrent/task_queue.ML#l147 http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2012/src/Pure/Concurrent/task_queue.ML#l324 Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] priority queues
Thanks. I used an ordered list as a temporary solution, but now replaced it with a table to avoid linear complexity (when adding new elements to the queue). Steffen On 24.10.2012, at 17:26, Lukas Bulwahn bulw...@in.tum.de wrote: I think priority queues are roughly ordered lists (the priority is the ordering). So, you could have a look at Pure/General/ord_list.ML Lukas On 10/24/2012 05:21 PM, Steffen Juilf Smolka wrote: Hi, is there an implementation of priority queues in the isabelle library? Steffen ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isatest report [...]
On Wed, 24 Oct 2012, Jasmin Christian Blanchette wrote: So the last threee lines of the attachment are shown. Would it be possible to increase that to four? That way, we'd get the much more instructive Test for platform mac-poly64-M2 failed. Log file attached. [...] Unfinished session(s): Codegen Finished at Wed Oct 24 02:40:50 CEST 2012 2:12:57 elapsed time, 3:44:19 cpu time, factor 1.68 --- test FAILED --- Wed Oct 24 02:40:50 CEST 2012 --- macbroy6 See c163145dd40f, which accomodates this extra line produced by isabelle build. I am glad that I did not attempt to make its final status report human-readable by formatting it as a paragraph or similar. So plain Unix tail can operate on it like that. When I am back from vacation (15-Nov) I would like to do some further clear-out of some isatest features that are no longer relevant for its core business of testing and publishing test reports / statistics. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit: tooltips don't have proper size
First the running gag on isabelle-dev: the new ... or the latest ... is
ill-defined. You have to refer to *the* changeset of the repository version
you are presently testing.
Sorry, I'll keep that in mind.
Concerning Source Code Pro font: I tried it some weeks ago when there was
an announcement somewhere, but dismissed it rather quickly. On JVM/Linux its
rendering quality appeared quite weak, and too many of our standard Isabelle
symbols are missing.
I'm quite happy with the font on MacOS, and the missing symbols haven't been a
problem so far since I usually work in ML{* *}. By the way, the tooltips are
really a great help when programming!
(This can be checked by opening $ISABELLE_HOME_USER/etc/symbols with
UTF-8-Isabelle encoding.)
Ah, good to know!
Steffen
On 27.10.2012, at 16:42, Makarius makar...@sketis.net wrote:
On Wed, 24 Oct 2012, Steffen Juilf Smolka wrote:
It seems there is a little (but annoying) issue with the new tooltips in
Isabelle/jEdit when using a font other than IsabelleText. I'm using the
Source Code Pro font and the tooltips are always just a little too small so
that part of the text is hidden/cut off. Of course an easy fix would be to
go back to using IsabelleText...
First the running gag on isabelle-dev: the new ... or the latest ... is
ill-defined. You have to refer to *the* changeset of the repository version
you are presently testing.
Nonetheless, I can guess what you mean and to which version range it might
refer: something close to my own latest version of my laptop, which is
8b50286c36d3. (This reference here is important for the mail archive of the
list, because in some weeks or months nobody remembers what was current in
the past.)
These fine points of sizing the Rich_Text_Area are not fully worked out yet,
and the next release is still many weeks ahead.
I will take your observation is a slight increase of the priority to address
it before the release, but this is not sure since many really important
things still need to happen elsewhere.
Concerning Source Code Pro font: I tried it some weeks ago when there was
an announcement somewhere, but dismissed it rather quickly. On JVM/Linux its
rendering quality appeared quite weak, and too many of our standard Isabelle
symbols are missing. (This can be checked by opening
$ISABELLE_HOME_USER/etc/symbols with UTF-8-Isabelle encoding.)
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
