The Coq mailing list

[Benoît Viguier <beviguier AT gmail.com>]

HI Michael,

In my case I am stuck at version 8.8.x, and the reason being my
researched depended a lot on specific version of VST & subsequently
Compcert.

When one of the major update of VST broke too many proofs of mine that I
lost the courage to fix them for the n^th time.
I have no qualms about the VST team and I do believe their work is going
towards the right direction. It is just that keeping dependencies
up-to-date is too time consuming.

As a result I froze my dependencies to VST 2.0 and as a consequence
Coq-Compcert 3.2.0 (tweaked to support the installation of .vo files)
and Coq to 8.8.

-- 
Kind regards,

Benoît Viguier
Software Engineer - PhD Student | Cryptography & Formal Methods
Radboud University | Mercator 1, Toernooiveld 212
6525 EC Nijmegen, the Netherlands | www.viguier.nl

On 12/22/20 1:11 PM, Michael Soegtrop wrote:
> Hi Pascal,
>
>> I am responsible for the request of Pierre. He needs an old version
>> for a course he will give at my university.
>
> This doesn't answer the question why he needs an old version. As I
> said, I am interested in the question why people are using old
> versions of Coq, because this might mean we need to improve something.
>
> Best regards,
>
> Michael