coq / coq.github.io

Source files of the coq.inria.fr website

Coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

Installation

Please see https://coq.inria.fr/download. Information on how to build and install from sources can be found in INSTALL.md.

Documentation

The sources of the documentation can be found in directory doc. See doc/README.md to learn more about the documentation, in particular how to build it. The documentation of the last released version is available on the Coq web site at coq.inria.fr/documentation. See also Cocorico (the Coq wiki), and the Coq FAQ, for additional user-contributed documentation.

The documentation of the master branch is continuously deployed. See:

• Reference Manual (master)
• Documentation of the standard library (master)
• Documentation of the ML API (master)

Changes

The Recent changes chapter of the reference manual explains the differences and the incompatibilities of each new version of Coq. If you upgrade Coq, please read it carefully as it contains important advice on how to approach some problems you may encounter.

Questions and discussion

We have a number of channels to reach the user community and the development team:

• Our Zulip chat, for casual and high traffic discussions.
• Our Discourse forum, for more structured and easily browsable discussions and Q&A.
• Our historical mailing list, the Coq-Club.

See also coq.inria.fr/community, which lists several other active platforms.

Bug reports

Please report any bug / feature request in our issue tracker.

To be effective, bug reports should mention the OCaml version used to compile and run Coq, the Coq version (coqtop -v), the configuration used, and include a complete source example leading to the bug.

Contributing to Coq

Guidelines for contributing to Coq in various ways are listed in the contributor's guide.

Information about release plans is at https://github.com/coq/coq/wiki/Release-Plan

Supporting Coq

Help the Coq community grow and prosper by becoming a sponsor! The Coq Consortium can establish sponsorship contracts or receive donations. If you want to take an active role in shaping Coq's future, you can also become a Consortium member. If you are interested, please get in touch!

coq.github.io's Issues

Better OPAM installation instructions

In https://coq.inria.fr/opam-using.html, under Using OPAM to install Coq, there should be instructions to check what version of OPAM you have (opam --version) before the 2 boxes. Also it probably should say that OPAM 2 is preferred (e.g., it's required to install the version of Dune we'll be using) and point you to the upgrade directions.

I had installed Ubuntu 18.04 and ran apt install opam, which gives you the old version. Since I'm familiar with OPAM upgrade, I thought to check the version. Others may not know to do this.

I followed the instructions at https://opam.ocaml.org/doc/Install.html#Ubuntu to do the OPAM upgrade.

HTML version of the tutorial on the website is not up-to-date

The tutorial available here https://coq.inria.fr/tutorial/ has not been updated with the latest version at the time of the 8.7.0 release.

How come that the script uploading the reference manual and the standard library did not also upload the tutorial? Did it use to be uploaded manually?

Why does the synchronization script copies 5 times aliases.footer.conf?

Upon synchronizing the website on the server with the sources in this repository, the content of aliases.footer.conf is copied 5 times to /etc/apache2/aliases.conf. I'm failing to understand how and why.

Something is wrong with https://coq.inria.fr/refman

As notice by @kyoDralliam, https://coq.inria.fr/refman seems to be displayed without any CSS, whereas https://coq.inria.fr/refman/ looks good.

Note that the same is true for https://coq.inria.fr/distrib/current/refman vs https://coq.inria.fr/distrib/current/refman/. Unfortunately, it is to the former that the official website points so it is likely that people are going to encounter the problem soon. I'm going to push a commit adding the trailing dot to the links as a temporary workaround.

Auto-sync not working.

@maximedenes

Lately, I've noticed that I had to manually run the sync.sh script (in sudo mode) on the Coq server to have the changes that were merged in this repo propagated to the website.

Here is the content of /var/deploy/latest-sync.log:

========== GIT PULL ==========
error: insufficient permission for adding an object to repository database .git/objects
fatal: failed to write object
fatal: unpack-objects failed

[Team page] People's names are in two different fonts.

People's names are in two different fonts, how about fixing that? Eg:

The boldface on this one seems inconsistent with the other entries:

Also, more trivially, "Coq-community manager" is capitalized differently for @Zimmi48 and @palmskog

Originally posted by @jfehrle in #172 (comment)

