Email Gateway (Aug 18 2022 at 16:18): Email Gateway (Aug 18 2022 at 16:18):From: grechukbogdan <grechukbogdan@yandex.ru>
Dear members of Isabelle group
Thank you for giving me so much attention during my trip to Munich. It was a great pleasure to visit you, to have useful discussions, and a possibility to ask questions.
However, as it often happens with research, the more you know, the more questions arise. So, I will continue to ask these questions via the mailing list.
It was mentioned by Johannes, that Multivariate Analysis becomes too big, and thus should be moved to the archive of formal proofs. I can easily use theories from the archive by downloading them, placing in my working folder, and import. For example, I can download the latest entry Binomial-Heaps, import BinomialHeap.thy, wait 1 minute, and then use it. If, however, I close and open emacs, I should again wait 1 minute to import BinomialHeap.thy (because the system will execute it again).
Now, if a big theory like Multivariate Analysis is moved to the archive, I will need, say, 30 minutes to import it (because the system will need to execute the whole entry). When I close and open emacs, will I need to wait 30 minutes again? Clearly, this is not convenient. In contrast, now I build the image with Multivariate Analysis once and then just use it.
I remember somebody mention that I can build intermediate images during my work, is this a correct solution here? If so, could you please explain in detail how to do this or point me pages in the documentation where this is explained.
But, if the correct thing to do will be download Multivariate Analysis from the archive and build image with it, why not make the user's life easier and allow to download a version of Isabelle with Multivariate Analysis and just run “./build -m HOL-Multivariate_Analysis HOL” as it is now? If you don't want Isabelle to be too heavy for non-mathematical users, I would imagine too possibilities for download – Isabelle Light and Isabelle Full. Moreover, why not Isabelle Full to contain all the formalized mathematics in Isabelle, including the archive? (I would just let it to build overnight). Prof. Nipkow mentioned some maintainence issues, but in any case theories from the archive should be maintained and updated with every version of Isabelle.
Sincerely,
Bogdan
Last updated: Nov 21 2024 at 12:39 UTC