Email Gateway (Aug 22 2022 at 20:55): Email Gateway (Aug 22 2022 at 20:55):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
I would like to provide a brief update on the status of the development of
the extension of Types-To-Sets (
https://github.com/xanonec/HOL-TTS-Ext/tree/ba4d22cac7fbcb907aad28ecbe00b6098c1f956c
and https://github.com/xanonec/HOL-SML-Relativization) and ask several
questions. The primary motivation for the development of the framework were
some of my personal applied formalization efforts. However, while my
extension of the framework Types-To-Sets has reached a certain level of
maturity, I slowly converged on the opinion that I would prefer not to rely
on it in my own applied formalization work (the reasons for converging on
this opinion are, primarily, subjective). Moreover, my personal
circumstances have changed and I can no longer afford to spend as much time
working on it as I was able around this summer.
Due to what is outlined in the previous paragraph, it no longer seems
feasible for me to continue investing a significant amount of time in the
further development of this framework (quite frankly, I have nearly
abandoned this project at some point in September). Nevertheless, given
that others have found Types-To-Sets useful, and I would like to think that
the extension that I developed significantly improves the user experience
for most of the routine relativization tasks, I am curious whether this
work could be considered/recommended for the submission to the AFP, despite
being somewhat rough.
Complete disclosure: the initial plans for further development included
(informal) proofs of what I considered to be the critical parts of the
implementation, unit testing of the less critical parts, user input
verification (in conjunction with the proof/unit testing), refactoring the
code and improvement of efficiency (the existing implementation is highly
suboptimal in almost every aspect), provision of the documentation and
further examples. Given my current circumstances, I would consider
improving the user input verification (without any testing or proof and,
therefore, without too much confidence) and providing documentation in the
style consistent with the Isabelle/Isar reference manual/tutorials prior to
the submission. However, refactoring, proof and/or unit testing would
require more time than I would like to dedicate to further development of
this framework.
I am reasonably impartial as to whether this work will be published on the
AFP or not. Therefore, the question comes down to whether the authors of
the original idea, those who have taken it further in the past and the
existing users of Types-To-Sets would consider adopting my implementation.
Most certainly, I would be keen to provide continuous support in the form
of bug fixes and explanations of any design decisions/functionality. If I
receive sufficient encouragement to submit it to the AFP, then I will
allocate (approximately) 2 hours every week (perhaps, a little bit more
time around Christmas) towards the completion of the development of a
system for the user input verification and the documentation. In this case,
I will be aiming to prepare it for the submission to the AFP before the end
of January. However, I expect that most of the code will remain as it
stands (the only exception being the removal of certain auxiliary and
unfinished features).
Thank you
Email Gateway (Aug 22 2022 at 20:59):From: Fabian Immler <immler@in.tum.de>
Hi,
On 11/3/2019 7:15 PM, mailing-list anonymous wrote:
Dear All,
I would like to provide a brief update on the status of the development of
the extension of Types-To-Sets (
https://github.com/xanonec/HOL-TTS-Ext/tree/ba4d22cac7fbcb907aad28ecbe00b6098c1f956c
and https://github.com/xanonec/HOL-SML-Relativization) and ask several
questions. The primary motivation for the development of the framework were
some of my personal applied formalization efforts. However, while my
extension of the framework Types-To-Sets has reached a certain level of
maturity, I slowly converged on the opinion that I would prefer not to rely
on it in my own applied formalization work (the reasons for converging on
this opinion are, primarily, subjective).
It would be interesting to know why you decided not to use your
framework in your own work - because of the framework, or because e.g.,
it builds on additional axioms?
Moreover, my personal
circumstances have changed and I can no longer afford to spend as much time
working on it as I was able around this summer.Due to what is outlined in the previous paragraph, it no longer seems
feasible for me to continue investing a significant amount of time in the
further development of this framework (quite frankly, I have nearly
abandoned this project at some point in September).
Nevertheless, given
that others have found Types-To-Sets useful, and I would like to think that
the extension that I developed significantly improves the user experience
for most of the routine relativization tasks, I am curious whether this
work could be considered/recommended for the submission to the AFP, despite
being somewhat rough.
This sounds very nice: if it significantly improves the user experience
for Types-To-Sets, I would encourage you to submit it to the AFP.
I think I would prefer to would use your framework instead of e.g., the
ad-hoc developments in e.g., Types_To_Sets/Examples/Linear_Algebra_On.thy
I did not look at the details of your implementation in a while, so I
cannot judge the technical quality of your work.
But ultimately that is up to the editors of the AFP.
Fabian
Complete disclosure: the initial plans for further development included
(informal) proofs of what I considered to be the critical parts of the
implementation, unit testing of the less critical parts, user input
verification (in conjunction with the proof/unit testing), refactoring the
code and improvement of efficiency (the existing implementation is highly
suboptimal in almost every aspect), provision of the documentation and
further examples. Given my current circumstances, I would consider
improving the user input verification (without any testing or proof and,
therefore, without too much confidence) and providing documentation in the
style consistent with the Isabelle/Isar reference manual/tutorials prior to
the submission. However, refactoring, proof and/or unit testing would
require more time than I would like to dedicate to further development of
this framework.I am reasonably impartial as to whether this work will be published on the
AFP or not. Therefore, the question comes down to whether the authors of
the original idea, those who have taken it further in the past and the
existing users of Types-To-Sets would consider adopting my implementation.
Most certainly, I would be keen to provide continuous support in the form
of bug fixes and explanations of any design decisions/functionality. If I
receive sufficient encouragement to submit it to the AFP, then I will
allocate (approximately) 2 hours every week (perhaps, a little bit more
time around Christmas) towards the completion of the development of a
system for the user input verification and the documentation. In this case,
I will be aiming to prepare it for the submission to the AFP before the end
of January. However, I expect that most of the code will remain as it
stands (the only exception being the removal of certain auxiliary and
unfinished features).Thank you
Email Gateway (Aug 22 2022 at 21:01):From: Manuel Eberl <eberlm@in.tum.de>
On 07/11/2019 02:30, mailing-list anonymous wrote:
1. If a given submission does not get accepted, is this event going to
appear on public records online?
No. And I at least have never heard of any academic conference or
journal that does that.
2. If a given submission does not get accepted, would I receive any
critical feedback (that goes beyond saying that the quality is not
acceptable)?
If possible, yes. If there are only a few minor problematic aspects,
authors are usually encouraged to remedy them and resubmit.
Source: I am an AFP editor.
We have not had many AFP entries so far that contained a significant
amount of ML code, let alone that consist entirely of ML code. Moreover,
I think René Thiemann is the only AFP editor who has ever worked with
Types-to-Sets at all and I don't know if he is familiar with its
internals. This might make your entry a bit tough to review, but I'm
sure we'll figure it out.
Lastly, I can imagine that the users of this mailing list are, most likely,
tired of hearing about Types-To-Sets.
If they are, they will have to endure it. ;)
Types-to-Sets is an important subject and anything that makes it more
usable in Isabelle is worth being discussed on the list. (Any decent
email program allows muting threads easily for those who are not interested)
Cheers,
Manuel
Last updated: Apr 20 2024 at 08:16 UTC