search

coq / coq.github.io

Source files of the coq.inria.fr website
https://coq.inria.fr/
Other
15 stars 37 forks source link

Mention Iris and VST in "What is Coq". #129

Closed robbertkrebbers closed 4 years ago

robbertkrebbers commented 4 years ago

I'd go even further and remove Bedrock (Bedrock is dead and Bedrock2 is still WIP) and replace it with Iris.

Done. I also added VST.

If you are doing the editing in an editor with support for this, could you also split this very long line into multiple ones? Reviewing this very long line is hell on GitHub.

I have manually inserted new lines after each new item.

Zimmi48 commented 4 years ago

Thanks!

robbertkrebbers commented 4 years ago

By the way, maybe we should also remove the link to https://github.com/coq/coq/wiki/List%20of%20Coq%20PL%20Projects This list is not very maintained and most projects there are pretty old.

If you agree with that, I can make an additional PR.

Zimmi48 commented 4 years ago

I don't want to commit on this just yet because it would also mean removing the link to math projects and to teaching. And then what should we do with these three wiki pages?

robbertkrebbers commented 4 years ago

I see, these pages are very old too.

My 2 cents: do not list them on the Coq home page, and make clear on the wiki that they are just there for legacy's sake?

Zimmi48 commented 4 years ago

Is it because you think it's going to be hard to keep such pages up-to-date, or because you think that they lack interest anyway?

robbertkrebbers commented 4 years ago

The former.

I think it would be great to have such pages, but we need someone to actively maintain them.

Zimmi48 commented 4 years ago

OK, then I do agree with your recommendation.