**Karl Palmskog @palmskog** posted in **CoqHammer 1.2.1 for Coq 8.10 and 8.11**

We are happy to announce the release of CoqHammer 1.2.1 for Coq 8.10 and Coq 8.11.

These releases include new automated reasoning tactics based on a general proof search procedure for the Calculus of Inductive Constructions, as described in a paper to appear in the proceedings of IJCAR 2020. The procedure is shown to be superior to many other general procedures, such as Coq’s firstorder tactic, o...

**@affeldt** posted in **MathComp 1.11.0 released**

We are proud to announce the immediate availability of the

Mathematical Components library version 1.11.0.

This release is compatible with Coq 8.7, 8.8, 8.9, 8.10, 8.11.

The main improvement introduced by this release is the introduction of

order structures. The change should mostly be visible by users of ssrnum.

Version 1.11.0 fixes a problem of 1.11+beta1 so that we allow again

min and max...

**Guillaume Melquiond @silene** posted in **CoqInterval 4.0 released**

The CoqInterval library provides tactics for simplifying the proofs of inequalities on expressions of real numbers, for Coq 8.8 and later. See http://coq-interval.gforge.inria.fr/ for the documentation. As usual, it is available as the coq-interval Opam package.

Since this release comes with some major breaking changes, I am exceptionally announcing it here to help users with the transition.

Ove...

**Clément Pit-Claudel @cpitclaudel** posted in **First release of Kôika 🦑, a core language for rule-based hardware design**

Hi all,

In preparation for PLDI, Thomas Bourgeat and I recently made our first public release of Kôika, a Coq EDSL for rule-based hardware design. Here is a brief description, taken from the README:Kôika is an experimental hardware design language inspired by BlueSpec SystemVerilog. Kôika programs are built from rules, small bits of hardware that operate concurrently to compute state updates ...

