coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Software foundation for older versions of coq
Date: Mon, 21 Dec 2020 19:28:18 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f174.google.com
Ironport-phdr: 9a23:WQeLRBwiZk5yd2/XCy+O+j09IxM/srCxBDY+r6Qd2u8WIJqq85mqBkHD//Il1AaPAdyEragc0aGP6/qocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTiwbalsIBmqswndudQajZd8Jq0s1hbHv3xEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlTwKPCAl/m7JlsNwjbpboBO/qBx5347Ue5yeOP5ncq/AYd8WWW9NU8BMXCJDH4y8dZMCAOUPPelar4fzqVgAowagCwawC+3i0SNIhmbs0KEmz+gtDQPL0Qo9FNwOqnTUq9D1Ob8IX+C00qbI1y/DYO1L0jrj74jIbwohoe2NXb1ubMra1E4iFxvEjlqOs4zlJS2a2v4RvGic8upgT/6vi285pAFsuTWvycIshZPIhoIR0FzL6SJ5wIMsKNC+VUV0bsKqHoFKuCGGK4t5XNkiQ2dwtSs117ELp562cicFxpooxxPSa+CLfYaK7x/hSuqfLip1iXJndbyxhBu/8UqtxOP8WMS3zFtEoSRIn9fCu30N1BHe7NWMRPV6/kekwzmP1gbT5/leLkAuiaXbK58hwqAumZYJtkTDBCD2lF3rjK+OaEok/O6o5/75bbr7u5+RMZJ/hALmMqk2hMCzHeA1PhINUmWb4+iwybzu8EzjTLlXjPA7na/Uu43AK8sBvK62GQpV354j6xmhCzem18wVnXwdI1JEfBKLlonpO1XTLPzhA/eznlahnThxy/DJOb3hBZrNLnzdn7v7Ybl97EtcxBIyzdBZ+Z1UFqkMLOzvVkL1rtDVDR80Pxapz+vmCdhxzJ4SVGCAD6OBNaPdq16I5uYhI+mWY48VvS7wK+Ak5/Hwl385g0EScbO10psQdXC4BOhmI0SHbnrxmdoBHmIKsRA/TOzuklGNTTlTZ3OqU6Im+j47EJ6mDZvERo21nLOB2z67EoRKaWBCF1CDCmzld56EWvcJcCKdONVtkj0CVbi7So8uzwuitAHgy+kvEu2B0SoB/bnnydI9s+bUjFQ58SF+J8WbyWCECW9uyDAmXTgziZh+rFZnxx+o1rVin/1VCJQH//JESB03c5Xb0vZmCt3vcg3Ed9aNDl2hR4P1UnkKUtstzopWMA5GENK4g0WGhnLyWu5Hp/mwHJUxt5nk8T30Lsd5xWzB0fB43VYjS8pLc2ahg/wmrlWBN8vyi0yc0p2SW+Ec0SrKrjnRyGOPuARZVFc1X/yaATYQYUzZqdm/7UTHHef3VeYXdzBZwMvHEZNkL8XzhAwfFvjmMdXaJWm2njXoCA==

Interesting. Well you need at least ocaml somewhere since opam uses
it. But it can be installed by other means.

Thanks for the remarks all.
Best,
Pierre

Le lun. 21 déc. 2020 à 19:22, Benjamin Pierce <bcpierce AT cis.upenn.edu> a
écrit :
>
> > 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