Note that the different fonts correspond to people whose name links to a website or not.

Mention, or link to the list of alternative UI directly on the front page.

Coq has now a growing set of well-maintained UI, and we should advertise this more prominently. The tool page is notoriously hard to update (two PRs have been opened for a while and never merged), completely outdated, and not the right name for a page listing UI anyways.

The list should be available on the front page, or a link should be added to the section "How to get Coq".

The UI to list are:

• Proof General for Emacs;
• Coqtail for Vim;
• VsCoq Reloaded (coq-community version) as soon as it is published on the VSCode marketplace which hopefully will be soon;
• JsCoq;
• The Coq Jupyter kernel.

See also coq/coq#10709.

Coq's website 404 page is not found.

Coq's Apache configuration files define a 404 page:

  ## Customized error messages.
  ErrorDocument 404 /notfound.html

in /etc/apache2/main.conf but this /notfound.html page does not exist. This leads the server to display a 404 page like:

The requested URL /static/notfound.html was not found on this server.

Additionally, a 404 Not Found error was encountered while trying to use an ErrorDocument to handle the request.

This is pretty lame...

Please publish documentation for offline viewing

Version

8.x

Operating system

N/A

Description of the problem

@Zimmi48 said:

We don't provide [documentation as downloadable PDFs] anymore.
It doesn't mean we can't debate whether we should provide a PDF but it should be its own issue then.

This is that issue 🙂

For users who wish to do any of the following things, it would be extremely helpful if the Coq maintainers published Coq's documentation as PDFs on the coq.inria.fr website:

• read the documentation without an Internet connection;
• print the documentation to read it without a computer;
• diff their own documentation builds against "official" builds (e.g. using diffpdf);
• view the documentation in PDF format without having to install all of the documentation build process's prerequisites in addition to the Coq software's build process's prerequisites.

coq.inria.fr is down

Help! Can't do any work as I need the reference manual.

This repository is looking for a maintainer

Who would be willing to watch this repository and provide feedback to people who open pull requests and merge them swiftly when they are ready?
Neither @maximedenes, nor I have time to do that but the lack of a maintainer makes contributing to the website a very difficult and frustrating task.

