Bas Spitters (May 29 2020 at 08:49): Bas Spitters (May 29 2020 at 08:49):I just noticed this is stuck in 8.8.0. Does anyone know why?
https://softwarefoundations.cis.upenn.edu/
Karl Palmskog (May 29 2020 at 08:51):that's a good point, e.g., LF fails very quickly on 8.11.1.
Bas Spitters (May 29 2020 at 08:56):It might be something to move to the coq-community, if they are not maintaining it.
Karl Palmskog (May 29 2020 at 09:01):unfortunately, I believe a decision has been made to not develop SF publicly. I guess it's possible to do a fork, but it wouldn't look good for the community in general.
Karl Palmskog (May 29 2020 at 09:03):to the best of my knowledge, SF is in Coq's CI, so there is a revision working with 8.11.1 in there (in a private repo).
Christian Doczkal (May 29 2020 at 09:09):That sounds really weird. Indeed, I recall an intern at STAMP being upset because she wanted to learn Coq from SF while working on a modern development. The only reason I can think of is that they continued the development internally and that new (not yet to be released) content got intertwined with the adaptations needed to keep the published version running in recent versions of Coq. Maybe someone can inquire?
Karl Palmskog (May 29 2020 at 09:14):ping @Li-yao who I have seen active here and is at UPenn and thus may know more, e.g., whom we should talk to about this issue.
Théo Zimmermann (May 29 2020 at 09:38):@Bas Spitters SF is actually maintained and even part of Coq's CI. This repository contains an up-to-date version: https://github.com/DeepSpec/sf. The URL that is shown in this repo https://deepspec.github.io/sf/ also contains more up-to-date versions (at least they are claimed to be compatible with Coq 8.9.1 but might even be the one that compile with Coq 8.12).
Théo Zimmermann (May 29 2020 at 09:40):Karl Palmskog said:
unfortunately, I believe a decision has been made to not develop SF publicly. I guess it's possible to do a fork, but it wouldn't look good for the community in general.
The reason SF is developed in a private repo is because this repo contains the solutions to the exercises but these solutions are not supposed to be generally available on the web.
Bas Spitters (May 29 2020 at 09:42):@Théo Zimmermann Thanks! If it is in CI, should we know whether it compiles with 8.12 ?
Théo Zimmermann (May 29 2020 at 09:43):The version that is in the repo does compile with Coq 8.12 for certain.
Théo Zimmermann (May 29 2020 at 09:43):The one that is on the https://deepspec.github.io/sf/ website may or may not be the exact same version (it likely is).
Bas Spitters (May 29 2020 at 09:44):So, it could be that the text in the book differs from the sources, but it will compile with 8.12
Karl Palmskog (May 29 2020 at 09:54):so it seems to boil down to advertising the right repo for current Coq. It's not at all easy to find the DeepSpec SF repo/website, e.g., doesn't show up on first few pages when googling "software foundations"
Théo Zimmermann (May 29 2020 at 09:58):cc @Yishuai Li who is actively involved in SF (at least from the translating point of view)
Yishuai Li (May 29 2020 at 10:06):The public repo currently is a cutting-edge preview, and as the README has stated, mainly for Coq CI. It could also serve as an issue tracker for non-SF-devs. I'll discuss with Benjamin on advertising this repo officially.
Last updated: Jun 03 2023 at 17:29 UTC