*** Prover IDE -- Isabelle/Scala/jEdit ***
* Dockable window "Find" provides query operations for formal entities
(GUI front-end to 'find_theorems' command).
This refers to Isabelle/90edb0669845. The main point here is the concept
of "query operations" behind the scenes. It allows to integrate one-shot
print commands into the asynchronous/parallel document model. The GUI
panel then looks mostly conventional, but with some fine points in the
semantics: the user does not have to wait for start nor finish of the
query. It is all flowing in timeless/stateless space.
The panel should be basically usable, although some fine points are still
expected to show up. I am also curious to see what the student by Fabian
will deliver in approx. 10 days. We might brush up the GUI further, based
on this project.
Anyway, what is the purpose of the find_theorems rem_dups / with_dups
option? I have made a tooltip that says "Allow duplicates in result
(faster for large theories)", although I am unsure if this is correct.
The result with duplicates is quite different, i.e. not sorted according
to the usual heuristics.
Is this special "Duplicates" treatment still relevant? Already for
Isabelle2013 I've put some Par_List.map combinators in place, both for
filter evaluation and pretty printing of the result. Can anyone with
access to secret benchmarks try how well this crunches on 8 or 16 cores?
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