@ybertot: would you be willing to do this?
Or should it be @letouzey? (But I'm under the impression that Pierre is already overwhelmed by other tasks and has a lot to do with Coq anyway.)

"||" doesn't render in the tutorial

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#4996
From: @chris-martin
Reported version: 8.5
CC: @silene

Update version info on "Installing Coq via OPAM"

https://coq.inria.fr/opam/www/using.html gives the code

export OPAMROOT=~/opam-coq.8.6 # installation directory
opam init -n --comp=4.01.0 -j 2 # 2 is the number of CPU cores
opam repo add coq-released http://coq.inria.fr/opam/released
opam install coq.8.6 && opam pin add coq 8.6

It should be updated from 8.6 to 8.7. I couldn't find any file named using.html in the present repo; please let me know if it is the wrong repo or the file is generated dynamically.

What shall we do with the distrib directory?

On the Coq website, the https://coq.inria.fr/distrib/ directory holds about 16 Gio of History. Do we want to keep it online? If so, where and how? In particular, it does not fit well with a move to a lighter web infrastructure as envisioned in #82.

Notice that recent releases are already available at https://github.com/coq/coq/releases/.

NB: I know that the manual of the current version is also stored in that directory; it does not count as “History” and I’m taking care of integrating it to the reworked website. Thus this is not the matter of this PR. Thanks.

Suggestions welcome.

The news infrastructure could be cleaned up from the Makefile.

#169 removed our news system in the left bar and archived the existing news items as "Old news". The news infrastructure is left-over and could be partially cleaned up.

Opam using: warn users that you need to install CoqIDE with opam if you want it to know about Coq packages.

A very frequent error users do is that they start installing Coq + CoqIDE with their preferred package manager, then they install opam and coq packages through opam. These packages depend on Coq but not on CoqIDE, so when they launch CoqIDE, it will be the system-wide installation that they use.

Depending how CoqIDE locates coqtop / coqidetop, several scenarios can then happen:

• CoqIDE locates the system-wide coqtop / coqidetop. In this case, everything works fine but the installed packages are not available (even if they might be when compiling through the console).
• CoqIDE locates the opam installed coqtop / coqidetop. In this case, if the versions match, it will work fine and the installed packages will be available. If the versions do not match, it will fail at launch.

The opam-using page should warn users about this caveat and recommend installing CoqIDE with opam and removing any previous installation. Additionally, the advanced section of the opam-using page could mention the possibility to keep using the system install of CoqIDE provided that the user make sure that they pin the right version of Coq when installing through opam.

This problem would also be resolved, in a much nicer way for the user, if the opam installation procedure could detect that the dependency on coq is already satisfied by a system-wide installation (see also discussion in coq/opam#595 but this is also a much more complex solution to implement, that could require changes to opam itself).

Very minor: rename repo description

I'd suggest the following change:

"Sources files of the coq.inria.fr website (static part) https://coq.inria.fr/" ->
"Source files of the coq.inria.fr website (static part) https://coq.inria.fr/"

Reference manual is still 8.9.0

In https://coq.inria.fr/documentation, the "Reference Manual" links to:

• https://coq.inria.fr/distrib/current/refman/

which is still at 8.9.0.

There is more recent documentation here, is this its new home: https://coq.github.io/doc/ ?

Version Apache configuration files

Right now, configuration files are located in /etc/apache2 on the Coq VPS. These files are not versioned (which is already in itself pretty annoying). Ideally, we would version them within the same repository as the rest of the website's sources (here) and have the script that synchronize the website push them at the right location.

BTW, something else that should be versioned is the above mentioned synchronization script.

Figures is epsent in Reference Manual

at page https://coq.inria.fr/distrib/current/refman/gallina.html (and may be at other pages, I didn't see) figures 1.1, 1.2 and 1.3 are absent

Bug of the website header in the stdlib.

Browsing to https://coq.inria.fr/documentation, then https://coq.inria.fr/distrib/current/stdlib/ changes the header (likely to an older version). It would be good to have a way to ensure that this stays the same (or to make it completely different like in the refman, which is also somewhat okay).

Bottom half of half the #nav links from stdlib pages can't be clicked on

From any page of the stdlib, for example this one, if one tries to click on "Documentation" or "Community" in the top nav bar, the mouse must point to the top 40% or so part of the button. Tested with chrome 88, firefox 85.0.

This is because the sidebar is on top of it:

Possible fix: in styles/barron/style.css, under #nav {, add: z-index: 1;. I would do a PR, but make && make run only gives me 404's. Maybe that's an issue as well.

Continuous integration

We should really set up a CI for this repo. @Zimmi48 could you help setting up a Gitlab CI mirror with coqbot synchro?

Wrong OPAM instructions

The documentation page on using OPAM with Coq is still incomplete and wrong. I proposed two pull-requests to correct it (#17 and #18). Unfortunately, they were reverted with no public explanations and no alternative solutions to the issue.

I propose to just remove the OPAM page from the Coq website for now. Indeed, this is misleading for the users and alternative correct documentations are already available anyway.

https://coq.inria.fr does not work anymore from a standard IPv6 browser

Hi,

Using Firefox-esr on Debian GNU/Linux, I get the following view:

I made a few other tests, and it seems to be the same issue as #157

$ curl -v https://coq.inria.fr
*   Trying 2001:41d0:305:2100::8b43:443...
* Connected to coq.inria.fr (2001:41d0:305:2100::8b43) port 443 (#0)
* ALPN, offering h2
* ALPN, offering http/1.1
* successfully set certificate verify locations:
*  CAfile: /etc/ssl/certs/ca-certificates.crt
*  CApath: /etc/ssl/certs
* TLSv1.3 (OUT), TLS handshake, Client hello (1):
* OpenSSL SSL_connect: Connection reset by peer in connection to coq.inria.fr:443 
* Closing connection 0
curl: (35) OpenSSL SSL_connect: Connection reset by peer in connection to coq.inria.fr:443 

$ curl -v --ipv4 https://coq.inria.fr
*   Trying 51.91.56.51:443...
* Connected to coq.inria.fr (51.91.56.51) port 443 (#0)

…

<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
  "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en">

<head>
  <title>Welcome! | The Coq Proof Assistant</title>

…

Cc @maximedenes @Zimmi48

Add a non-English language documentation category on the website.

I'm thinking that the https://coq.inria.fr/documentation page could benefit from a section listing all the available documentation in other languages than English.

We could list:

• the French and Chinese translation of the Coq'Art
• the Chinese translation of SF (cc @liyishuai)
• the book in Japanese by Manabu Hagiwara and @affeldt
• the video lectures of @ybertot in French that are already mentioned on this page

What else?

No update to the website for the 8.10+beta3 release.

The download link still points to 8.10+beta2, and there is no news.

Typo in nahas_tutorial.v

Very minor. See here https://github.com/coq/www/blob/master/files/nahas_tutorial.v#L1609

There's supposed to be a conjunction and a disjunction but it's two conjunctions.

https://coq.inria.fr/news/ does not mention 8.9+beta1

It does mention 8.8+beta1, and the newest is 8.8.2. I think it should mention 8.9+beta1.

[opam-packaging] missing doc: field in template opam file

In the Creating and Submitting a Package page, it is mentioned that

Documentation should be available (see the doc: field in the Opam metadata)

but no such field is introduced in the template file provided earlier in the page.

Tutorial, distributivity improperly formulated (missing parentheses).

https://coq.inria.fr/tutorial/1-basic-predicate-calculus
End of section "1.3.3 Tauto".
Retrieved at Wed May 29.

Says:
Lemma distr_and : A -> B /\ C -> (A -> B) /\ (A -> C).

Should say:
Lemma distr_and : (A -> B /\ C) -> (A -> B) /\ (A -> C).

Remark:
Both are true and provable, but it seems to me that the former is rather trivial (A, B and C are all assumed true), while only the latter properly expresses distributivity.

coq.inria.fr IPv6 issue?

Description of the problem

This is a follow-up of the issue raised on Zulip, which is still reproducible:

it seems the coq.inria.fr server has some configuration issue w.r.t. IPv6, which can also impact opam update:

$ opam update

<><> Updating package repositories ><><><><><><><><><><><><><><><><><><><><><><>
[default] no changes from https://opam.ocaml.org/
[ERROR] Could not update repository "coq-extra-dev": OpamDownload.Download_fail(_, "Curl failed:
        \"/usr/bin/curl --write-out %{http_code}\\\\n --retry 3 --retry-delay 2 --user-agent opam/2.0.5
        -L -o /tmp/opam-31195-4bcc67/index.tar.gz.part
        https://coq.inria.fr/opam/extra-dev/index.tar.gz\" exited with code 35")
[ERROR] Could not update repository "coq-released": OpamDownload.Download_fail(_, "Curl failed:
        \"/usr/bin/curl --write-out %{http_code}\\\\n --retry 3 --retry-delay 2 --user-agent opam/2.0.5
        -L -o /tmp/opam-31195-9b8556/index.tar.gz.part https://coq.inria.fr/opam/released/index.tar.gz\"
        exited with code 35")

To be more precise, here is an example session on a Linux environment where DNS addresses appear to resolve to IPv6 first:

$ timeout -s SIGINT 10s curl -s -v -o /dev/null https://coq.inria.fr
* Rebuilt URL to: https://coq.inria.fr/
*   Trying 2001:41d0:305:2100::8b43...
* TCP_NODELAY set
* Connected to coq.inria.fr (2001:41d0:305:2100::8b43) port 443 (#0)
* ALPN, offering h2
* ALPN, offering http/1.1
* Cipher selection: ALL:!EXPORT:!EXPORT40:!EXPORT56:!aNULL:!LOW:!RC4:@STRENGTH
* successfully set certificate verify locations:
*   CAfile: /etc/ssl/certs/ca-certificates.crt
  CApath: /etc/ssl/certs
* TLSv1.2 (OUT), TLS header, Certificate Status (22):
} [5 bytes data]
* TLSv1.2 (OUT), TLS handshake, Client hello (1):
} [512 bytes data]


$ timeout -s SIGINT 10s ping coq.inria.fr
PING coq.inria.fr(2001:41d0:305:2100::8b43 (2001:41d0:305:2100::8b43)) 56 data bytes

--- coq.inria.fr ping statistics ---
10 packets transmitted, 0 received, 100% packet loss, time 9222ms

while it is OK with IPv4:

$ sudo docker run --rm -it debian

root@9d275163954e:/# timeout -s SIGINT 10s ping coq.inria.fr
PING coq.inria.fr (51.91.56.51) 56(84) bytes of data.
64 bytes from 51.ip-51-91-56.eu (51.91.56.51): icmp_seq=1 ttl=58 time=39.1 ms
64 bytes from 51.ip-51-91-56.eu (51.91.56.51): icmp_seq=2 ttl=58 time=298 ms
64 bytes from 51.ip-51-91-56.eu (51.91.56.51): icmp_seq=3 ttl=58 time=59.6 ms
64 bytes from 51.ip-51-91-56.eu (51.91.56.51): icmp_seq=4 ttl=58 time=100 ms
64 bytes from 51.ip-51-91-56.eu (51.91.56.51): icmp_seq=5 ttl=58 time=40.8 ms
64 bytes from 51.ip-51-91-56.eu (51.91.56.51): icmp_seq=6 ttl=58 time=36.8 ms
64 bytes from 51.ip-51-91-56.eu (51.91.56.51): icmp_seq=7 ttl=58 time=416 ms
64 bytes from 51.ip-51-91-56.eu (51.91.56.51): icmp_seq=8 ttl=58 time=132 ms
64 bytes from 51.ip-51-91-56.eu (51.91.56.51): icmp_seq=9 ttl=58 time=36.5 ms
64 bytes from 51.ip-51-91-56.eu (51.91.56.51): icmp_seq=10 ttl=58 time=42.3 ms

--- coq.inria.fr ping statistics ---
10 packets transmitted, 10 received, 0% packet loss, time 13ms
rtt min/avg/max/mdev = 36.528/120.106/415.658/124.943 ms
root@9d275163954e:/# 

ideas on how this could be fixed or workarounded? (especially for the opam update use case)

Bugzilla attachments should live on GitHub

Description of the problem

Currently migrated bugs link to bugzilla attachments. GitHub supports uploading .txt, .log, and .zip files as attachments on issues. I propose that for all bugs with attachments on bugzilla, we archive the files in a .zip file, and attach that to the github issue.

One possible alternative is to special-case .txt, .log, and .v files, to rename foo.v to foo.v.txt, and upload these separately. However, I don't think there's any particular benefit to doing this, as I don't think you can view .txt or .log file attachments in the browser without downloading them.

Expand explanation on opam

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#5207
From: @Lionel-Rieg
Reported version: 8.6

Invisibly redirect some pages to https://coq.github.io/doc?

Since the plan has moved from relying on GH pages for everything to using a new hosting service, but we deploy documentation to https://coq.github.io/doc/, it would be good if https://coq.inria.fr/doc/ could become an alias (invisible redirection) to https://coq.github.io/doc.

I would also suggest that from now on, https://coq.inria.fr/refman and https://coq.inria.fr/stdlib should redirect visibly (so that people stop putting URLs without a version number in their papers) to a URL like https://coq.inria.fr/doc/V8.9.1/refman/ (which would then invisibly redirect to https://coq.github.io/doc/V8.9.1/refman/).

Since we already define the current stable release tag in the website sources, the website infrastructure should use this information to set up this redirection: this would be one less manual step for the RM when preparing a new release. A CI test should however ensure that the webpage has already been deployed before this tag can be updated on the website.

Why does the "Using OPAM to install Coq" instructions set OPAMROOT instead of using switches?

Switches strike me as the more principled way of managing distinct opam environments.

Read the tutorial using Google Translate

Google Translate even targets the code. It changes the code and this significantly reduces the readability. I changed the class attribute to work around this. What do you think of these changes?
https://github.com/ksoda/www/commit/2ad23435b142db4d71d4c1863caedfb8e5393f35

Installation instructions do not work on latest version of opam

Description of the problem

https://coq.inria.fr/opam-using.html says

Depending on your operating system, installing Coq using opam may require you to first install some system packages. The recommended way to determine the names of required system packages is via the opam-depext tool:

opam install opam-depext
opam-depext coq

However, the first command gives

[ERROR] opam-depext unmet availability conditions, e.g. 'opam-version >= "2.0.0~beta5" & opam-version < "2.1"'

Document site deployment setup / server configuration / access.

I'd like this repository to contain a document with all the information needed for a developer to administrate the repository, including how to get ssh access to the new servers.

Replacing list of tutorials on the website with link to awesome list?

Recently, I've proposed that we could extend the list of available Coq documentation on the website to include non-English learning resources: #189.

More recently, I've noticed by looking at https://www.google.com/search?q=coq+proof+course&tbm=vid that there are many Coq video tutorials and this could deserve a category on its own in the documentation page.

Overall, I've reflected that keeping a curated list on the website is hard and maybe this is best done externally, e.g. with an awesome list.

The awesome-coq list already has a resources category: https://github.com/coq-community/awesome-coq#resources.

Another possibility would be to have a separate awesome-coq-learning list dedicated to collecting and curating books, tutorials, videos, etc. about Coq. Separate awesome lists for learning exist in several ecosystems:

• https://github.com/iamericfletcher/awesome-r-learning-resources#readme
• https://github.com/GustavBertram/awesome-common-lisp-learning#readme
• https://github.com/pehapkari/awesome-symfony-education#readme
• https://github.com/fukuball/Awesome-Laravel-Education#readme
• https://github.com/siboehm/awesome-learn-datascience#readme
• https://github.com/ujjwalkarn/Machine-Learning-Tutorials#readme
• https://github.com/guillaume-chevalier/awesome-deep-learning-resources#readme
• https://github.com/gaerae/awesome-algorithms-education#readme

What do @palmskog and @anton-trunov (awesome-coq maintainers) think? Does it sound like a good idea to replace the list being maintained on the website by a link to an awesome list? Should this become a separate awesome list or is awesome-coq the right place to do this? Are non-English resources and video tutorials good categories to add to such list?

And what do @coq/website-maintainers and @coq/core think?

opam-packaging page has not been updated to opam 2.0

cc @gares, @palmskog, @Lysxia

redirect coq.inria.fr/download to the wiki?

https://github.com/coq/coq/wiki#coq-installation seems much more helpful than https://coq.inria.fr/download. Perhaps the short URL should redirect (or at least link) to the wiki page?

In particular, the wiki page includes a breakdown of advice per platform and preferred editor, which is I believe is important for a pleasant onboarding of users who already have preferences between these.

Create developer map page

In the WG, there was discussion about missing visibility of the development team: we said that we should have a page listing current (and past) developers. At some other point, during the discussion on diversity in the Coq community, it was said that it would be good to have a page mapping developers and their topics of interests. Both requirements could probably be adequately combined (and replace the CREDITS file in the main repo). Here is an example of such a page: https://www.sagemath.org/development-map.html

Hidden doc versions?

In https://coq.inria.fr/distrib/ we can see a bunch of versions, but the more recent ones do not appear for some reason (even though eg https://coq.inria.fr/distrib/V8.11.0/stdlib/ exists)

broken links on the website

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#5511
From: @MatejKosik
Reported version: unspecified
CC: @herbelin

stdlib / library duplicate urls

One of https://coq.inria.fr/library/Coq.Init.Wf.html and https://coq.inria.fr/stdlib/Coq.Init.Wf.html should not exist or should redirect to the other.

There should be a Coq YouTube channel

There should be a Coq YouTube channel, and Working Group live-streams should be located there. Finally there should be a link from the website to this channel.

(As discussed at the Coq Working group of October 3rd, 2017)

Remove announcement of Proof Assistants SE in about one month (mid-April).

This is commit 4fed741 from #193.

Missing right curly braces on the faq's bibtex entry

It's a bit of a weird one: the braces show up in the source but not on the website

Moving to GitHub pages

As part of a general strategy to reduce the sysadmin work we have to do in the team, @vbgl and I are preparing the move of the website to GitHub pages.

In this first step, we would keep the infrastructure unchanged, but the deployment would be done automatically using CI.