Stream: Beginner Questions

Topic: Making sense out of the sessions library

hmijail (Jul 20 2025 at 11:59):

The HOL theory library in the Isabelle documentation page goes to a list of sessions.
Let's say I am looking for the Finite_Map theory. How am I supposed to know that it's part of the HOL-Probability session?
The only way I have found to find documentation is google online and grep locally. This surfaces stuff, but in isolated patches that don't allow me to get any idea of a bigger picture.
Am I missing something?

Mathias Fleury (Jul 20 2025 at 17:23):

Finite_Map is in HOL-Library, not HOL-Probability

Mathias Fleury (Jul 20 2025 at 17:26):

and Isabelle has no policy to move things one at a time. So when "library"-like version enters HOL it is usually with everything in it

Mathias Fleury (Jul 20 2025 at 19:16):

You can see it in the AFP with the number of _More theories

hmijail (Jul 21 2025 at 00:20):

Huh... When I googled for Finite_Map, the result I got was in session HOL-Probability: HOL-Probability/HOL-Library.Finite_Map. I see now:

• that it's also in the HOL-Library session, where it makes more sense
• that one file can be reflected in 2 positions of the session hierarchy
• that the "HOL-Library" part of its name seems to mean another session (at first I assumed it was a filepath)

OK, so this all together hints at how to navigate sessions and search results a bit better... thank you.

Mathias Fleury (Jul 21 2025 at 04:33):

The issue is that an Isabelle session can only be built on top of one other session

Mathias Fleury (Jul 21 2025 at 04:34):

Until recently: you would usually pick the most important (slowest) one to avoid recompiling it each time you start the development

Mathias Fleury (Jul 21 2025 at 04:35):

(now you can declare in the ROOT file that some sessions should be known, so you do not have to recompile them each time... but it is not really merging several sessions and has weird side effects like you saw on Finite_Map)

Last updated: Aug 13 2025 at 08:30 UTC