Email Gateway (Sep 14 2020 at 20:59): Email Gateway (Sep 14 2020 at 20:59):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,
I have a question about the "Submission Guidelines" for the AFP. At the
moment, the guidelines contain the following clause:
I would like to understand what would be the right circumstances for making
such exceptions. I am working on a certain applied formalization
study/library for Isabelle/HOL. However, it is becoming resource hungry,
and I find it convenient to break it into several smaller sessions while
working. However, I doubt that any of these smaller parts,
taken individually, are sufficiently interesting as independent AFP
entries. Is performance/development time optimization a sufficiently good
reason for allowing the submission of several sessions in one entry?
Lastly, in the future, should I direct the questions about the AFP to
afp-submit@in.tum.de, or is it better/acceptable to post such queries on
the mailing list?
Kind Regards,
Mikhail Chekhov
Email Gateway (Sep 15 2020 at 06:48):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
On 15 Sep 2020, at 04:58, Mikhail Chekhov <mikhail.chekhov.w@gmail.com> wrote:
The entry must contain a ROOT file with one session that has the name of
the entry. We strongly encourage precisely one session per entry, but
exceptions can be made.I would like to understand what would be the right circumstances for making
such exceptions. I am working on a certain applied formalization
study/library for Isabelle/HOL. However, it is becoming resource hungry,
and I find it convenient to break it into several smaller sessions while
working. However, I doubt that any of these smaller parts,
taken individually, are sufficiently interesting as independent AFP
entries. Is performance/development time optimization a sufficiently good
reason for allowing the submission of several sessions in one entry?
Usually not, because performance usually decreases with multiple sessions. Multiple sessions are nicer for interactive work during development, but once that phase is mostly over, a single large session can be usually be processed more efficiently by Isabelle than multiple small ones.
My own process these days is to have multiple sessions (when the development is large) until it has reached a maintenance phase, and then switch over. AFP submission is often (but not always) a good point for that.
Can I ask what the current processing time time is for the sessions you have?
Lastly, in the future, should I direct the questions about the AFP to
afp-submit@in.tum.de, or is it better/acceptable to post such queries on
the mailing list?
Both are fine. afp-submit is more private, but it’s good to have some of these questions here so they are more accessible.
Cheers,
Gerwin
Email Gateway (Sep 15 2020 at 15:53):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear Gerwin Klein/All,
Thank you for your reply.
Usually not, because performance usually decreases with multiple sessions.
Multiple sessions are nicer for interactive work during development, but
once that phase is mostly over, a single large session can be usually be
processed more efficiently by Isabelle than multiple small ones.Please accept my apologies for not describing the issue in my original
query in more detail. Indeed, I meant the performance during the
interactive development phase. I suppose I neglected the idea that the AFP
is meant to be used, primarily, for the publication of finished work,
rather than as a repository for stable releases. I have formed such a
biased impression because I noticed that several entries are updated quite
regularly (e.g. ODE, ZFC in HOL and category3/bicategories). However, the
answer that you have given, of course, is still applicable.My own process these days is to have multiple sessions (when the
development is large) until it has reached a maintenance phase, and then
switch over. AFP submission is often (but not always) a good point for that.This seems like a good and rather obvious solution to my problem.
Can I ask what the current processing time time is for the sessions you
have?I expect it to be somewhere between forty minutes and one hour on mid-range
modern laptop hardware, but it is growing quite quickly (sorry for a vague
order of magnitude estimate, it is difficult to be precise as it has been
some time since it was possible to build all relevant sessions
simultaneously). In any case, I am not yet certain whether I will ever wish
to submit any of this work to the AFP: I might opt-out for a solution
similar to https://isarmathlib.org/ (most of my own work is also,
primarily, set-theory-based library material).
Kind Regards,
Mikhail Chekhov
On Tue, Sep 15, 2020 at 9:47 AM Klein, Gerwin (Data61, Kensington NSW) <
Gerwin.Klein@data61.csiro.au> wrote:
On 15 Sep 2020, at 04:58, Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
wrote:The entry must contain a ROOT file with one session that has the name of
the entry. We strongly encourage precisely one session per entry, but
exceptions can be made.I would like to understand what would be the right circumstances for
making
such exceptions. I am working on a certain applied formalization
study/library for Isabelle/HOL. However, it is becoming resource hungry,
and I find it convenient to break it into several smaller sessions while
working. However, I doubt that any of these smaller parts,
taken individually, are sufficiently interesting as independent AFP
entries. Is performance/development time optimization a sufficiently good
reason for allowing the submission of several sessions in one entry?Usually not, because performance usually decreases with multiple sessions.
Multiple sessions are nicer for interactive work during development, but
once that phase is mostly over, a single large session can be usually be
processed more efficiently by Isabelle than multiple small ones.My own process these days is to have multiple sessions (when the
development is large) until it has reached a maintenance phase, and then
switch over. AFP submission is often (but not always) a good point for
that.Can I ask what the current processing time time is for the sessions you
have?Lastly, in the future, should I direct the questions about the AFP to
afp-submit@in.tum.de, or is it better/acceptable to post such queries on
the mailing list?Both are fine. afp-submit is more private, but it’s good to have some of
these questions here so they are more accessible.Cheers,
Gerwin
Email Gateway (Sep 20 2020 at 22:32):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,
This is merely a quick comment with regard to my previous post.
Email Gateway (Sep 20 2020 at 22:37):From: Manuel Eberl <eberlm@in.tum.de>
You don't happen to have debug mode enabled, do you? Although then I
would be surprised you can build them at all (they usually just crash
for me).
What /are/ your hardware specs?
Or are you perhaps on Windows and have third-party anti-virus software
enabled or something like that? Just a wild guess.
Manuel
Email Gateway (Sep 20 2020 at 23:40):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear Manuel Eberl/All,
Email Gateway (Sep 22 2020 at 02:15):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
Ok, so as summary from the discussion so far I would say for the AFP:
For working with something in the range of 1h, I would recommend multiple sessions for development, esp with memory constraints on the hardware (in my experience, memory size, e.g. 8GB vs e.g. 2GB can make a huge difference — so if you are looking to upgrade only something specific that is what I would go for).
Cheers,
Gerwin
Last updated: Jul 15 2022 at 23:21 UTC