These were the last 4 announcements on Discourse. Starting now, anyone wanting to announce a new release or event may do so on Discourse only and it will be forwarded to Zulip. This stream is otherwise restricted (only admins can post here). So if you wish to post a reply to an announcement, head over to Discourse (note that replies won't be forwarded to Zulip).

**Pierre Marie Pédrot @ppedrot** posted in **Coq 8.11.2**

Coq 8.11.2 is now officially released! As usual, you’ll find it on

or in your favourite packaging infrastructure.

Coq 8.11.2 brings in a handful of minor bugfixes, see the changelog at

https://coq.github.io/doc/V8.11.2/refman/changes.html#changes-in-8-11-2

**Théo Zimmermann @Zimmi48** posted in **First beta release of Coq 8.12 (and a call for help to improve the documentation)**

We are happy to announce the first beta release of Coq 8.12.

This new version integrates many usability improvements, in particular to notations, scopes and implicit arguments, along with many bug fixes and major improvements to the reference manual. See the changelog for details.

As usual, we are looking for feedback from beta testers. In addition, we are looking for beta readers of the update...

**Matthieu Sozeau @mattam82** posted in **Equations 1.2.2 for Coq 8.11 and Coq 8.12**

It is my pleasure to announce the release of Equations 1.2.2 for Coq 8.11 and Coq 8.12. Equations 1.2.2 is a bugfix release of the 1.2 version solving a number of issues detailed in the release notes, notably on the dependent elimination and induction tactics. It is compatible with Coq 8.12 beta1 (package coq-equations.1.2.2+8.12 in the coq-opam core-dev repository).

Enjoy!

**Théo Zimmermann @Zimmi48** posted in **Call for partipation to the Coq workshop 2020**

July 5-6, the Internet.

https://coq-workshop.gitlab.io/2020/

The Coq Workshop 2020 is part of IJCAR 2020 and the Paris Nord Summer of LoVe 2020.

Registration is free of charge, but required: https://fscd-ijcar-2020.org/register

The Coq workshop 2020 is the 11th Coq Workshop. The Coq Workshop series brings together Coq users, developers, and contributors. While conferences usually provide a v...

**@Guest0x0** posted in **[ANN] Coqoune**

I am glad to announce the first public release of coqoune, a Coq plugin for the kakoune editor, featuring a similar interface to coqIDE.

The features provided by coqoune is currently rather primitive, compared to more mature Coq environments like coqIDE, vsCoq, etc. The benefits of coqoune is basically those of the kakoune editor, for example:kakoune features a great modal editing interface a...

**Karl Palmskog @palmskog** posted in **Initial release of Roosterize, a tool for suggesting lemma names, for Coq 8.10**

Dear Coq users and developers,

We are happy to announce the initial release of Roosterize, a tool for suggesting lemma names in Coq verification projects.Roosterize learns and suggests lemma names using neural networks that take serialized Coq lemma statements and elaborated terms as input. The technique is described in a research paper published in the proceedings of IJCAR 2020, where it was...

**Karl Palmskog @palmskog** posted in **Initial release of machine learning dataset based on Mathematical Components 1.9.0**

Dear Coq users and developers,

We are happy to announce the initial release of a dataset for use in machine learning, based on Coq 8.10.2 and the Mathematical Components library version 1.9.0.The dataset is based on 449 source files from 21 Coq projects, which are in total over 297k lines of code and contains over 23k lemmas, with projects divided into tiers based on adherence to the MathComp...

**Clément Pit-Claudel @cpitclaudel** posted in **PLV has a new blog!**

Hi all,

We just launched our new blog at https://plv.csail.mit.edu/blog/! Multiple members of our lab were looking for an informal way to share research updates, Coq tips, tutorials, and new ideas, so we set one up.

We’re launching with a few posts already, plus a small intro page at https://plv.csail.mit.edu/blog/pages/how-to.html:Some Coq tips:

How to write a type-safe unwrap (aka fromJ...

**@RalfJ** posted in **Iris 3.3 and std++ 1.4**

Hello everyone,

We are pleased to announce the release of Iris 3.3, a concurrent separation logic framework for Coq. For an overview of the numerous research projects employing Iris, see https://iris-project.org/. Iris 3.3 is accompanied by std++ 1.4, an extended “standard” library for Coq.

This Iris release does not have any outstanding highlights, but contains a large number of improvements al...

**Li-yao Xia @Lyxia** posted in **Coq Planet, a link aggregator about Coq**

There are so many sites to talk about Coq nowadays. You can now find many recent discussion threads in one place at https://coq.pl-a.net

**Théo Zimmermann @Zimmi48** posted in **Coq 8.12.0 is out!**

Dear Coq users,

We are happy to announce the release of Coq 8.12.0.

Some highlights from this release are:

- a new binder notation for non-maximal implicit arguments;
- an improved Search command which accepts more complex queries;
- many additions to the standard library;
- a restructured reference manual;
- the deprecation of the omega tactic in favor the lia tactic.

Please see the chang...

**@Sophie_Tourret** posted in **CADE-28 Call for Papers, Workshops, Tutorials, and Competitions**

CADE-28: Call for Papers, Workshops, Tutorials and Competitions

The 28th International Conference on Automated Deduction (CADE-28)

Carnegie Mellon University, Pittsburgh, USA. 11-16th July 2021.

http://www.cade-28.info

CADE will carefully monitor the development of the COVID-19 pandemic, and take

guidance from from the health authorities, to determine whether CADE-28 will be

physical or onl...

**Pierre Marie Pédrot @ppedrot** posted in **[poll] Next CUDW 2020 -- Reloaded**

as you may recall the Coq User and Developer Workshop that was supposed to take place in June was cancelled. Since it is a very helpful event for people trying to get into the intricacies of the Coq development, we are tentatively trying to get an ersatz version of the CUDW this fall.

The exact format is not decided yet, but the event will be held remotely and spread over a week. In order to sett...

**@amintimany** posted in **CoqPL 2021: Call for Presentations**

===================================================================

CoqPL 2021`7th International Workshop on Coq for Programming Languages -- January 19, 2021, co-located with POPL Copenhagen, Denmark CALL FOR PRESENTATIONS https://popl21.sigplan.org/home/CoqPL-2021`

====...

**Matthieu Sozeau @mattam82** posted in **PhD Position on Certified Extraction in Nantes**

The Gallinette team is looking for a highly qualified PhD student to

work on an Inria-Nomadic Labs project on the subject of certified

extraction from Coq to OCaml. The student will be part of the Gallinette

team in Nantes, attached to the Inria Rennes - Bretagne Atlantique

research center (http://gallinette.inria.fr). The thesis will be funded

for 3 years, and the starting date is flexible b...

**Jonathan Protzenko @msprotz** posted in **Call for Presentations: PriSC 2021 @ POPL 2021 **

All details are on the PriSC site

https://popl21.sigplan.org/home/prisc-2021 and in this email.

Call for Presentations: PriSC 2021 @ POPL 2021

The emerging field of secure compilation aims to preserve security properties of programs when they have been compiled to low-level languages such as assembly, where high-level abstractions don’t exist,

and unsafe, unexpected interactions with libraries,...

**Mariano M. Moscato @marianomoscato** posted in **NASA Formal Methods 2021 - Call for Papers**

(Apologies for possible cross-posting.)

The Thirteenth NASA Formal Methods Symposiumhttps://shemesh.larc.nasa.gov/nfm2021/

24-28 May 2021

Norfolk, VA, USAThe symposium will be held in an in-person/virtual hybrid format in Norfolk, VA, USA, possibly transitioning to fully virtual depending on the COVID-19 situation.

Theme of the Symposium

The widespread use and increasing complexity of miss...

**Donald Sebastian Leung @DonaldKellett** posted in **Coq 8.12 is now supported on Codewars**

The Codewars community is excited to announce the support of Coq 8.12 for all approved Kata (code challenges) and all but 2 Beta Kata as of 08/10/2020. Here at Codewars, we believe that practice makes perfect and in order to ensure the continued quality of our platform as an invaluable training resource for those wishing to learn Coq and/or further refine their Coq-fu, it is necessary to support t...

**Pierre Marie Pédrot @ppedrot** posted in **Next CUDW 2020/11/30 to 2020/12/04 — Save the Date!**

At last, the Coq User and Developer Workshop has been properly scheduled! It will be held remotely between November, 30th and December, 4th. Given the novelty of this endeavour, the precise organization, format, and technology used are yet to be decided.

There is a dedicated Zulip stream to precisely discuss these matters. If you are interested, you are encouraged to join atCrowdsourcing a CU...

**@barryjay** posted in **Tree Calculus**

The draft of my book “Reflective Programs in Tree Calculus” is now available for comment at https://github.com/barry-jay-personal/tree-calculus/blob/master/tree_book.pdf Some front-matter is available from https://github.com/barry-jay-personal/tree-calculus/blob/master/tweets_on_trees.pdf

It may be of interest for two reasons:all proofs have been verified in Coq, and

the subject matter will be...

**@JasonGross** posted in **Ph.D. Defense of Jason Gross on Performance Engineering of Proof-Based Software Systems at Scale**

To those of you who may be interested, I’ll be defending my Ph.D. thesis (titled “Performance Engineering of Proof-Based Software Systems at Scale”, aka “Why is Coq so Slow‽ and How Do We Fix It?”) on Monday, November 30th at 11 am EST on Zoom. Anyone is welcome to attend; email me directly at jgross@mit.edu if you’d like the zoom link and password (not shared here to prevent zoombombing).

Abstr...

**Clément Pit-Claudel @cpitclaudel** posted in **Alectryon: tools for writing technical documents that mix Coq code and prose**

Hi all,

I’ve just released Alectryon 1.0!

Alectryon is a collection of tools for writing technical documents that mix Coq code and prose. It includes a compiler that produces interactive webpages from Coq source files, as well as tools to translate back and forth between Coq and reStructuredText, allowing you to toggle between the proof and prose views of a file at will as you edit it. From the...

**Théo Zimmermann @Zimmi48** posted in **Coq 8.12.1 is out!**

Dear Coq users and contributors,

We are happy to announce the release of Coq 8.12.1.

This release contains numerous bug fixes and documentation improvements. Some bug fix highlights:Polymorphic side-effects inside monomorphic definitions were incorrectly handled as not inlined. This allowed deriving an inconsistency.

Regression in error reporting after SSReflect’s case tactic. A generic error...

**@affeldt** posted in **MathComp 1.12.0 released**

We are proud to announce the immediate availability of the Mathematical

Components library version 1.12.0.

The webpage, and documentation, are available at https://math-comp.github.io/.

This release is compatible with Coq 8.10, Coq 8.11, and Coq 8.12.

The main changes are:

support for Coq 8.7, 8.8, and 8.9 have been dropped,

a change of implementation of intervals and the updated theory,

th...

**@Lasse** posted in **Announcing Tactician 1.0 beta1**

I’d like to announce the first beta release of Tactician, a tactic machine learning plugin for Coq. I have copied the release notes below:

We would like to announce Tactician 1.0 beta1, the first official release of Tactician.

Tactician is a tactic learner and prover for the Coq Proof Assistant. The system will help users make tactical proof decisions while they retain control over the general ...

**Erik Martin Dorel @erikmd** posted in **About the -native-compiler flag and the coq-native opam package (to be released before Coq 8.13+beta1)**

Dear Coq users,

This announcement deals with Coq’s native_compute support (which is typically interesting to get increased performance when using reflexive tactics). It focuses in particular on the -native-compiler flag for both ./configure and coqc binaries, as well as the corresponding packaging in opam-repository.

TL;DR: Following the discussion that took place in the CEP 48 (Coq Enhancement ...

**Enrico Tassi @gares** posted in **Release of Coq 8.13+beta1**

Dear Coq users,

The Coq development team is proud to announce the immediate

availability of Coq 8.13+beta1:The full list of changes is available at the following address

We encourage our users to test this beta release, in particular:

- The windows installer is now based on the Coq platform: This

greatly simplifies its build process and makes it easy to add

more packages. At the sa...

**@lthms** posted in **Towards coqffi.1.0.0 (Call for Testers)**

I am pleased to announce that coqffi is almost ready for its first official release, and is already available in the released repository of the Opam Coq Archive for users to try it.

If you do not already know, coqffi generates the necessary Coq boilerplate to use OCaml functions in a Coq development, and configures the Coq extraction mechanism accordingly. In practice, it greatly reduces the hass...

**Catalin Hritcu @catalin.hritcu** posted in **Research internships at MPI**

3 Max Planck Institutes are offering CS research internships next summer. We are looking for advanced students in all areas of CS. Applicants do not need prior research experience. The application deadlines are December 31 and January 31: https://www.cis.mpg.de/internships

**Théo Zimmermann @Zimmi48** posted in **Coq 8.12.2 is out**

Dear Coq users and contributors,

We are happy to announce the release of version 8.12.2 of the Coq

proof assistant:This release is virtually identical to the 8.12.1 release except for

two fixes of impacting 8.12 regressions.

In addition, the Windows installer is now based on the Coq platform

(https://github.com/coq/platform), like the one of the recently

released 8.13+beta1 version. For ...

**Enrico Tassi @gares** posted in **Release of Coq 8.13.0**

Dear Coq users,

The Coq development team is proud to announce the immediate

availability of Coq 8.13.0:The full list of changes is available at the following address

https://coq.github.io/doc/v8.13/refman/changes.html#version-8-13

Highlights:

Introduction of primitive persistent arrays in the core language,

implemented using imperative persistent arrays.Introduction of definition...

**Cyril Cohen @CohenCyril** posted in **A formal proof of Abel-Ruffini Theorem in Coq**

Dear Coq community,

I am happy to announce that we – Sophie Bernard, Cyril Cohen, Assia Mahoubi and Pierre-Yves Strub – were able to formalize in Coq a proof of Abel-Ruffini Theorem, which states that there are polynomials of degree 5 that are not solvable by radicals, e.g. X^5 - 4X + 2.

Lemma example_not_solvable_by_radicals :

~ solvable_by_radical_poly ('X^5 - 4%:R *: 'X + 2%:Q%:P).This is...

**Christian Doczkal @chdoc** posted in **[CFP] The Coq Workshop 2021 : Call for Talk Proposals**

The Coq Workshop 2021: Call for Talk Proposals

Colocated with the 12th conference on Interactive Theorem Proving (ITP 2021)

Online

Find this call online at: The Coq Workshop 2021

We are pleased to invite you to submit talk proposals for the Coq

Workshop 2021, which will be held online on July 2nd, 2021.

The Coq Workshop is part of ITP 2021, which will also be held online.

The Coq Workshop 2...

**Pierre Castéran @casteran** posted in **Hydra battles**

Dear Coq users,

The objective of coq-community <coq-community · GitHub> is to maintain and/or document coq developments. The project hydra-battles (in reference to Kirby and Paris's work) is an attempt to understand which kind of document may go with Coq libraries. It is developped in <GitHub - coq-community/hydra-battles: Variations on Kirby & Paris' hydra battles and other entertaining math in ...

**Enrico Tassi @gares** posted in **[Coq-Club] Release of Coq 8.13.1**

Dear Coq users,

The Coq development team is proud to announce the immediate

availability of Coq 8.13.1:Highlights:

- Fix arities of VM opcodes for some floating-point operations that

could cause memory corruption.

Best,

**Enrico Tassi @gares** posted in **Release of the Coq platform 2021.02.0**

Dear Coq community,

the Coq development team is proud to announce the immediate

availability of the Coq Platform version 2021.02.0

The Coq platform is a distribution of the Coq proof assistant together

with a selection of Coq libraries. It provides a set of scripts to

compile and install OPAM, Coq, Coq libraries and Coq plugins on MacOS,

Windows and many Linux distributions in a reliable w...

**Arthur Azevedo de Amorim @arthuraa** posted in **Deriving: a library for deriving class instances for inductive types**

Hi everyone,

I would like to announce the release of Deriving v0.1.0 (GitHub - arthuraa/deriving: Class instances for Coq inductive types with little boilerplate, available as coq-deriving on OPAM). It is a library for automating the generation of MathComp class instances for inductive types, akin to how deriving declarations work in OCaml or Haskell. With a few lines of code, you can derive inst...

**Fabian Kunze @fakusb** posted in **Release of VSCoq 0.3.4 IDE**

We’d like to announce the most recent release of VSCoq 0.3.4, the extension adding Coq support to the Visual Studio Code IDE.

The new version fixes several usability bugs (unreadable narrow proof views, bad performance in huge files of over 3000 lines and some other glitches that were only fixed by restarting) and improves several other aspects, see changelog.

We of course still have all the oth...

**Matthieu Sozeau @mattam82** posted in **Equations 1.2.4 release**

I am happy to announce availability of equations 1.2.4, a bugfix release that improves the compatibility of equations with ssreflect’s tactics and has more robust automated proofs of the elimination principle associated to a definition, including when functional extensionality is disabled. This version is available on opam for Coq 8.13, 8.12 and 8.11 and should be entirely backwards compatible.

P...

**Guillaume Melquiond @silene** posted in **Interval 4.2, now with plotting**

The 4.2.0 release of Interval departs a bit from the previous versions in that it is no longer just about proving properties of real-valued expressions. It can now be used to investigate such properties visually, that is, it can now plot function graphs from inside Coq. The main difference with traditional computer algebra systems is that a plot is not a list of points obtained by sampling, it is ...

**@Maximilian_Haslbeck** posted in **Proof Ground 2021 - Call for Problems**

Dear Coq enthusiasts,

we are organizing another edition of the proving competition workshop

"Proof Ground", which will take place virtually just before ITP 2021.

Please take noteof our Call for Problems, and spread the word!

**Théo Zimmermann @Zimmi48** posted in **Renaming Coq**

Dear members of the Coq community,

The Coq development team acknowledges the recent discussions (started on the Coq-Club mailing list) around Coq’s logo and name.

We wish to thank everyone that participated in these discussions. Testimonies from people who experienced harassment or awkward situations, reports about students (notably women) who ended up not learning / using Coq because of its nam...

**@Danil_Annenkov** posted in **Certified Elm web apps**

Dear Coq community,

I would like to share a project related to the Elm functional programming language.

As part of ConCert (https://github.com/AU-COBRA/ConCert), we have developed an extraction pipeline that allows for generating Elm code.

We have several simple examples/tests here https://github.com/AU-COBRA/ConCert/blob/master/extraction/examples/ElmExtractExamples.v.

A more “domain-specific...

**Enrico Tassi @gares** posted in **Release of the Coq platform 2021.02.1 - Coq 8.13.2**

Dear Coq community,

the Coq development team is proud to announce the immediate

availability of the Coq Platform version 2021.02.1, based on Coq

8.13.2.

The Coq platform is a distribution of the Coq proof assistant together

with a selection of Coq libraries. See [1] for the project homepage,

and [2] for the new instructions for getting Coq.

For expert users it provides a set of scripts to...

**Christian Doczkal @chdoc** posted in **[CFP] The Coq Workshop 2021 : 2nd Call for Talk Proposals**

The Coq Workshop 2021: 2nd Call for Talk Proposals

Colocated with the 12th conference on Interactive Theorem Proving (ITP 2021)

Online

Find this call online at: The Coq Workshop 2021

We are pleased to invite you to submit talk proposals for the Coq

Workshop 2021, which will be held online on July 2nd, 2021.

The Coq Workshop is part of ITP 2021, which will also be held online.

The Coq Worksh...

**Matthieu Sozeau @mattam82** posted in **Equations 1.3 beta release**

Dear Coq/Equations users, I’m happy to announce version 1.3 of the Equations package.

This is a new major release of Equations, working with Coq 8.13. This version adds an improved syntax (less ; -separation), integration with the Coq-HoTT library and numerous bug fixes. See the reference manual for details.

This version introduces some minor potentially breaking changes along with the following...

**@benediktahrens** posted in **PhD position in HoTT/UF at TU Delft**

A PhD position [1] is open in the Programming Languages group [2] at TU Delft, in the area of HoTT/UF. The student will be supervised by Benedikt Ahrens [3].

Information about the position is available on the dedicated website [1]. If you have any questions or consider applying, please get in touch with Benedikt (benedikt.ahrens@gmail.com).

[1] PhD studentship in homotopy type theory and univale...

**Maximilian Haslbeck @maxhaslbeck** posted in **Proof Ground 2021 - Call for Participation**

Call for participation

Proof Ground 2021

Interactive Proving Contest

June 28, 2021

https://www21.in.tum.de/~wimmers/proofground/

at ITP 2021

Interactive Theorem Proving

June 29 - July 2, 2021, (originally in) Rome, Italy, now fully virtual

https://easyconferences.eu/itp2021/

------------...

**Christian Doczkal @chdoc** posted in **[Call for Participation] July 2nd: The Coq Workshop 2021**

The Coq Workshop 2021: Call for Participation (July 2nd)

Colocated with the 12th conference on Interactive Theorem Proving (ITP 2021)

Online

We are pleased to invite you to participate in the Coq workshop 2021, which will be held online on July 2nd. The Coq workshop is part of ITP 2021.

The Coq Workshop 2021 is the 12th iteration of the Coq Workshop series. The workshop brings together users,...

**@amintimany** posted in **CoqPL 2022: Call for Presentations**

===================================================================

CoqPL 2022`8th International Workshop on Coq for Programming Languages -- January, 2022, co-located with POPL Philadelphia, Pennsylvania, United States CALL FOR PRESENTATIONS https://popl22.sigplan.org/home/CoqPL-20...`

**@jespercockx** posted in **Call for Contributions: WITS 2022**

CALL FOR CONTRIBUTIONS

`1st Workshop on the Implementation of Type Systems WITS 2022 January 22, 2022 Philadelphia, PA, USA https://popl22.sigplan.org/home/wits-2022`

WITS 2022 is the first Workshop on the Implementation of Type

Systems. The workshop will be held on January 22, 2022, in

Phi...

**Théo Zimmermann @Zimmi48** posted in **Call to participate to the WG that will prepare the Coq community survey**

Dear all,

We are about to launch a community-wide survey to get input from the

Coq community and learn more about it. The survey will include things

like demographics, questions about pain points, the roadmap and a

possible renaming.

To prepare this survey, we are setting up a working group. We expect

this working group to coordinate on Zulip and to meet every week for

the next few weeks un...

**Marco Maggesi @maggesi** posted in **School on Univalent Mathematics, Cortona (Italy), July 17-23, 2022**

We are pleased to announce the

School on Univalent Mathematics 2022,

to be held at the Palazzone di Cortona,

Cortona, Italy, July 17-23, 2022Overview

Homotopy Type Theory is an emerging field of mathematics that studies a fruitful relationship between homotopy theory and (dependent) type theory. This relation plays a crucial role in Voevodsky’s program of Univalent Foundations, a new approac...

**Emilio Jesús Gallego Arias @ejgallego** posted in **[ANN] PyCoq preview release**

Dear Coq users and developers,

we are happy to announce the initial release of pyCoq, a Python library to interact with Coq programmatically.The library is very experimental at the moment; expect significant non-backward compatible changes and problems.

We are however doing an early-stage announcement due to:we feel there is significant demand for this kind of library

we’d love to gather ...

**Christian Doczkal @chdoc** posted in **MathComp 1.13.0 released**

We are proud to announce the immediate availability of the Mathematical

Components library version 1.13.0.

The webpage, and documentation, are available at

https://math-comp.github.io/.

This release is compatible with Coq 8.11, 8.12, 8.13 and 8.14.

The main changes are new theories on the diagonalization of matrices,

on bounded sequences, and on the pairwise predicate.

The contributors to t...

**Tiago Cogumbreiro @AssertionError** posted in **Turing: a library to teach Introduction to Theory of Computation**

The Turing project aims to offer the foundations of a course on introduction to the theory of computing. We are formalizing some content of the textbook Introduction to the Theory of Computation, by Michael Sipser.

Our library includes results on

Formal languages: common operators and language equality results

Regular languages: regular expressions, pumping lemma

Turing machines: acceptance, ...

**Tej Chajed @tchajed** posted in **Iris 3.5 and std++ 1.6 released**

We are happy to announce the release of Iris 3.5 and std++ 1.6. Iris is a concurrent separation logic framework for Coq; for an overview of the numerous research projects employing Iris, see https://iris-project.org/. std++ is an extended “standard” library for Coq.

The highlights and most notable changes of Iris 3.5 are:Coq 8.14 is now supported, while Coq 8.12 and Coq 8.13 remain supported.

T...

**Théo Zimmermann @Zimmi48** posted in **Coq Platform 2021.09.0**

Dear Coq community,

On behalf of the Coq development team, the release managers of

Coq 8.13 and Coq 8.14, and the Coq Platform team, we are happy to

announce the immediate availability of the Coq Platform version

2021.09.0.

This is the first Coq Platform release which includes several

versions of Coq. Furthermore, the included package set was

significantly extended since the 2021.02.2 relea...

**Jim Fehrle @jfehrle** posted in **Preview of Ltac Visual Debugger in CoqIDE is now available**

Today’s release of Coq Platform 2021.09.0 includes a preview of the Ltac Visual Debugger on top of Coq 8.14. It’s not merely “interactive”; it’s a visual debugger. It’s described in https://github.com/coq/coq/wiki/Ltac-Debugger-Preview. Let me know your suggestions for it and whether you find it useful.

[image.png]

**Emilio Jesús Gallego Arias @ejgallego** posted in **Coq Hackaton Winter 2022 edition**

Dear all,

We are happy to announce a virtual Coq Hackathon and Working Group on Feb 15th-17th 2022. We were hoping to make this event a hybrid one, but due to the current circumstances it will be online only.

The event is targeted at people who are interested in the implementation of Coq, and would like to learn more about how Coq works and possibly contribute to its development. We hope that th...

**@Cyril_Cohen** posted in **MathComp 1.14.0 released**

We are proud to announce the immediate availability of the Mathematical Components library version 1.14.0.

The webpage, and documentation, are available at https://math-comp.github.io/.

This release is compatible with Coq 8.11, 8.12, 8.13, 8.14 and 8.15.

This release only includes minor changes.

The contributors to this version are: Cyril Cohen, Erik Martin-Dorel, Kazuhiko Sakaguchi, Laurent T...

**Tej Chajed @tchajed** posted in **Iris 3.6 and std++ 1.7 released**

We are happy to announce the release of Iris 3.6 and std++ 1.7. Iris is a concurrent separation logic framework for Coq; for an overview of the numerous research projects employing Iris, see https://iris-project.org/. std++ is an extended “standard” library for Coq.

The highlights and most notable changes of Iris 3.6 are:Coq 8.15 is now supported, while Coq 8.13 and Coq 8.14 remain supported.

...

**Théo Zimmermann @Zimmi48** posted in **Coq Platform 2022.01.0**

Dear Coq community,

On behalf of the Coq development team, the release managers of

Coq 8.14 and Coq 8.15, and the Coq Platform team, we are happy to

announce the immediate availability of the Coq Platform version

2022.01.0.

Release highlights:

- An important newly added package, coq-hammer, provides the hammer

tactic, which uses external ATPs (Automated Theorem Provers) to

automatically cr...

**Théo Zimmermann @Zimmi48** posted in **Coq community survey 2022**

Dear Coq community,

The Coq team requests your participation in the Coq community survey 2022. This survey will help get an updated picture of the Coq community, and help inform future decisions. Participation from every Coq user, learner or prospective user is extremely useful. Please advertise the survey to your students, colleagues, and friends, who are learning or using Coq, but might have mi...

**Enzo Crance @ecranceMERCE** posted in **Trakt 1.0 released**

Hello,

I am glad to announce the first release of Trakt, a generic goal preprocessing tool for proof automation tactics in Coq.Automation tactics in Coq are usually tailored for specific subsets of goals. Yet, when designing their proof statements, Coq users can choose from a range of different inductive types with advantages and drawbacks (computational efficiency, ease of proof, etc). This v...

**Assia Mahboubi @amahboubi** posted in **Workshop: Machine-Checked Mathematics, March 2-4**

Sander Dahmen, Assia Mahboubi, and I have been planning a workshop for a while at the Lorentz Center in Leiden. Pandemic planning is impossible and the workshop keeps changing shape. But we can finally be certain enough to announce: we will be hosting a virtual workshop, Machine-Checked Mathematics, March 2-4! It will happen European afternoons, in an attempt to be accessible by as many people as ...

**Karl Palmskog @palmskog** posted in **The Coq Workshop 2022: Call for Presentation Proposals**

The Coq Workshop 2022: Call for Presentation Proposals

We are pleased to invite you to submit presentation proposals for the Coq Workshop 2022, which will be held in Haifa, Israel on August 12, 2022, as part of FLoC 2022.

The Coq Workshop 2022 is affiliated with ITP 2022, and is the 13th installment of the Coq Workshop series. The workshop brings together users, contributors, and developers of t...

**Talia Ringer @tlringer** posted in **Job opening: visiting research programmer, machine learning for Coq**

Hi all, hope you’re doing well!

I’m hiring a visiting research programmer to build machine learning tools for Coq. This position will mostly be focused on building a usable tool that people can interact with—so some Coq plugin development, some interface design, and some interfacing with machine learning models and frameworks. But the programmer will also be involved in multiple aspects of a cros...

**Théo Zimmermann @Zimmi48** posted in **Proof Assistants SE public beta**

There is now a Stack Exchange Q&A site dedicated to Proof Assistants! Do not hesitate to post and answer Coq questions there (use the coq tag).

**Pierre Marie Pédrot @ppedrot** posted in **Coq 8.16 Release Schedule**

The release schedule for Coq 8.16 has been roughly decided.

The Release Manager will be thy servant, Pierre-Marie Pédrot. Following the release cycle CEP, the first move of the 8.16 will be the official branch out of master, followed by a swift V8.16+rc1 tag. Eventually a V8.16.0 tag will be published when the release process converges.

Tentative schedule:Mid May 2022: 8.16 branch

End of May ...

**Évariste G. @evaristeg** posted in **Upcoming Coq Hackathon and workgroup session**

Hi everyone,

We are organizing an upcoming Coq Hackathon and workgroup session to work on two topics: jsCoq (see the Wiki section here) and the initial implementation of “CoqDB”, an attempt to develop a unified framework where information about Coq objects and metadata can be handled (see the Wiki section here).

At this time, we would like to define the date for this upcoming event. Please use t...

**Évariste G. @evaristeg** posted in **Upcoming Coq Hackathon and workgroup session on Thursday, March 31st**

Hi everyone,

Our next Coq Hackathon and workgroup session is happening this Thursday, March 31st, 14h00 Paris time (08h00 NYC time - 05h00 Seattle time). Please join us! We’ll be focusing on two topics: jsCoq (see the Wiki section here) and the initial implementation of “CoqDB”, an attempt to develop a unified framework where information about Coq objects and metadata can be handled (see the Wiki...

**Ana Borges @ana-borges** posted in **PhD student position on proof theory and verification of legal software in Coq, Barcelona (Deadline: April 3rd, AoE)**

The University of Barcelona offers a 3 year PhD position in collaboration with the Catalan industrial sector. The industrial component of the PhD revolves around the development and verification of legal software in Coq within Formal Vindications SL (formalvindications.com). This work will be complemented with the formalisation of parts of logic/mathematics and possibly research of a less applied ...

**@shinnar** posted in **FormalML: A library for (general) probability**

We would like to announce our (open source and publicly available)

library for working with general probability spaces in Coq. Starting

with Sigma-Algebras, it works its way up to general expectation, and

general conditional expectation (defined over any nonnegative or

finite expectation measurable random variable), with the expected

properties.

This is used for various applications, such a...

**Guillaume Melquiond @silene** posted in **Interval 4.5, now with root finding**

The 4.5.0 release of Interval comes with a new pair of tactics: root and root_intro. Contrarily to the original tactics interval and integral (and their *_intro counterparts), root does not compute a new enclosure by forward interval analysis. Instead, it refines an existing enclosure according to a given equation using Newton’s method.

Let us illustrate the root tactic with the quintic equation x...

**Marco Maggesi @maggesi** posted in **School on Univalent Mathematics, Cortona (Italy), July 17-23: Application deadline 15 April**

We are pleased to announce the

School on Univalent Mathematics 2022,

to be held at the Palazzone di Cortona, Cortona, Italy, July 17-23, 2022Application deadline

15 April 2022Overview

Homotopy Type Theory is an emerging field of mathematics that studies a fruitful relationship between homotopy theory and (dependent) type theory. This relation plays a crucial role in Voevodsky’s program of ...

**Théo Zimmermann @Zimmi48** posted in **Coq Platform release 2022.04.0**

Dear Coq community,

On behalf of the Coq development team, the release manager of Coq

8.15, and the Coq Platform team, we are happy to announce the

immediate availability of the Coq Platform version 2022.04.0.

Release highlights:

- Coq 8.15 is now stable and the default version proposed in the Coq Platform.
- Flocq has been upgraded to major version 4.0.0. Flocq 3 is still

available under t...

**@UlrikBuchholtz** posted in **HoTTEST Summer School July+August 2022**

We’re delighted to announce the HoTTEST Summer School, part of the

Homotopy Type Theory Electronic Seminar Talks, which will take

place online everywhere in the world during the months of July and

August 2022.

The school will run both synchronously and asynchronously. The lectures

will be delivered live (between 2:30-4pm UTC) and paired with various

tutorial sessions run by teaching assistan...

**Alex Gryzlov @alex.gryzlov** posted in **HTT 1.0 released**

Hello,

We would like to to announce the first public release of Hoare Type Theory (HTT), a verification system for reasoning about sequential heap-manipulating programs based on Separation logic. It is available on Github and can be installed via opam.

HTT incorporates Hoare-style specifications via preconditions and postconditions into types. A Hoare type ST P (fun x : A => Q) denotes computati...

**Maxime Dénès @maximedenes** posted in **CompCert receives ACM Software System Award**

After Coq in 2013, CompCert receives the 2021 ACM Software System Award. Congrats to everybody involved!

**@erikmd (Erik Martin Dorel)** posted in **ANN: (docker-coq: Bump to Debian 11) & (docker-coq-action: Remove ocaml_version: "minimal")**

TL;DR: if you use docker-coq images and (install Debian packages manually or use the docker-coq-action with ocaml_version: "minimal"), then you could be impacted by the upgrade planned on next Monday 2022-06-27.

Up to now, all changes done in docker-coq and docker-coq-action repositories have been done with a special focus on backward compatibility.

However, two upcoming changes might impact Do...

**@Marcus_Zibrowius** posted in **Full-time positions in formalized mathematics at Düsseldorf**

Heinrich Heine University Düsseldorf is seeking two full-time postdocs

within the projectADAM: Anticipating the Digital Age of Mathematics,

which is funded by the public foundation Stiftung Innovation in der Hochschullehre. The core aim of

the project is to develop, test and publish online resources that

provide an introduction to formalized mathemati...

**@Zimmi48 (Théo Zimmermann)** posted in **Coq Platform release 2022.04.1**

Dear Coq community,

On behalf of the Coq development team, the release manager of Coq

8.15, and the Coq Platform team, we are happy to announce the

immediate availability of the Coq Platform version 2022.04.1.

Release highlights:

The latest release version of Coq has been updated from 8.15.1 to 8.15.2.

The main supported version is:Coq 8.15.2 with the same package collection as the 202...

**@gares (Enrico Tassi)** posted in **MathComp 1.15.0 released**

We are proud to announce the immediate availability of the Mathematical

Components library version 1.15.0

The webpage, and documentation, are available at

https://math-comp.github.io/.

This release is compatible with Coq 8.13, 8.14, 8.15 and 8.16.

The contributors to this version are: Cyril Cohen, ed-hermoreyes,

Enrico Tassi, Erik Martin-Dorel, Evgenii Moiseenko,

Georges Gonthier, Jonathan ...

**@mattam82 (Matthieu Sozeau)** posted in **MetaCoq 1.0 released**

We are happy to announce release 1.0 of the MetaCoq project for Coq 8.14, 8.15, and 8.16, available both as sources and as opam packages. See the website for a detailed overview of the project, introductory material and related articles and presentations.

MetaCoq integrates Template-Coq, a reification and denotation plugin for Coq terms and global declarations, a Template monad for metaprogrammin...

**@amahboubi (Assia Mahboubi)** posted in **Certified Symbolic-Numeric Computation**

We are pleased to make the following:

First Announcement: on May 22 — May 26, 2023 a workshop on`CERTIFIED AND SYMBOLIC-NUMERIC COMPUTATION`

will take place at ENS de Lyon (Lyon, France).

More information can be found on our website:

https://rtca2023.github.io/pages_Lyon/m2.html

The last twenty years have seen the advent of computer-aided proofs in mathematics and this trend is getting more ...

**@mgbedmar (Mireia González Bedmar)** posted in **FormalV 1.0.0 released**

Formal Vindications S.L. is happy to announce the availability of the FormalV Library version 1.0.0.

The library includes three packages:FV Prim63 to MathComp provides conversions from the Coq primitive integers Uint63 and Sint63 to the MathComp natural and integer numbers nat and int, and vice versa, as well as lemmas to rewrite between their respective operations.

FV Check Range provides tac...

**@blanqui (Frédéric Blanqui)** posted in **EuroProofNet workshop on the development, maintenance, refactoring and search of large libraries of formal proofs**

Dear all,

EuroProofNet is going to organize a workshop on the development, maintenance, refactoring and search of large libraries of formal proofs, on September 23-24, in Tbilisi, Georgia, as part of the Computational Logic Autumn Summit 2022, so in co-location with many other interesting conferences and schools (*). See EuroProofNet Workshop on the development, maintenance, refactoring and searc...

**@palmskog (Karl Palmskog)** posted in **Coq Community Survey 2022 Results: Part I**

Coq Community Survey 2022 Results: Part I

In this post, we give an introduction to the survey and then provide the first part (out of three planned parts) of a result summary. This part is about who is using Coq and in what context.Introduction to the Survey

The Coq Community Survey 2022 was an online public survey conducted during February 2022. Its main goal was to obtain an updated picture ...

**@palmskog (Karl Palmskog)** posted in **Coq Community Survey 2022 Results: Part II**

Coq Community Survey 2022 Results: Part II

This post is the second of three that summarize the results of the Coq Community Survey 2022. Here, we cover how people use Coq, such as their Coq version and IDE choice.

We invite the Coq community to give feedback as replies to this post. In particular, please tell us if the survey questions or plot are unclear in any way.Introduction to the survey

...

**@DonaldKellett (Donald Sebastian Leung)** posted in **Coq 8.15.2 now available on Codewars**

Coq 8.15.2 is now available on Codewars, a community-driven platform featuring code challenges (Kata) for learners of all levels and disciplines. This release includes the base compiler, plus versions of selected packages compatible with Coq Platform 2022.04.1:

Equations

mathcompA list of Coq Kata is available through the Kata search page. The original request for Coq 8.15 support can be found...

**@RalfJ** posted in **Iris 4.0 and std++ 1.8 released**

Hi everyone,

We are happy to announce the release of Iris 4.0 and std++ 1.8. Iris is a concurrent separation logic framework for Coq; for an overview of the numerous research projects employing Iris, see https://iris-project.org/. std++ is an extended “standard” library for Coq.

The highlight of Iris 4.0 is the later credits mechanism, which provides a new way to eliminate later modalities.

Thi...

**@gares (Enrico Tassi)** posted in **MathComp Workshop and Winter School (Dec 5-9 2022)**

Dear Coq enthusiasts,

we are organizing a winter school titled

“The Mathematical Components library”

in Sophia-Antipolis (Nice) from Monday 5th December 2022 to Friday

9th. On Wednesday of the same week we are organizing the workshop

“Mathematical Components - 10 years after the Odd Order Theorem”

The school will be in English and will target master or PhD students

with basic knowle...

**@palmskog (Karl Palmskog)** posted in **Coq Community Survey 2022 Results: Part III**

Coq Community Survey 2022 Results: Part III

This is the third post summarizing the results of the Coq Community Survey 2022. It covers Coq features, tools, plugins and libraries and their respective popularity. The first part focused on who respondents are, while the second part focused on how they use Coq.

We invite the Coq community to give feedback as replies to this post. In particular, plea...

**@Benjamin_Pierce** posted in **New release of Software Foundations**

The Software Foundations team is delighted to announce a new release of the entire SF series.

Software Foundations is a set of textbooks on logic, programming language theory, functional algorithms, and machine-assisted proofs of functional and imperative programs, all 100% formalized and machine-checked in Coq. This release brings all volumes up to date with the current release of Coq (8.15.2) a...

**@palmskog (Karl Palmskog)** posted in **Volunteer interim maintainers needed for VsCoq**

The Coq core team and Coq-community are looking for volunteer interim maintainers of the VsCoq project.

VsCoq is an extension of the Visual Studio Code (VS Code) editor to support Coq source files and interaction with Coq. In a recent survey of Coq users, around one third of respondents reported that they use VS Code for Coq.

As described in the public roadmap, VsCoq developers are currently foc...

**@amahboubi (Assia Mahboubi)** posted in **Two positions at the University of Bonn in the field of formal mathematics and computer assisted theorem proving**

See University of Bonn, Hausdorff Center for Mathematics

The cluster of excellence Hausdorff Center for Mathematics (HCM) at the University of Bonn brings together researchers in mathematics and its applications. In this framework the center is looking forward to filling in the area of theoretical mathematics

a permanent W2-Professorship and

a temporary W2-Professorship for five years

in the f...

**@Zimmi48 (Théo Zimmermann)** posted in **Coq Platform 2022.09.0 (including beta version for Coq 8.16.0 and a updated and extended package pick)**

Dear Coq community,

On behalf of the Coq development team, the release manager of Coq

8.16, and the Coq Platform team, we are happy to announce the

immediate availability of the Coq Platform 2022.09.0 release.

Release highlights:

The latest version of Coq has been updated from 8.15.2 to 8.16.0,

with a beta package pick.Many new packages have been added. In particular, Itauto,

mathcomp...

**@gares (Enrico Tassi)** posted in **MathComp Workshop and Winter School (Dec 5-9 2022) - second call**

Dear Coq enthusiasts,

we are organizing a winter school titled

“The Mathematical Components library”

in Sophia-Antipolis (Nice) from Monday 5th December 2022 to Friday

9th. On Wednesday of the same week we are organizing the workshop

“Mathematical Components - 10 years after the Odd Order Theorem”

The school will be in English and will target master or PhD students

with basic knowle...

**@spitters (Bas Spitters)** posted in **PhD/postdoc vacancy on the verification of cryptographic protocols at Aarhus University**

We are looking for a strong PhD-candidate at Aarhus University (DK).

( There may be possibilities for a postdoc position. Please contact me

for more information. )

A description of the project can be found below.

deadline 1 November 2022 at 23:59 CET.

https://phd.nat.au.dk/for-applicants/open-calls/november-2022/privacy-preserving-and-software-independent-voting-protocols

The PhD positions i...

**@jasonrute** posted in **Postdoc and Internship positions at IBM Research**

IBM Research is looking for both a post-doc and a summer intern, both to work at the intersection of AI and interactive theorem proving with me and others.

Post-doc position:

Start Jan 2023 (or later if negotiated)

Based in Yorktown Heights, NY, USA

See here for the post-doc position description and application link.

We are looking to make a decision very soon. If you are interested please do b...

**@silene (Guillaume Melquiond)** posted in **Interval 4.6, now with decimal enclosures and floating-point rounding operators**

The 4.6.0 release of Interval comes with two new features.

First, the *_intro tactics as well as their degenerate forms (for tactic-in-term uses) can now represent enclosure bounds using decimal numbers, for extra readability. This feature is enabled by passing the i_decimal option to the tactics.

From Coq Require Import Reals.

From Interval Require Import Tactic.

Open Scope R_scope.Definition...

**@Matafou (Pierre Courtieu)** posted in **ProofGeneral release 4.5**

We are happy to announce the release of Proof General version 4.5.

Proof General is a generic Emacs mode for proof assistants. It can be instantiated for the proof assistant of your choice, and is supplied ready-customized for Coq, PhoX, EasyCrypt, Qrhl-tool.

Website: https://proofgeneral.github.io/

Core maintainers e-mail: proof-general-maintainers@groupes.renater.fr

Proof General includes th...

**@gares (Enrico Tassi)** posted in **MathComp Workshop and Winter School (Dec 5-9 2022) - last call**

Dear Coq enthusiasts,

we are organizing a winter school titled

“The Mathematical Components library”

in Sophia-Antipolis (Nice) from Monday 5th December 2022 to Friday

9th. On Wednesday of the same week we are organizing the workshop

“Mathematical Components - 10 years after the Odd Order Theorem”

The school will be in English and will target master or PhD students

with basic knowle...

**@CohenCyril (Cyril Cohen)** posted in **Job offer - postdoc position in Inria Sophia Antipolis**

We offer a 1-year long postdoc position from March 1st, in the context of the CoREACT french ANR.

All the details are in the following document http://cyrilcohen.fr/CoREACT1.pdf

Note that the application link in the document is not valid yet and should be active by January.

Best wishes

**@dankoi** posted in **Position in software dependability at the French space agency CNES - Toulouse**

Bonjour,

Une poste en assurance de sûreté de fonctionnement du logiciel est ouverte au CNES-Toulouse :N’hésitez pas à postuler si ces sujets vous intéressent.

Cordialement,

Danko ILIK

**@ejgallego (Emilio Jesús Gallego Arias)** posted in **Coq LSP release 0.1.2**

Dear all,

we are happy to announce the release of coq-lsp 0.1.2, a new language Server and VSCode extension for the Coq interactive proof assistant.

coq-lsp aims to provide a modern and streamlined proof-editing experience, supporting incremental checking, markdown documents, and an error recovery strategy friendly to step wise development of proof documents.

The 0.1.2 release has been signific...

**@karthikbhargavan** posted in **Verification Jobs @ Cryspen (France/Germany)**

Cryspen is a small research-oriented company that seeks to apply formal verification tools to build high-assurance production-ready cryptographic software. We have a few open roles at Cryspen right now in Germany and in France.

In particular, we are looking to hire a Software Verification Engineer who will focus on implementing and verifying high-assurance software, which includes writing and mai...

**@lthery (Laurent Théry)** posted in **VsCoq 0.3.7 is out**

Vscoq 0.3.7 is out!!

Change log :0.3.7

add an option to disable “Proof View Diff” (#321 by @Blaisorblade)

add logo as icon to coq file (#302 by dlesbre)

add hover provider (#300 by dlesbre)

add color to more keywords (#299 by dlesbre)

various improvements and consolidations (by Huỳnh Trần Khanh)

fixed leaking error message when only shelved goals remain (#268 by fakusb)

**@Zimmi48 (Théo Zimmermann)** posted in **Coq Platform 2022.09.1 release with Coq 8.16.1**

Dear Coq community,

On behalf of the Coq development team, the release manager of Coq 8.16, and the Coq Platform team, we are happy to announce the immediate availability of the Coq Platform 2022.09.1 release.

Release highlights:

- The latest version of Coq has been updated to 8.16.1, which fixes critical soundness bugs with previous versions, and brings other improvements (see the Coq release ...

**@palmskog (Karl Palmskog)** posted in **Volunteer co-maintainer needed for Docker-Coq**

The Coq Team and Coq-community are looking for a volunteer co-maintainer of the Docker-Coq project, which provides Docker container images of many versions of Coq as a service to Coq users.

Docker-Coq is an open source project on GitHub under the BSD-3-Clause license. It maintains definitions of a set of Docker images that provide a basic Coq environment for continuous integration and local use. ...

**@affeldt** posted in **MathComp 1.16.0 released**

We are proud to announce the immediate availability of the Mathematical Components library version 1.16.0.

The webpage, and documentation, are available at https://math-comp.github.io/.

This release is compatible with Coq 8.13, 8.14, 8.15, 8.16, and 8.17.

The contributors to this version are:

Cyril Cohen, Enrico Tassi, Erik Martin-Dorel, Georges Gonthier, Yoshihiro Ishiguro, Julien Puydt, Kazu...

Last updated: Feb 06 2023 at 05:03 UTC