Email Gateway (Aug 18 2022 at 19:11): Email Gateway (Aug 18 2022 at 19:11):From: Christian Sternagel <c-sterna@jaist.ac.jp>
@lukas: thanks for the hint.
@rene: sorry, I confused two things (map and mapM) so, Rene's suggestion
is orthogonal to what I said and indeed a useful lemma missing from
Option.thy in HOL.
cheers
chris
Email Gateway (Aug 18 2022 at 19:11):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear all,
related to Lukas comment (that also small contributions are appropriate
for the AFP) I have some thoughts:
(At least for me) the AFP has a somewhat formal flavor (like a
publication). Furthermore, every entry is associated to fixed authors
(is it possible to extend the author list later on?).
As for Option_Monad: this is a completely unfinished adhoc collection of
functions and lemmas related to the option type, so I'm reluctant to
send it to the AFP. What I do however want, is that other users that
could make use of an option monad have access to the parts that have
already been done and can contribute their own ideas.
It would be nice to have a common platform, where arbitrarily mature
developments could be posted, discussed, and improved by the community
(without any formal reviewing; what is useful to the community will
evolve, what is not will decay). Something like hackage for Haskell.
Maybe the AFP is exactly this platform and I was just not aware of it?
cheers
chris
Email Gateway (Aug 18 2022 at 19:11):From: Lukas Bulwahn <bulwahn@in.tum.de>
On 02/17/2012 02:06 PM, Christian Sternagel wrote:
Dear all,
related to Lukas comment (that also small contributions are
appropriate for the AFP) I have some thoughts:Tobias has encouraged small contributions. Don't think about it like a
publication, but like a library! (something like hackage, in your words.)
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2010-February/msg00092.html
(At least for me) the AFP has a somewhat formal flavor (like a
publication). Furthermore, every entry is associated to fixed authors
(is it possible to extend the author list later on?).As for Option_Monad: this is a completely unfinished adhoc collection
of functions and lemmas related to the option type, so I'm reluctant
to send it to the AFP. What I do however want, is that other users
that could make use of an option monad have access to the parts that
have already been done and can contribute their own ideas.Of course, the authors and the content can be extended. There is no
reason to be reluctant, many theory developments are being continued to
be completed, so there is no fear that an entry is rejected because it
is incomplete, as long as it is in a comprehensible state.
It would be nice to have a common platform, where arbitrarily mature
developments could be posted, discussed, and improved by the community
(without any formal reviewing; what is useful to the community will
evolve, what is not will decay). Something like hackage for Haskell.
Maybe the AFP is exactly this platform and I was just not aware of it?In the follow-ups of the mail above, the issues of reusing AFP entries
was discussed, but those issues should NOT stop you and others
contributing to the AFP.
Lukas
cheers
chris
On 02/17/2012 09:33 PM, Makarius wrote:
On Fri, 17 Feb 2012, Lukas Bulwahn wrote:
Just two comments:
First, the discussion about this should be on the isabelle mailing
list, not the isabelle developer's mailing list.
There has been a discussion just a few days ago that the developer's
mailing list is limited to arbitrary repository versions and the
related development process, including administrative things like
isatest, mira etc.Second, the AFP is a perfect place to also submit small library
developments. The List-Index theory is such an example.
So, the Option monad could be just turned into a small AFP entry.I've also asked myself again this question about isabelle-users vs.
isabelle-dev, when looking at the message for 2min, but considered it is
a boundary case that could go either way.In practice it is also a matter of the size of audience. There might be
yet unknown library contributions out there that could be joined in such
efforts. So there is definitely a tendency more towards isabelle-users.(Oddly isabelle-dev appears to be much more active recently than
isabelle-users. Are there fewer users or fewer user problems now?)Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 18 2022 at 19:11):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Seconded. Maybe I did not state it that way above, but actually I also
want the AFP to stay publication-like (and I viewed it like that until
now; if nothing else, to value the effort that is put into such entries).
Maybe there could be a different AFP "branch" that is purely library
oriented.
Concerning Tobias original mail (on small AFP entries): Strange how one
can forget mailing list discussions that were actually read with great
interest ;). What is the current state w.r.t. the discussion that
followed in 2010? IIRC, the points were roughly
Is there any way in which non-developers (like me) could contribute to
anything of the above?
cheers
christian
Email Gateway (Aug 18 2022 at 19:11):From: Gerwin Klein <gerwin.klein@nicta.com.au>
On 18/02/2012, at 1:07 AM, Christian Sternagel wrote:
On 02/17/2012 10:34 PM, Christian Urban wrote:
>On Friday, February 17, 2012 at 22:06:31 (+0900), Christian Sternagel wrote:
[ .. AFP should stay publication-like .. ]
To confirm previous discussions: Small entries in the AFP are perfectly fine. Libraries are wanted as well.
I think we do want to stay with a publication-like model.
That model seems to be working well for finished pieces of work, not so well for libraries. Of course, libraries are harder to create in the first place, so it's not surprising that there are fewer.
I don't see that a good reason for the AFP becoming a development platform with rapid development inside its repository. Similarly to hackage, cpan, ctan, and others, it should stay a release and collection place. Active development should happen elsewhere (own sourceforge project, bitbucket, etc). Regular releases from there could then go into the AFP.
Maybe there could be a different AFP "branch" that is purely library oriented.
I don't think a separate branch makes sense, but we could tag certain entries as libraries if that helps the psychology aspect. If they are actively developed, they can get a link to their home page/project page. That would also solve the problem of who to contact if you have something to contribute/request/etc. Technically we already support evolving versions of entries, and if things like author lists change, that can be marked in the change history.
Concerning Tobias original mail (on small AFP entries): Strange how one can forget mailing list discussions that were actually read with great interest ;). What is the current state w.r.t. the discussion that followed in 2010? IIRC, the points were roughly
- module name spaces
Centerum censeo that we need them more every year ;-)
- visibility of syntax
should be treated under the above
- installing entries (+ dependencies; something like cabal for Haskell)
I had a student project written out for this for a while, but no takers so far.
Is there any way in which non-developers (like me) could contribute to anything of the above?
If your interested in the last point, we could discuss that.
Cheers,
Gerwin
Email Gateway (Aug 18 2022 at 19:11):From: Makarius <makarius@sketis.net>
On Fri, 17 Feb 2012, Christian Sternagel wrote:
Concerning Tobias original mail (on small AFP entries): Strange how one
can forget mailing list discussions that were actually read with great
interest ;). What is the current state w.r.t. the discussion that
followed in 2010?
Can you point to the specific thread? These are recurrent topics, and I
have commented on them many times with varying details and focus.
IIRC, the points were roughly
- module name spaces
This probably means several things:
(1) clear indentification of theory files in the file-system
(2) qualified theory names
(3) ways to include theories without flat name space merge
- visibility of syntax
The latter is probably closely related to (3), and there is some chance
that the existing concept of syntax_declaration in the local_theory
department will address that.
Point (1) is addressed to some extent in official Isabelle2011-1 when
using the Isabelle/Scala document model, currently mainly via
Isabelle/jEdit. Here nodes are identified by full file names, so the
implicit collapse to theory base names is avoided. Thus it is already
possible to load most of AFP into one editor session without interfering
(which is only fun on 32 GB hardware). Using separate theories
Foo/Array.thy and Bar/Array.thy together requires some further reforms
that are not immediate.
Point (2) sounds easy, but is hard due to many entrenched customs about
name space usage in Isabelle. When the concept first occurred in 1998 it
was already clear that the common format of long names A.c (or A.b.c with
locales) is only accidental. Nonetheless, existing tools occasionally
depend on that. It will take more time to sort out all improper uses of
long names and name spaces. (Just some days ago I've convinced myself
that at least the use of "intern" is mostly right in the existing code
base for the next Isabelle release.)
- installing entries (+ dependencies; something like cabal for Haskell)
What means "installing"? Once we have a proper session specification in
the source trees (not ROOT.ML nor IsaMakefile) you merely point to such
points in the file space without "installation". Or did you mean
installation of so-called Isabelle components?
Dependencies are already managed pretty well by the Isabelle/Scala layer.
I hope people will dispose their private perl/python approximations at
some point. It is only one more step to unify this with the batch mode,
and discontinue the old usedir stuff (which is from the mid 1990-ies).
It will mean that there is only one way to process sources, without
surprises about different flags for skipping proofs etc. -- but sometimes
this behaviour is actually exploited, hindering such reforms again.
Is there any way in which non-developers (like me) could contribute to
anything of the above?
Part of the problem is the adhesion of many power users to extremely old
versions of Proof General / Emacs. De-facto I am still the main
maintainer of Proof General 3.x and 4.x, with lots of Emacsen on Linux,
Mac OS X, Windows. At the same time I am trying to get rid of the
TTY/Emacs regime for 4 years already.
It would help if the adherents to Proof General would somehow organize
themselves to take over the responsibility to maintain it with all
consequences.
Makarius
Email Gateway (Aug 18 2022 at 19:12):From: Brian Huffman <huffman@in.tum.de>
I would interpret "installing" to mean downloading theory files and
putting them into an appropriate place in the user's filesystem. After
"installing" an entry or theory library, users should be able to
easily import that library into their own theory files, by writing
something reasonable on the "imports" line (i.e., no absolute or
user-specific path names, but rather something portable that would
work also for anyone else who has installed the same library).
Email Gateway (Aug 18 2022 at 19:12):From: Gerwin Klein <gerwin.klein@nicta.com.au>
Yes, that would be precisely the idea.
It may be enough to just put a download of the entire AFP wherever the users wants and add the appropriate line to the user components file. Florian has basically already done the rest. The AFP is still of a size where we don't really need to disentangle separate entries.
Dependency management is then reduced to downloading the version of the AFP that fits to the Isabelle version the user has installed.
Cheers,
Gerwin
Email Gateway (Aug 18 2022 at 19:12):From: Christian Sternagel <c-sterna@jaist.ac.jp>
On 02/20/2012 05:19 AM, Makarius wrote:
On Fri, 17 Feb 2012, Christian Sternagel wrote:
Concerning Tobias original mail (on small AFP entries): Strange how
one can forget mailing list discussions that were actually read with
great interest ;). What is the current state w.r.t. the discussion
that followed in 2010?Can you point to the specific thread? These are recurrent topics, and I
have commented on them many times with varying details and focus.
I'm referring to this thread.
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2010-February/msg00092.html
(Sorry I had Lukas' answer (which contains the above link) already on my
machine before it arrived at the list but did not notice the difference
at first.)
cheers
chris
IIRC, the points were roughly
- module name spacesThis probably means several things:
(1) clear indentification of theory files in the file-system
(2) qualified theory names
(3) ways to include theories without flat name space merge
- visibility of syntax
The latter is probably closely related to (3), and there is some chance
that the existing concept of syntax_declaration in the local_theory
department will address that.Point (1) is addressed to some extent in official Isabelle2011-1 when
using the Isabelle/Scala document model, currently mainly via
Isabelle/jEdit. Here nodes are identified by full file names, so the
implicit collapse to theory base names is avoided. Thus it is already
possible to load most of AFP into one editor session without interfering
(which is only fun on 32 GB hardware). Using separate theories
Foo/Array.thy and Bar/Array.thy together requires some further reforms
that are not immediate.Point (2) sounds easy, but is hard due to many entrenched customs about
name space usage in Isabelle. When the concept first occurred in 1998 it
was already clear that the common format of long names A.c (or A.b.c
with locales) is only accidental. Nonetheless, existing tools
occasionally depend on that. It will take more time to sort out all
improper uses of long names and name spaces. (Just some days ago I've
convinced myself that at least the use of "intern" is mostly right in
the existing code base for the next Isabelle release.)
- installing entries (+ dependencies; something like cabal for Haskell)
What means "installing"? Once we have a proper session specification in
the source trees (not ROOT.ML nor IsaMakefile) you merely point to such
points in the file space without "installation". Or did you mean
installation of so-called Isabelle components?Dependencies are already managed pretty well by the Isabelle/Scala
layer. I hope people will dispose their private perl/python
approximations at some point. It is only one more step to unify this
with the batch mode, and discontinue the old usedir stuff (which is from
the mid 1990-ies). It will mean that there is only one way to process
sources, without surprises about different flags for skipping proofs
etc. -- but sometimes this behaviour is actually exploited, hindering
such reforms again.Is there any way in which non-developers (like me) could contribute to
anything of the above?Part of the problem is the adhesion of many power users to extremely old
versions of Proof General / Emacs. De-facto I am still the main
maintainer of Proof General 3.x and 4.x, with lots of Emacsen on Linux,
Mac OS X, Windows. At the same time I am trying to get rid of the
TTY/Emacs regime for 4 years already.It would help if the adherents to Proof General would somehow organize
themselves to take over the responsibility to maintain it with all
consequences.Makarius
Email Gateway (Aug 18 2022 at 19:12):From: Christian Sternagel <c-sterna@jaist.ac.jp>
On 02/20/2012 06:45 AM, Gerwin Klein wrote:
On 20/02/2012, at 7:55 AM, Brian Huffman wrote:
On Sun, Feb 19, 2012 at 9:19 PM, Makarius<makarius@sketis.net> wrote:
- installing entries (+ dependencies; something like cabal for Haskell)
What means "installing"? Once we have a proper session specification in the
source trees (not ROOT.ML nor IsaMakefile) you merely point to such points
in the file space without "installation". Or did you mean installation of
so-called Isabelle components?I would interpret "installing" to mean downloading theory files and
putting them into an appropriate place in the user's filesystem. After
"installing" an entry or theory library, users should be able to
easily import that library into their own theory files, by writing
something reasonable on the "imports" line (i.e., no absolute or
user-specific path names, but rather something portable that would
work also for anyone else who has installed the same library).Yes, that would be precisely the idea.
Yes that was what I meant.It may be enough to just put a download of the entire AFP wherever the users wants and add the appropriate line to the user components file. Florian has basically already done the rest. The AFP is still of a size where we don't really need to disentangle separate entries.
Dependency management is then reduced to downloading the version of the AFP that fits to the Isabelle version the user has installed.
I guess it would suffice, but I was more thinking of the following
(again, like cabal for Haskell): you type on your machine the entry that
you want to install, e.g.,
$ afp install Refine_Monadic
and then the above (i.e., downloading theory files and putting them into
an appropriate place in the filesystem) happens for all files from the
afp on which Refine_Monadic does depend on. Afterwards (as Brian pointed
out) it should be possible without further ado, to import the
"installed" entry in your own theories in a way that does not depend on
any local setup.
cheers
chris
Email Gateway (Aug 18 2022 at 19:12):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear all,
Agreeing to the below
I started a sourceforge project to develop a "library" for the option monad:
http://sourceforge.net/p/optionmonad/
Of course in Isabelle/HOL it is difficult to have the "right" lemmas
without actual applications. Some applications of the current version of
Option_Monad.thy can be found in the theories Substitution,
Ground_Context_Impl, Equational_Reasoning, and Check_Equational_Proof of
http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR
That's where the current lemmas originate.
It would make sense to have example applications (for regression
testing) as part of the project. Please join the project, contribute
(monadic functions, properties, or example applications), and comment.
I would like to view this as a playground (to find out how such a kind
of project works for Isabelle/HOL), so don't worry to much before
changing something.
cheers
chris
Email Gateway (Aug 18 2022 at 19:12):From: Makarius <makarius@sketis.net>
On Mon, 20 Feb 2012, Gerwin Klein wrote:
It may be enough to just put a download of the entire AFP wherever the
users wants and add the appropriate line to the user components file.
This sounds good. The whole download is approx. 7MB compressed and 43MB
uncompressed. This is tiny compared with the main Isabelle distribution.
By providing a suitable etc/settings its file-space can be easily injected
into Isabelle via some $AFP variable. So imports can refer to theories
like "$AFP/Foo/Bar".
Florian has basically already done the rest. The AFP is still of a size
where we don't really need to disentangle separate entries.
This probably refers to
http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/5b970f669325
Florian has called it "rudimentary support for AFP as Isabelle component",
but it looks fine to be. The remaining odditiy is that is unavailable for
actual users: the official downloads of AFP only contain the content of
the thys directory, without this etc/settings file.
Makarius
Email Gateway (Aug 18 2022 at 19:13):From: Gerwin Klein <gerwin.klein@nicta.com.au>
On 20/02/2012, at 10:53 PM, Makarius wrote:
On Mon, 20 Feb 2012, Gerwin Klein wrote:
It may be enough to just put a download of the entire AFP wherever the users wants and add the appropriate line to the user components file.
This sounds good. The whole download is approx. 7MB compressed and 43MB uncompressed. This is tiny compared with the main Isabelle distribution.
By providing a suitable etc/settings its file-space can be easily injected into Isabelle via some $AFP variable. So imports can refer to theories like "$AFP/Foo/Bar".
Yes, exactly.
Florian has basically already done the rest. The AFP is still of a size where we don't really need to disentangle separate entries.
This probably refers to http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/5b970f669325
Yes.
Florian has called it "rudimentary support for AFP as Isabelle component", but it looks fine to be. The remaining odditiy is that is unavailable for actual users: the official downloads of AFP only contain the content of the thys directory, without this etc/settings file.
Good point. That can easily be fixed.
Gerwin
Last updated: Apr 25 2024 at 04:18 UTC