Email Gateway (Nov 13 2021 at 17:02): Email Gateway (Nov 13 2021 at 17:02):From: Peter Lammich <lammich@in.tum.de>
Hello,
I noticed that the Find_Theorems signature does not allow
to decouple the filtering of the theorems from the obtaining of the
unfiltered 'master' list of theorems.
This yields to me being forced to duplicate the filtering code, just to
filter over another source of theorems.
My use-case:
find_in_theorems <filters> in <fact_refs>
to search in explicitly stated theorems, e.g.
find_in_theorems "_+_" in algebra_simps
Problem:
Find_Theorems hides filtering, and only exposes combined function
that filters all theorems from context.
Proposed solution:
add filter_theorems and filter_theorems_cmd to FIND_THEOREMS
signature.
Background:
This has proved a very valuable tool for searching large fact
databases, such as Hoare-rules in my Isabelle-LLVM project.
Back then, I simply copy-pasted the code from find_in_theorems, but now
stumbled over the code-duplication again as some changes are necessary
to transition to 2021-1.
Please advise me if I should simply commit such a change (and hopefully
remember it on the next release, when I can use it from my tools (that
work on release versions)), or how to get such a change in, or if the
strong hiding is intentional, and I have to live with the code
duplication.
Email Gateway (Nov 13 2021 at 18:05):From: Makarius <makarius@sketis.net>
The isabelle-dev repository is already for Isabelle2022.
If you want anything in Isabelle2021-1, you need to show me a changeset
(result of "hg export" wrt. a clone of
https://isabelle.sketis.net/repos/isabelle-release).
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 14 2021 at 00:51):From: Gerwin Klein <kleing@unsw.edu.au>
I would welcome that change, happy for you to implement it (it doesn't have to be in 2021-1 from my side, I'll leave that up to you).
Cheers,
Gerwin
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 25 2021 at 15:53):From: Makarius <makarius@sketis.net>
This is still open. Is there anything you want to have changed in the
Find_Theorems signature?
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 25 2021 at 17:06):From: Peter Lammich <lammich@in.tum.de>
On Thu, 2021-11-25 at 16:53 +0100, Makarius wrote:
On 13/11/2021 19:05, Makarius wrote:
The isabelle-dev repository is already for Isabelle2022.
If you want anything in Isabelle2021-1, you need to show me a
changeset
(result of "hg export" wrt. a clone of
https://isabelle.sketis.net/repos/isabelle-release).This is still open. Is there anything you want to have changed in the
Find_Theorems signature?
not for the next release. It's not a regression of this release, and as
my schedule is tight, I'll live with the same hack for one more release
cycle, rather than trying to rush something now.
Peter
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Apr 20 2024 at 04:19 UTC