Stream: General

Topic: ✔ Limit superior


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Lukas Stevens (Nov 28 2021 at 20:19):

Wolfgang Jeltsch said:

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?

Yes.

view this post on Zulip 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.

view this post on Zulip Wolfgang Jeltsch (Nov 28 2021 at 20:30):

Lukas Stevens said:

Wolfgang Jeltsch said:

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?

Yes.

Well, no, according to Manuel’s statement and the experience I meanwhile gathered myself. :frown:

view this post on Zulip 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.

view this post on Zulip Wolfgang Jeltsch (Nov 28 2021 at 20:32):

No, HOL is already built. It wasn’t in older releases, but in Isabelle2021 it is.

view this post on Zulip Lukas Stevens (Nov 28 2021 at 20:33):

Interesting, that isn't the case on NixOS.

view this post on Zulip Wolfgang Jeltsch (Nov 28 2021 at 20:33):

Manuel Eberl said:

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.

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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Lukas Stevens (Nov 28 2021 at 20:46):

Wolfgang Jeltsch said:

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?

That is normal.

view this post on Zulip Wolfgang Jeltsch (Nov 28 2021 at 20:46):

Okay, this build has finished now, but it took almost half an hour.

view this post on Zulip Lukas Stevens (Nov 28 2021 at 20:46):

Wolfgang Jeltsch said:

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?

I think so.

view this post on Zulip 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?

view this post on Zulip Wolfgang Jeltsch (Nov 28 2021 at 20:48):

Lukas Stevens said:

Wolfgang Jeltsch said:

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?

I think so.

Which one, the first (I have to import Main) or the second (it is guaranteed to be provided).

view this post on Zulip 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?

view this post on Zulip 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 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?

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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Notification Bot (Nov 28 2021 at 21:05):

Wolfgang Jeltsch has marked this topic as resolved.


Last updated: Aug 15 2022 at 02:13 UTC