Code Monkey home page Code Monkey logo

coq.github.io's Introduction

Coq website

This repository contains the static pages of the Coq website

make
make run

Pre-html sources are in pages/ and news/, while final html files will be assembled in dest/.

Note that links may not work locally, and pages will have to have .html appended to the URL in order to view them.

Prerequisites

The html files are pre-processed by Yamlpp. A copy of yamlpp is included in this repository, we simply need an OCaml toplevel to run it as a script. If you further modify the source file yamlpp.mll to customize the pre-processing, you will also need ocamllex to regenerate yamlpp.ml.

How to edit an existing page?

  • Edit the source file containing the webpage.
  • Run make and check that the produced file is ok. If that may help, make run launches a small local webserver
  • Commit your change and push it to the main repository The update of coq.inria.fr should then be automatic (TODO)

How to create a new page?

  • Add your new file in pages/. File name is up to you, but please avoid strange ones. Files in pages/ will be pre-processed by Yamlpp (see yamlpp-*/README for me details). Basically, to be uniform with the other pages of the site, your file should look like:

    <#def TITLE> your page title </#def>
    <#include "incl/header.html">
    

    with your HTML code corresponding roughly to the inner of the HTML body:

    <#include "incl/footer.html">
    

    In addition, you could add just after the TITLE two other macro definitions:

    • HEAD : anything in it will be added at the end of the <head> section
    • PATH : some code displayed before the title of your page, usually a sequence of links to your page ancestors. See Drupal's breadcrumb. By default: <a href="/">Home</a>.
  • Ensure that your page is built and installed. Normally, this should be automatic now. You could add multiple lines to have multiple aliases for the same page.

    Nota: for pages converted from Drupal, the relevant part of the url is now a directory, in with we place an index.html. This approach is also recommended for new pages, but not mandatory.

  • make, verify, commit, push as for the edition of an existing page below.

And for news?

  • Add a new file in news/ with the file name of your liking. You can for instance copy news/template and adapt it, or any existing news files. See news/template for details about the expected syntax.

  • In the file NEWSINDEX, add your news title (filename) at the top (this list is sorted in chronological order, most recent first).

  • make, verify, commit, push as usual

coq.github.io's People

Contributors

achlipala avatar alizter avatar amahboubi avatar aspiwack avatar brandenburg avatar clarus avatar cohencyril avatar gares avatar gasche avatar herbelin avatar jnarboux avatar letouzey avatar lysxia avatar mattam82 avatar maximedenes avatar mdnahas avatar palmskog avatar pirbo avatar ppedrot avatar psteckler avatar robbertkrebbers avatar silene avatar skyskimmer avatar strub avatar tchajed avatar thery avatar vbgl avatar whonore avatar ybertot avatar zimmi48 avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

coq.github.io's Issues

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.

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

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

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...

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.

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.

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).

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.

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.

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 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)

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.

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"'

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.

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.

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.

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:

Screenshot from 2021-02-09 10-59-28

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.

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:

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?

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.

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)

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:

2022-03-09_18-42-13_Screenshot_coq_inria_fr

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

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.)

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.