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.
Last updated: Nov 07 2025 at 16:23 UTC