diff --git a/.travis.yml b/.travis.yml index 4e2dcfd..1ee6a05 100644 --- 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 index cd45068..0c955fe 100644 --- 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 make install diff --git a/default.nix b/default.nix index 0e763aa..b0b8c9d 100644 --- 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 index 7722ef9..0bbaad3 100644 --- a/resources/index.html +++ b/resources/index.html @@ -1,11 +1,19 @@ - - + + - - + + Lemma Overloading - + + @@ -13,15 +21,15 @@ - +
View the project on GitHub

About

Welcome to the Lemma Overloading project website! This project is part of coq-community.

-

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.

+

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.

This is an open source project, licensed under the GNU General Public License v3.0 or later.

Get the code

The current stable release of Lemma Overloading can be downloaded from GitHub.

@@ -39,8 +47,8 @@

Documentation

Help and contact

Authors and contributors