-
Advantages of maintaining a multi-task project-specific bot: an experience report
Authors:
Théo Zimmermann,
Julien Coolen,
Jason Gross,
Pierre-Marie Pédrot,
Gaëtan Gilbert
Abstract:
Bots are becoming a popular method for automating basic everyday tasks in many software projects. This is true in particular because of the availability of many off-the-shelf task-specific bots that teams can quickly adopt (which are sometimes completed with additional task-specific custom bots). Based on our experience in the Coq project, where we have developed and maintained a multi-task projec…
▽ More
Bots are becoming a popular method for automating basic everyday tasks in many software projects. This is true in particular because of the availability of many off-the-shelf task-specific bots that teams can quickly adopt (which are sometimes completed with additional task-specific custom bots). Based on our experience in the Coq project, where we have developed and maintained a multi-task project-specific bot, we argue that this alternative approach to project automation should receive more attention because it strikes a good balance between productivity and adaptibility. In this article, we describe the kind of automation that our bot implements, what advantages we have gained by maintaining a project-specific bot, and the technology and architecture choices that have made it possible. We draw conclusions that should generalize to other medium-sized software teams willing to invest in project automation without disrupting their workflows.
△ Less
Submitted 27 April, 2022;
originally announced April 2022.
-
Extending the team with a project-specific bot
Authors:
Théo Zimmermann,
Julien Coolen,
Jason Gross,
Pierre-Marie Pédrot,
Gaëtan Gilbert
Abstract:
While every other software team is adopting off-the-shelf bots to automate everyday tasks, the Coq team has made a different choice by develo** and maintaining a project-specific bot from the ground up. In this article, we describe the reasons for this choice, what kind of automation this has allowed us to implement, how the many features of this custom bot have evolved based on internal feedbac…
▽ More
While every other software team is adopting off-the-shelf bots to automate everyday tasks, the Coq team has made a different choice by develo** and maintaining a project-specific bot from the ground up. In this article, we describe the reasons for this choice, what kind of automation this has allowed us to implement, how the many features of this custom bot have evolved based on internal feedback, and the technology and architecture choices that have made it possible.
△ Less
Submitted 14 December, 2021;
originally announced December 2021.
-
Design and Implementation of the Andromeda Proof Assistant
Authors:
Andrej Bauer,
Gaëtan Gilbert,
Philipp G. Haselwarter,
Matija Pretnar,
Christopher A. Stone
Abstract:
Andromeda is an LCF-style proof assistant where the user builds derivable judgments by writing code in a meta-level programming language AML. The only trusted component of Andromeda is a minimalist nucleus (an implementation of the inference rules of an object-level type theory), which controls construction and decomposition of type-theoretic judgments.
Since the nucleus does not perform complex…
▽ More
Andromeda is an LCF-style proof assistant where the user builds derivable judgments by writing code in a meta-level programming language AML. The only trusted component of Andromeda is a minimalist nucleus (an implementation of the inference rules of an object-level type theory), which controls construction and decomposition of type-theoretic judgments.
Since the nucleus does not perform complex tasks like equality checking beyond syntactic equality, this responsibility is delegated to the user, who implements one or more equality checking procedures in the meta-language. The AML interpreter requests witnesses of equality from user code using the mechanism of algebraic operations and handlers. Dynamic checks in the nucleus guarantee that no invalid object-level derivations can be constructed. %even if the AML code (or interpreter) is untrusted.
To demonstrate the flexibility of this system structure, we implemented a nucleus consisting of dependent type theory with equality reflection. Equality reflection provides a very high level of expressiveness, as it allows the user to add new judgmental equalities, but it also destroys desirable meta-theoretic properties of type theory (such as decidability and strong normalization).
The power of effects and handlers in AML is demonstrated by a standard library that provides default algorithms for equality checking, computation of normal forms, and implicit argument filling. Users can extend these new algorithms by providing local "hints" or by completely replacing these algorithms for particular developments. We demonstrate the resulting system by showing how to axiomatize and compute with natural numbers, by axiomatizing the untyped $λ$-calculus, and by implementing a simple automated system for managing a universe of types.
△ Less
Submitted 17 February, 2018;
originally announced February 2018.
-
Formalising Real Numbers in Homotopy Type Theory
Authors:
Gaëtan Gilbert
Abstract:
Cauchy reals can be defined as a quotient of Cauchy sequences of rationals. The limit of a Cauchy sequence of Cauchy reals is defined through lifting it to a sequence of Cauchy sequences of rationals. This lifting requires the axiom of countable choice or excluded middle, neither of which is available in homotopy type theory. To address this, the Univalent Foundations Program uses a higher inducti…
▽ More
Cauchy reals can be defined as a quotient of Cauchy sequences of rationals. The limit of a Cauchy sequence of Cauchy reals is defined through lifting it to a sequence of Cauchy sequences of rationals. This lifting requires the axiom of countable choice or excluded middle, neither of which is available in homotopy type theory. To address this, the Univalent Foundations Program uses a higher inductive-inductive type to define the Cauchy reals as the free Cauchy complete metric space generated by the rationals. We generalize this construction to define the free Cauchy complete metric space generated by an arbitrary metric space. This forms a monad in the category of metric spaces with Lipschitz functions. When applied to the rationals it defines the Cauchy reals. Finally, we can use Altenkirch and Danielson (2016)'s partiality monad to define a semi-decision procedure comparing a real number and a rational number.
The entire construction has been formalized in the Coq proof assistant. It is available at https://github.com/SkySkimmer/HoTTClasses/tree/CPP2017 .
△ Less
Submitted 18 October, 2016; v1 submitted 17 October, 2016;
originally announced October 2016.
