coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Software foundation for older versions of coq

From: Benjamin Pierce <bcpierce AT cis.upenn.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Software foundation for older versions of coq
Date: Mon, 21 Dec 2020 13:21:46 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=bcpierce AT cis.upenn.edu; spf=Pass smtp.mailfrom=bcpierce AT seas.upenn.edu; spf=None smtp.helo=postmaster AT mail-qt1-f170.google.com
Ironport-phdr: 9a23:DRH29hEaz7Km1ZycsEiETJ1GYnF86YWxBRYc798ds5kLTJ7yps+wAkXT6L1XgUPTWs2DsrQY0rWQ6fi6EjVYu96oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vLhi6txvdutUIjYdtN6o91gXFqWZUdupLwm9lOUidlAvm6Meq+55j/SVQu/Y/+MNFTK73Yac2Q6FGATo/K2w669HluhfFTQuU+3sTSX4WnQZSAwjE9x71QJH8uTbnu+Vn2SmaOcr2Ta0oWTmn8qxmRgPkhDsBOjUk9mzcl85+g79BoB+5uxNwzJPaboGXO/Rwca3Tft0aS3RGUMtKSyxBG4a8Y5cPD+YdP+tVqZT2qVsUrRu5AAmhHP7ixSFOhn/0x6I61uUhEQfb1wI6HtIBrm7Uo8nrO6wPVu2617XHzS3Cb/xIwzfy9JbHfws9rvGNRrJ8a9fRyVExGAPDiFWcs5LqMC6I1ukUtWWQ8uVvW/61hWE9twFxviagxt0qioTRmo8YyU7J+yt9zYsxONG1SkB1b96nHZVQsyyXKYR7T8IsTmxopis0xaEKtJqmcSQW1pkqwx/SZv6ZfoWV7BzuVOCcKip2inJifbKwnRey8U64x+LmTMm7zFZKritbktbSrHwN0AbT6sefRvtg5keuxzCP1wbJ5u5aPE80iKzWIIMizL4ojpcfr1jPEyvslEj1jKKabFgo9+m05+j9f7nrpIOQO5dphg3iMakigMOyDf4mPgUBQ2SX4+ax2bPl8EbkWrtFlOc2nbPcsJ3CJcQUuKq5AwhN34Ym8Rm/DjOm3M0BnXkbMV5JYRyHg5XrNl3SOvz4AvC/g1OjkDdv2f/KJKHuApLILnTbkbfhe6hy61JExQYt0dxS44hYB7IBLf7pR0P8tcDUAgUkPwG23+rrENB92ZkfWWKLDK+ZKqTSsVqQ6+00P+aMfI4VtyjnK/c5+fHjlmQ5lkEHcqmyx5cXdWi4EepgI0Wfe3bjnMoOEXoSsgokUOPqkEGCUSJUZ3uqQ6084Sg7BJu6AofHW4Cim6eM3Dy7H51TfmBJEEqAEXbud4WeWvcDcjieIsF7km9Mab/0QIg4kBqqqQXSyrx9L+OS9DdLm4jk0Y1f6uvRnBQz83RMDsmH2GzFG2t/hmIFXTQ79Kt+ugpg0lqF1+51j+EORo8b3O9ATgpvbc2U9Od9Ed2nAluQLOfMc06vR5CdOR90S9swx9EUZEMkRYe5gxnYmTeyDrkT0bGHGc5tq/+O7z3KP894jk3++uwhgl0hGJUdMGSngutm61GWCdeWywOWkKGlcala1ynIpj/akTi++XpAWQs1ap3rGGgFbxKL/9/4/QXfV7KoD/IqPhYTkcM=

> Another solution would be to ask each student
> to install opam, ocaml, coq and coqide in there account but is it
> really reasonable in terms of disk space?

This is exactly what we do at Penn. ~70 students / year, no complaints.
(Except: We don’t ask them to install OCaml — do you really need it?)

- B

>
> Best,
> Pierre
>
> Le lun. 21 déc. 2020 à 17:57, Clément Pit-Claudel
> <cpitclaudel AT gmail.com> a écrit :
>>
>> On 12/21/20 10:03 AM, Pierre Courtieu wrote:
>>> Hi, I post this question here, since I didn't find a more dedicated
>>> channel. Please feel free to point me to a more appropriate one.
>>>
>>> For technical reasons I need a version of software foundation that
>>> would compile with coq-8.9. What is the standard way to obtain it
>>> please?
>>
>> The web archive has a few old releases:
>> -
>> https://web.archive.org/web/20190317204001/https://softwarefoundations.cis.upenn.edu/lf-current/lf.tgz
>> (09 Jan 2019, Coq 8.8.1)
>> -
>> https://web.archive.org/web/20190317204037/https://softwarefoundations.cis.upenn.edu/plf-current/plf.tgz
>> (08 Feb 2019, Coq 8.8.1)

Re: [Coq-Club] Software foundation for older versions of coq, (continued)
- Re: [Coq-Club] Software foundation for older versions of coq, Clément Pit-Claudel, 12/21/2020
  - Re: [Coq-Club] Software foundation for older versions of coq, Pierre Courtieu, 12/21/2020
    - Re: [Coq-Club] Software foundation for older versions of coq, Benjamin Pierce, 12/21/2020
      - Re: [Coq-Club] Software foundation for older versions of coq, Pierre Courtieu, 12/21/2020
        
        Re: [Coq-Club] Software foundation for older versions of coq, Benjamin Pierce, 12/21/2020
    - Re: [Coq-Club] Software foundation for older versions of coq, Michael Soegtrop, 12/21/2020
      - RE: [Coq-Club] Software foundation for older versions of coq, Fernandez, Matthew, 12/22/2020
        
        Re: [Coq-Club] Software foundation for older versions of coq, Michael Soegtrop, 12/23/2020
        
        RE: [Coq-Club] Software foundation for older versions of coq, Fernandez, Matthew, 12/23/2020
    - Re: [Coq-Club] Software foundation for older versions of coq, Michael Soegtrop, 12/21/2020