Regenerate files from latest templates.

Includes a move from the Gitter badge to the Zulip badge in README.
coq-community · May 29, 2020 · f0e28d2 · f0e28d2
1 parent e19c33d
commit f0e28d2
Show file tree

Hide file tree

Showing 5 changed files with 34 additions and 21 deletions.
diff --git a/.travis.yml b/.travis.yml
@@ -1,6 +1,9 @@
-opam: &OPAM
-  language: minimal
-  sudo: required
+os: linux
+dist: bionic
+language: shell
+
+.opam: &OPAM
+  language: shell
   services: docker
   install: |
     # Prepare the COQ container
@@ -11,6 +14,7 @@ opam: &OPAM
       echo \"Build triggered by ${TRAVIS_EVENT_TYPE}\"
       export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m '
       set -ex  # -e = exit on failure; -x = trace for debug
+      opam repo -a --set-default add coq-extra-dev https://coq.inria.fr/opam/extra-dev
       opam update -y
       opam pin add ${PACKAGE} . -y -n -k path
       opam install ${PACKAGE} -y -j ${NJOBS} --deps-only
@@ -30,12 +34,12 @@ opam: &OPAM
   - docker stop COQ  # optional
   - echo -en 'travis_fold:end:script\\r'
 
-nix: &NIX
+.nix: &NIX
   language: nix
   script:
   - nix-build --argstr coq-version-or-url "$COQ" --extra-substituters https://coq.cachix.org --trusted-public-keys "cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= coq.cachix.org-1:5QW/wwEnD+l2jvN6QRbRRsa4hBHG3QiQQ26cxu1F5tI="
 
-matrix:
+jobs:
   include:
 
   # Test supported versions of Coq via Nix

diff --git a/README.md b/README.md
@@ -3,7 +3,7 @@
 [![Travis][travis-shield]][travis-link]
 [![Contributing][contributing-shield]][contributing-link]
 [![Code of Conduct][conduct-shield]][conduct-link]
-[![Gitter][gitter-shield]][gitter-link]
+[![Zulip][zulip-shield]][zulip-link]
 [![coqdoc][coqdoc-shield]][coqdoc-link]
 [![DOI][doi-shield]][doi-link]
 
@@ -16,8 +16,8 @@
 [conduct-shield]: https://img.shields.io/badge/%E2%9D%A4-code%20of%20conduct-%23f15a24.svg
 [conduct-link]: https://github.com/coq-community/manifesto/blob/master/CODE_OF_CONDUCT.md
 
-[gitter-shield]: https://img.shields.io/badge/chat-on%20gitter-%23c1272d.svg
-[gitter-link]: https://gitter.im/coq-community/Lobby
+[zulip-shield]: https://img.shields.io/badge/chat-on%20zulip-%23c1272d.svg
+[zulip-link]: https://coq.zulipchat.com/#narrow/stream/237663-coq-community-devs.20.26.20users
 
 [coqdoc-shield]: https://img.shields.io/badge/docs-coqdoc-blue.svg
 [coqdoc-link]: https://coq-community.github.io/lemma-overloading/docs/latest/coqdoc/toc.html
