Wolfgang Jeltsch (Nov 28 2021 at 18:39): Wolfgang Jeltsch (Nov 28 2021 at 18:39):Is there a definition for the limit superior operator in one of the sessions distributed with Isabelle? At least for lim sup X ≤ x, I could write something like max X (λ_. x) ⇢ x, but maybe there’s also a dedicated function lim_sup or so.
Manuel Eberl (Nov 28 2021 at 19:35):Yes! There is Limsup :: 'a filter ⇒ ('a ⇒ 'b) ⇒ 'b in HOL-Library.Liminf_Limsup, although it may be better to just import HOL-Analysis.Analysis (and set the session to HOL-Analysis by running JEdit with -l HOL-Analysis) since there may be more useful topological results that are in HOL-Analysis but not in HOL-Library.Liminf_Limsup.
Wolfgang Jeltsch (Nov 28 2021 at 20:18):Thanks a lot for the pointers.
Is HOL-Analysis pre-built, so that I can derive a session from HOL-Analysis instead of HOL, thus saving build time?
Lukas Stevens (Nov 28 2021 at 20:19):Wolfgang Jeltsch said:
Thanks a lot for the pointers.
Is
HOL-Analysispre-built, so that I can derive a session fromHOL-Analysisinstead ofHOL, thus saving build time?
Yes.
Manuel Eberl (Nov 28 2021 at 20:20):The first time you use the HOL-Analysis session, e.g. by running isabelle jedit -l HOL-Analysis, Isabelle will build a heap image and save it for future use.
Wolfgang Jeltsch (Nov 28 2021 at 20:30):Lukas Stevens said:
Wolfgang Jeltsch said:
Thanks a lot for the pointers.
Is
HOL-Analysispre-built, so that I can derive a session fromHOL-Analysisinstead ofHOL, thus saving build time?Yes.
Well, no, according to Manuel’s statement and the experience I meanwhile gathered myself. :frown:
Lukas Stevens (Nov 28 2021 at 20:32):I mean it will be prebuilt much in the same way as the HOL image is. You need to still build it once.
Wolfgang Jeltsch (Nov 28 2021 at 20:32):No, HOL is already built. It wasn’t in older releases, but in Isabelle2021 it is.
Lukas Stevens (Nov 28 2021 at 20:33):Interesting, that isn't the case on NixOS.
Wolfgang Jeltsch (Nov 28 2021 at 20:33):Manuel Eberl said:
The first time you use the
HOL-Analysissession, e.g. by runningisabelle jedit -l HOL-Analysis, Isabelle will build a heap image and save it for future use.
It’s just doing that for me. :smile: However, this means I won’t be able to readily use HOL-Analysis in automated builds on GitHub. Well, perhaps I need only few or even no bits from it in my (small) development.
Lukas Stevens (Nov 28 2021 at 20:35):If you use docker, you could create an image that builds HOL-Analysis first, or cache the relevant directory where the images are located.
Wolfgang Jeltsch (Nov 28 2021 at 20:37):Yes, I would use GitHub’s caching mechanism, which I’m actually already using, as I’m using the TeX Live Docker image and download and unpack Isabelle into it (the Isabelle Docker image doesn’t contain TeX). However, I would have to separately trigger the building of the HOL-Analyis heap image.
Wolfgang Jeltsch (Nov 28 2021 at 20:37):On a related note, do I have to import Main when importing HOL-Analysis.Analysis, or is it perhaps guaranteed that HOL-Analysis imports Main itself such that my development gets access to it as well?
Wolfgang Jeltsch (Nov 28 2021 at 20:45):And is it normal that, when building the HOL-Analysis session, Isabelle processes the various theories in relatively quick succession but then spends ages on HOL-Analysis.Analysis, consuming lots of CPU power?
Lukas Stevens (Nov 28 2021 at 20:46):Wolfgang Jeltsch said:
And is it normal that, when building the
HOL-Analysissession, Isabelle processes the various theories in relatively quick succession but then spends ages onHOL-Analysis.Analysis, consuming lots of CPU power?
That is normal.
Wolfgang Jeltsch (Nov 28 2021 at 20:46):Okay, this build has finished now, but it took almost half an hour.
Lukas Stevens (Nov 28 2021 at 20:46):Wolfgang Jeltsch said:
On a related note, do I have to import
Mainwhen importingHOL-Analysis.Analysis, or is it perhaps guaranteed thatHOL-Analysisimports Main itself such that my development gets access to it as well?
I think so.
Lukas Stevens (Nov 28 2021 at 20:47):Wolfgang Jeltsch said:
Okay, this build has finished now, but it took almost half an hour.
If I recall correctly HOL-Analysis benefits quite a bit from more memory. How much do you have?
Wolfgang Jeltsch (Nov 28 2021 at 20:48):Lukas Stevens said:
Wolfgang Jeltsch said:
On a related note, do I have to import
Mainwhen importingHOL-Analysis.Analysis, or is it perhaps guaranteed thatHOL-Analysisimports Main itself such that my development gets access to it as well?I think so.
Which one, the first (I have to import Main) or the second (it is guaranteed to be provided).
Wolfgang Jeltsch (Nov 28 2021 at 20:49):Lukas Stevens said:
If I recall correctly HOL-Analysis benefits quite a bit from more memory. How much do you have?
8 GB. But why does it spend about 80 % of its time on the last theory? Or didn’t it spend it on the last theory, but on some postprocessing, which, despite being the longest part, isn’t mentioned in the output?
Lukas Stevens (Nov 28 2021 at 20:49):Wolfgang Jeltsch said:
Lukas Stevens said:
Wolfgang Jeltsch said:
On a related note, do I have to import
Mainwhen importingHOL-Analysis.Analysis, or is it perhaps guaranteed thatHOL-Analysisimports Main itself such that my development gets access to it as well?I think so.
Which one, the first (I have to import
Main) or the second (it is guaranteed to be provided).
Sorry. HOL-Analysis should import Main already.
Lukas Stevens (Nov 28 2021 at 20:50):Wolfgang Jeltsch said:
Lukas Stevens said:
If I recall correctly HOL-Analysis benefits quite a bit from more memory. How much do you have?
8 GB. But why does it spend about 80 % of its time on the last theory? Or didn’t it spend it on the last theory, but on some postprocessing, which, despite being the longest part, isn’t mentioned in the output?
It launches into processing a lot of files and therefore proofs. And then does them all in parallel. This is why you get quickly to all files but it takes a while to finish them.
Lukas Stevens (Nov 28 2021 at 20:52):Proofs are using futures so you assume that you will get a proof at some point but you can process the rest of the proof (and file) already.
Manuel Eberl (Nov 28 2021 at 20:57):HOL-Analysis is a bit of a beast. On my machine, it takes something like 3.5 minutes, but I have a pretty beefy 24-core machine with 64 GB of RAM. Not sure whether CPU or memory is more of a bottleneck, but I think it definitely benefits from more cores. You might get away with just using HOL-Library.Liminf_Limsup though depending on what you need.
Notification Bot (Nov 28 2021 at 21:05):Wolfgang Jeltsch has marked this topic as resolved.
Last updated: Dec 30 2024 at 16:22 UTC