From d0e4d8ab90cb6bc7cb75bd8922b968e51bfdd6f8 Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Thu, 1 Aug 2024 15:54:09 +0200 Subject: [PATCH] Added the link to CEP to the extended abstract for CoqWorkshopITP24 --- ressources/extended_abstract_ITP24_CoqWorkshop.tex | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/ressources/extended_abstract_ITP24_CoqWorkshop.tex b/ressources/extended_abstract_ITP24_CoqWorkshop.tex index 2af998b..6ad952e 100644 --- a/ressources/extended_abstract_ITP24_CoqWorkshop.tex +++ b/ressources/extended_abstract_ITP24_CoqWorkshop.tex @@ -48,9 +48,9 @@ \section{Motivation} Having a proper, clean and accessible documentation is one of the keys to the success of software. There are different forms of documentation: abstract and detailed documentation -like the reference manual~(\cite{Link_Coq_Ref}), course-shaped documentation like -Coq'Art~(\cite{bertot2013interactive}) or -Software Foundations~(\cite{Pierce:SF1}), or short action-oriented +like the reference manual~\cite{Link_Coq_Ref}, course-shaped documentation like +Coq'Art~\cite{bertot2013interactive} or +Software Foundations~\cite{Pierce:SF1}, or short action-oriented documentation. We focus on the latter. Short action-oriented documentation provides users with practical information on specific features of Coq, so that users can learn and discover new @@ -63,7 +63,7 @@ \section{Motivation} Books like Coq'Art or Software Foundations provide nice pedagogical explanations but target specific audiences, and are rather meant to be read from cover to cover. -Moreover, they are not well suited to learn about specific features, to discover +Moreover, they are not well suited for learning about specific features, to discover horizontally, and are not easy to keep updated. Yet, short action-oriented documentation has many interests: @@ -157,7 +157,7 @@ \section{Description of the project} In the future, we hope to support a more standard and expressive format, possibly using Alectryon~\cite{pit2020untangling}. -We are also writing a Coq Enhancement Proposal to discuss the project further with the community. +To further discuss the project, we have written a \href{https://github.com/coq/ceps/pull/91}{Coq Enhancement Proposal}. We hope that, eventually, this documentation will become part of the website that will be created when renaming Coq to \emph{the Rocq Prover}. \label{sect:bib}