Email Gateway (Jan 10 2025 at 12:11): Email Gateway (Jan 10 2025 at 12:11):From: Christian Pardillo Laursen <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle Community,
We have two undergraduate students in the Computer Science department at
the University of York who are doing final year projects on creation of a
package manager for Isabelle/HOL. The package manager is envisioned to
complement the AFP and streamline Isabelle-based development lifecycles. As
part of their methodology, they would like to survey the Isabelle community
to gather requirements and preferences for the development.
We'd be very grateful if you can therefore fill out the following survey:
https://york.qualtrics.com/jfe/form/SV_eUKMk2amXlWBsmq. May we please ask
you to only reply via the survey link, rather than by email. Thank you for
your help with this.
Best regards,
Christian Pardillo Laursen
Email Gateway (Jan 10 2025 at 12:42):From: Fabian Huch <huch@in.tum.de>
Could you elaborate what kind of packages you mean?
Fabian
On 1/8/25 13:06, Christian Pardillo Laursen (via cl-isabelle-users
Mailing List) wrote:
Dear Isabelle Community,
We have two undergraduate students in the Computer Science department
at the University of York who are doing final year projects on
creation of a package manager for Isabelle/HOL. The package manager is
envisioned to complement the AFP and streamline Isabelle-based
development lifecycles. As part of their methodology, they would like
to survey the Isabelle community to gather requirements and
preferences for the development.We'd be very grateful if you can therefore fill out the following
survey: https://york.qualtrics.com/jfe/form/SV_eUKMk2amXlWBsmq. May we
please ask you to only reply via the survey link, rather than by
email. Thank you for your help with this.Best regards,
Christian Pardillo Laursen
Email Gateway (Jan 10 2025 at 22:56):From: Makarius <makarius@sketis.net>
On 08/01/2025 13:06, Christian Pardillo Laursen (via cl-isabelle-users Mailing
List) wrote:
We have two undergraduate students in the Computer Science department at the
University of York who are doing final year projects on creation of a package
manager for Isabelle/HOL. The package manager is envisioned to complement the
AFP and streamline Isabelle-based development lifecycles.
Just a few side-remarks to widen the perspective.
* My paper "Isabelle/jEdit as IDE for domain-specific formal languages and
informal text documents"
https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?FIDE2018.6 from the FIDE workshop
2018 explains "PIDE document structure" in section 2. Such Isabelle-specific
concepts have emerged over decades from technical and cultural
side-conditions. There is usually little concern to copy other approaches,
just because they are "popular" or "every does it".
Further note, that for 25 years I've always been talking about "formal proof
documents" or "formal mathematical documents", rather than "program code" etc.
It still remains to be seen, if or when Isabelle will manage to present an
authoring model that is free from "program development" paradigms,
terminology, tooling etc. In this respect, see also my paper "Interaction with
Formal Mathematical Documents in Isabelle/PIDE"
https://arxiv.org/abs/1905.01735 from CICM 2019.
* At ITP 2023, some Coq people have published a paper on their build and
package management under the somewhat misleading title "Proof Repair
Infrastructure for Supervised Models: Building a Large Proof Repair Dataset",
see
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.26/LIPIcs.ITP.2023.26.pdf
Note that Coq projects follow a conventional model of make files with OPAM
packages (with many variations). That causes some problems, though, which were
the starting point for this paper: The authors wanted to collect data, but
ended up tinkering with Coq builds.
In Isabelle you could move directly to the application (harvesting formal
content from project results). See also this quote from section "5.2 Other
proof assistants" of the Coq paper:
"""
In Isabelle, the Archive of Formal Proofs (AFP) provides a highly centralized,
standard host for proof developments and eases their association with metadata
that may be useful for ML. The AFP also neatly versions proof developments for
every official release of Isabelle and semantically groups them in different
folders. At the time of writing, the AFP includes 725 proof developments [1],
and it already forms the basis of a static dataset for Isabelle [32]. We
suspect the AFP would also make a very strong basis for a proof repair dataset
due to its neat versioning.
"""
Please ignore what they later about PISA and scala-isabelle. The official
Isabelle/Scala infrastructure is sufficient to do all the heavy lifting,
without extra complication.
Makarius
Email Gateway (Jan 11 2025 at 11:58):From: "christian.laursen" <cl-isabelle-users@lists.cam.ac.uk>
By packages we mean collections of Isabelle theories which depend on other
packages.
Effectively AFP entries with more flexible versioning, although the specific
features that packages will have will be influenced by the data we collect
from the survey.
-Christian
Email Gateway (Jan 11 2025 at 12:07):From: Makarius <makarius@sketis.net>
On 10/01/2025 14:08, christian.laursen (via cl-isabelle-users Mailing List) wrote:
By packages we mean collections of Isabelle theories which depend on other
packages.
You probably mean "session" in official Isabelle terminology.
Effectively AFP entries with more flexible versioning, although the specific
features that packages will have will be influenced by the data we collect
from the survey.
An "AFP entry" is a slight extension of the concept of "session". Its precise
meaning is defined by the metadata and tooling of AFP (in Isabelle/Scala).
Makarius
Last updated: Jan 30 2025 at 04:21 UTC