Email Gateway (Aug 23 2022 at 08:42): Email Gateway (Aug 23 2022 at 08:42):From: huch@in.tum.de
Hi everyone!
As part of my master's thesis I've built a search engine for theory
content in Isabelle and the AFP.
Try it out here: search.isabelle.in.tum.de
<https://search.isabelle.in.tum.de>
Status is still a bit WIP, but all features should be working.
All feedback is much appreciated! Especially filling out this short (< 5
minutes) survey <https://forms.gle/mPaResj2EfoXmVpH8> would be awesome.
Fabian Huch
Email Gateway (Aug 23 2022 at 08:46):From: huch@in.tum.de
Thank you for your interest in the tool! Those are very good questions.
I'll answer them in detail:
Is there an Isar command associated with the tool (i.e. something
similar to find_theorems)?
No, currently not.
Does there exist a public Isabelle/ML interface associated with the
tool, i.e. something that would enable the users of the Isabelle/ML
infrastructure to (easily) define queries programmatically when
working on the development of other tools?
There exists a scala interface for user-defined queries (see the
repository for details: https://github.com/qaware/isabelle-afp-search),
though you'd have to build the search index first (or download a
pre-build one).
Also, there is a REST interface deployed to which you can simply send
queries programatically (see API doc under
search.isabelle.in.tum.de/docs), without building an index yourself.
If the answers to 1 and/or 2 are negative, are there any plans to
provide an Isabelle/ML interface and/or an Isar command for this tool?
The tool has been developed with integration into Isabelle in mind, but
right now integrating it into isabelle is not in my scope.
Is the code for the tool going to be added to the AFP at some point in
the future?
Not quite sure if I understand what you mean with 'Added to the AFP' - A
link will probabily added isa-afp.org site, if that's what you mean.
Also, I have some critical feedback about the survey (not the tool).
The questions "How intuitive was the user interface?" and "What is the
likelihood you will use the tool in the future?" have the comments
"very intuitive" and "very likely" near score "1". However, "How
useful was the tool for you?" does not have any comments around the
scores. Should the users of the survey assume that "1" is "very
useful" and "5" is "not useful at all"? Personally, I find this
slightly counter-intuitive.
Thank you for the heads-up, that is of course a bug. I re-added the
scale there.
If you have further questions, please let me know!
Last updated: Apr 26 2024 at 01:06 UTC