Email Gateway (Mar 20 2025 at 10:52): Email Gateway (Mar 20 2025 at 10:52):From: Lawrence Paulson <lp15@cam.ac.uk>
This facility for locating theorems in theories that have not yet been loaded will be useful to many people. But it would be great to have some hints how to use it.
It looks like one has to build an index first, then launch the server.
isabelle find_facts_index HOL
isabelle find_facts_server -p 8080
open http://localhost:8080/find_facts#search?q=Hilbert
So this gives us an index for HOL, but could one make an index for all of HOL+AFP?
Larry
Email Gateway (Mar 20 2025 at 11:09):From: Fabian Huch <huch@in.tum.de>
On 3/20/25 11:51, Lawrence Paulson wrote:
This facility for locating theorems in theories that have not yet been loaded will be useful to many people. But it would be great to have some hints how to use it.
It looks like one has to build an index first, then launch the server.
isabelle find_facts_index HOL
isabelle find_facts_server -p 8080
open http://localhost:8080/find_facts#search?q=Hilbert
In general, yes; In the Isabelle release starting from Isabelle2025,
there is an index of the entire distribution already included, which you
launch with:
isabelle find_facts_server -p 8080 -o find_facts_database_name=isabelle
So this gives us an index for HOL, but could one make an index for all of HOL+AFP?
Certainly, and it could be included in future AFP releases.
Fabian
Last updated: Apr 17 2025 at 20:22 UTC