@@ -65,7 +65,7 @@ opam install coq-lemma-overloading
 To instead build and install manually, do:
 
 ``` shell
-git clone https://github.com/coq-community/lemma-overloading
+git clone https://github.com/coq-community/lemma-overloading.git
 cd lemma-overloading
 make   # or make -j <number-of-cores-on-your-machine>
 make install

diff --git a/default.nix b/default.nix
@@ -31,5 +31,5 @@ pkgs.stdenv.mkDerivation {
 
   src = if shell then null else ./.;
 
-  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
+  installFlags = "COQMF_COQLIB=$(out)/lib/coq/${coq.coq-version}/";
 }
diff --git a/resources/index.html b/resources/index.html
@@ -1,27 +1,35 @@
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
-<html xmlns="http://www.w3.org/1999/xhtml">
+<!DOCTYPE html>
+<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en">
 <head>
-  <meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
-  <meta http-equiv="Content-Style-Type" content="text/css" />
+  <meta charset="utf-8" />
   <meta name="generator" content="pandoc" />
+  <meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes" />
   <title>Lemma Overloading</title>
-  <style type="text/css">code{white-space: pre;}</style>
+  <style>
+      code{white-space: pre-wrap;}
+      span.smallcaps{font-variant: small-caps;}
+      span.underline{text-decoration: underline;}
+      div.column{display: inline-block; vertical-align: top; width: 50%;}
+  </style>
+  <!--[if lt IE 9]>
+    <script src="//cdnjs.cloudflare.com/ajax/libs/html5shiv/3.7.3/html5shiv-printshiv.min.js"></script>
+  <![endif]-->
   <style type="text/css"> body {font-family: Arial, Helvetica; margin-left: 5em; font-size: large;} </style>
   <style type="text/css"> h1 {margin-left: 0em; padding: 0px; text-align: center} </style>
   <style type="text/css"> h2 {margin-left: 0em; padding: 0px; color: #580909} </style>
   <style type="text/css"> h3 {margin-left: 1em; padding: 0px; color: #C05001;} </style>
   <style type="text/css"> body { width: 1100px; margin-left: 30px; }</style>
 </head>
 <body>
-<div id="header">
+<header id="title-block-header">
 <h1 class="title">Lemma Overloading</h1>
-</div>
+</header>
 <div style="text-align:left">
 <img src="https://github.githubassets.com/images/modules/logos_page/Octocat.png" height="25" style="border:0px"> <a href="https://github.com/coq-community/lemma-overloading">View the project on GitHub</a> <img src="https://github.githubassets.com/images/modules/logos_page/Octocat.png" height="25" style="border:0px">
 </div>
 <h2 id="about">About</h2>
 <p>Welcome to the Lemma Overloading project website! This project is part of <a href="https://github.com/coq-community/manifesto">coq-community</a>.</p>
-<p>This project contains Hoare Type Theory libraries which demonstrate a series of design patterns for programming with canonical structures that enable one to carefully and predictably coax Coq's type inference engine into triggering the execution of user-supplied algorithms during unification, and illustrates these patterns through several realistic examples drawn from Hoare Type Theory. The project also contains typeclass-based re-implementations for comparison.</p>
+<p>This project contains Hoare Type Theory libraries which demonstrate a series of design patterns for programming with canonical structures that enable one to carefully and predictably coax Coq’s type inference engine into triggering the execution of user-supplied algorithms during unification, and illustrates these patterns through several realistic examples drawn from Hoare Type Theory. The project also contains typeclass-based re-implementations for comparison.</p>
 <p>This is an open source project, licensed under the GNU General Public License v3.0 or later.</p>
 <h2 id="get-the-code">Get the code</h2>
 <p>The current stable release of Lemma Overloading can be <a href="https://github.com/coq-community/lemma-overloading/releases">downloaded from GitHub</a>.</p>
@@ -39,8 +47,8 @@ <h2 id="documentation">Documentation</h2>
 <h2 id="help-and-contact">Help and contact</h2>
 <ul>
 <li>Report issues on <a href="https://github.com/coq-community/lemma-overloading/issues">GitHub</a></li>
-<li>Chat with us on <a href="https://gitter.im/coq-community/Lobby">Gitter</a></li>
-<li>Discuss with us on Coq's <a href="https://coq.discourse.group">Discourse</a> forum</li>
+<li>Chat with us on <a href="https://coq.zulipchat.com/#narrow/stream/237663-coq-community-devs.20.26.20users">Zulip</a></li>
+<li>Discuss with us on Coq’s <a href="https://coq.discourse.group">Discourse</a> forum</li>
 </ul>
 <h2 id="authors-and-contributors">Authors and contributors</h2>
 <ul>

diff --git a/resources/index.md b/resources/index.md
@@ -1,5 +1,6 @@
 ---
 title: Lemma Overloading
+lang: en
 header-includes:
   - |
     <style type="text/css"> body {font-family: Arial, Helvetica; margin-left: 5em; font-size: large;} </style>
@@ -47,7 +48,7 @@ Other related publications, if any, are listed below.
 ## Help and contact
 
 - Report issues on [GitHub](https://github.com/coq-community/lemma-overloading/issues)
-- Chat with us on [Gitter](https://gitter.im/coq-community/Lobby)
+- Chat with us on [Zulip](https://coq.zulipchat.com/#narrow/stream/237663-coq-community-devs.20.26.20users)
 - Discuss with us on Coq's [Discourse](https://coq.discourse.group) forum
 
 ## Authors and contributors