Yosuke Ito (Oct 20 2025 at 08:49): Yosuke Ito (Oct 20 2025 at 08:49):Is FindFacts down now?
I can't access
https://search.isabelle.in.tum.de/
Fabian Huch (Oct 20 2025 at 09:13):Thanks - is up again.
Yosuke Ito (Oct 20 2025 at 09:16):Thank you!
I got the access again.
Wenda Li (Oct 29 2025 at 18:55):Happened to notice that FindFacts is defaulted for Isabelle2024/AFP2024? Any plan to keep it update-to-date?
Yosuke Ito (Oct 30 2025 at 07:30):I hope it would be up-to-date. :-)
Fabian Huch (Oct 30 2025 at 08:00):Yes; however, we will switch to the Find_Facts now distributed with Isabelle. The switch will happen with the next release (Isabelle2025-1).
Fabian Huch (Oct 30 2025 at 08:02):What I would love to see is concept extraction (as demonstrated by the SErAPIS prototype) also integrated in Find_Facts, but so far nobody has stepped up to build this.
Fabian Huch (Oct 30 2025 at 08:02):(and I didn't have the time yet)
Yosuke Ito (Oct 30 2025 at 08:19):Oh, I am happy to hear that!
Wenda Li (Oct 31 2025 at 12:38):Fabian Huch said:
Yes; however, we will switch to the Find_Facts now distributed with Isabelle. The switch will happen with the next release (Isabelle2025-1).
Lovely to know! Just be curious: since Find_Facts can search through AFP, if Find_Facts is to be bundled with Isabelle distribution, will AFP be bundled with the distribution (so Find_Facts can search locally) or will Find_Facts check AFP over the Internet?
Wenda Li (Oct 31 2025 at 12:39):Fabian Huch said:
What I would love to see is concept extraction (as demonstrated by the SErAPIS prototype) also integrated in Find_Facts, but so far nobody has stepped up to build this.
Could be a student project :-) though long-term maintaining has always been a problem.
Fabian Huch (Nov 03 2025 at 07:58):Wenda Li said:
Fabian Huch said:
Yes; however, we will switch to the Find_Facts now distributed with Isabelle. The switch will happen with the next release (Isabelle2025-1).
Lovely to know! Just be curious: since Find_Facts can search through AFP, if Find_Facts is to be bundled with Isabelle distribution, will AFP be bundled with the distribution (so Find_Facts can search locally) or will Find_Facts check AFP over the Internet?
Only the library is indexed in the release. To search the AFP, you'll have to use the web version over the internet.
Fabian Huch (Dec 24 2025 at 12:54):Fabian Huch said:
Yes; however, we will switch to the Find_Facts now distributed with Isabelle. The switch will happen with the next release (Isabelle2025-1).
Find_Facts is now deployed in that version, and for AFP-2025-1 -- enjoy! Also feel free to DM me if you have feedback.
Yosuke Ito (Dec 24 2025 at 13:11):Thanks for letting me know.
For clarity, could you tell me what you mean by "Find_Facts now distributed with Isabelle"?
E.g., can we now use Find_Facts through Isabelle/jEdit?
Last updated: Dec 28 2025 at 02:03 UTC