Verified Commit 4e781240 authored by Tej Chajed's avatar Tej Chajed

Stop using coq-community/template

parent 50aba1e3
os: linux
dist: bionic
language: shell
.opam: &OPAM
language: shell
services: docker
install: |
# Prepare the COQ container
docker pull ${COQ_IMAGE}
docker run -d -i --init --name=COQ -v ${TRAVIS_BUILD_DIR}:/home/coq/${PACKAGE} -w /home/coq/${PACKAGE} ${COQ_IMAGE}
docker exec COQ /bin/bash --login -c "
# This bash script is double-quoted to interpolate Travis CI env vars:
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 update -y
opam pin add ${PACKAGE} . -y -n -k path
opam install ${PACKAGE} -y -j ${NJOBS} --deps-only
opam config list
opam repo list
opam list
"
script:
- echo -e "${ANSI_YELLOW}Building ${PACKAGE}...${ANSI_RESET}" && echo -en 'travis_fold:start:script\\r'
- |
docker exec COQ /bin/bash --login -c "
export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m '
set -ex
sudo chown -R coq:coq /home/coq/${PACKAGE}
opam install ${PACKAGE} -v -y -j ${NJOBS}
"
- docker stop COQ # optional
- echo -en 'travis_fold:end:script\\r'
.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="
jobs:
include:
# Test supported versions of Coq via Nix
- env:
- COQ=https://github.com/coq/coq-on-cachix/tarball/master
<<: *NIX
# Test supported versions of Coq via OPAM
- env:
- COQ_IMAGE=coqorg/coq:dev
- PACKAGE=coq-iris-ltac2-string-ident.dev
- NJOBS=2
<<: *OPAM
- env:
- COQ_IMAGE=coqorg/coq:v8.11
- PACKAGE=coq-iris-ltac2-string-ident.dev
- NJOBS=2
<<: *OPAM
# Iris Ltac2 string_to_ident
[![Travis][travis-shield]][travis-link]
[travis-shield]: https://travis-ci.com//iris-ltac2-string-ident.svg?branch=master
[travis-link]: https://travis-ci.com//iris-ltac2-string-ident/builds
This package implements string_to_ident in Ltac2, enabling support for Gallina names in Iris intro patterns (within strings).
## Meta
- Author(s):
- Tej Chajed (initial)
- License: [GNU Lesser General Public License v3.0 or later](LICENSE)
- Compatible Coq versions: v8.11 or later
- Compatible OCaml versions: 4.05.0 or later
- Additional dependencies:
- This package implements string_to_ident in Ltac2, enabling support for Gallina names in Iris intro patterns (within strings).
- Coq namespace: `IrisStringIdent`
- Related publication(s): none
## Building and installation instructions
The easiest way to install the latest released version of Iris Ltac2 string_to_ident
is via [OPAM](https://opam.ocaml.org/doc/Install.html):
```shell
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-iris-ltac2-string-ident
```
To instead build and install manually, do:
``` shell
git clone https://github.com//iris-ltac2-string-ident.git
cd iris-ltac2-string-ident
make # or make -j <number-of-cores-on-your-machine>
make install
```
# Ltac2 implementation of `string_to_ident`
Implements `string_to_ident` using Ltac2, providing support for Gallina names in Iris intro patterns on Coq 8.11 and later.
## Usage
Import this file:
Simply require this file before using the feature in the proof mode:
```coq
From IrisStringIdent Require ltac2_string_ident.
From Iris.proofmode Require Import ltac_tactics.
......
{ pkgs ? (import <nixpkgs> {}), coq-version-or-url, shell ? false }:
let
coq-version-parts = builtins.match "([0-9]+).([0-9]+)" coq-version-or-url;
coqPackages =
if coq-version-parts == null then
pkgs.mkCoqPackages (import (fetchTarball coq-version-or-url) {})
else
pkgs."coqPackages_${builtins.concatStringsSep "_" coq-version-parts}";
in
with coqPackages;
pkgs.stdenv.mkDerivation {
name = "iris-ltac2-string-ident";
propagatedBuildInputs = [
coq
];
src = if shell then null else ./.;
installFlags = "COQMF_COQLIB=$(out)/lib/coq/${coq.coq-version}/";
}
---
fullname: Iris Ltac2 string_to_ident
shortname: iris-ltac2-string-ident
community: false
travis: true
synopsis: >-
Add support for Gallina names in intro patterns to the Iris Proof Mode
description: |-
This package implements string_to_ident in Ltac2, enabling support for Gallina names in Iris intro patterns (within strings).
authors:
- name: Tej Chajed
initial: true
maintainers:
- name: Tej Chajed
nickname: tchajed
opam-file-maintainer: tchajed@mit.edu
opam-file-version: dev
license:
fullname: GNU Lesser General Public License v3.0 or later
identifier: LGPL-3.0-or-later
supported_coq_versions:
text: v8.11 or later
opam: '{>= "8.11"}'
supported_ocaml_versions:
text: 4.05.0 or later
opam: '{>= "4.05.0"}'
dependencies:
- opam:
name: coq-iris
version: '{ (= "dev.2020-03-23.0.3a0d7152") | (= "dev") }'
tested_coq_nix_versions:
- version_or_url: https://github.com/coq/coq-on-cachix/tarball/master
tested_coq_opam_versions:
- version: dev
- version: v8.11
namespace: IrisStringIdent
keywords:
- name: iris
- name: ltac2
categories:
- name: Miscellaneous/Coq Extensions
documentation: |
## Usage
Import this file:
```coq
From IrisStringIdent Require ltac2_string_ident.
From Iris.proofmode Require Import ltac_tactics.
(* TODO *)
```
## Acknowledgements
This implementation strategy was suggested by Robbert Krebbers.
---
opam-version: "2.0"
maintainer: "tchajed@mit.edu"
name: "coq-ltac2-string-ident"
maintainer: "Tej Chajed <tchajed@mit.edu>"
authors: "Tej Chajed <tchajed@mit.edu>"
license: "BSD"
homepage: "https://gitlab.mpi-sws.org/iris/ltac2-string-ident"
bug-reports: "https://gitlab.mpi-sws.org/iris/ltac2-string-ident/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/iris/ltac2-string-ident.git"
version: "dev"
homepage: "https://github.com//iris-ltac2-string-ident"
dev-repo: "git+https://github.com//iris-ltac2-string-ident.git"
bug-reports: "https://github.com//iris-ltac2-string-ident/issues"
license: "LGPL-3.0-or-later"
synopsis: "Add support for Gallina names in intro patterns to the Iris Proof Mode"
description: """
This package implements string_to_ident in Ltac2, enabling support for Gallina names in Iris intro patterns (within strings)."""
build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
"ocaml" {>= "4.05.0"}
"coq" {>= "8.11"}
"coq-iris" { (= "dev.2020-03-23.0.3a0d7152") | (= "dev") }
]
build: [make "-j%{jobs}%"]
install: [make "install"]
tags: [
"category:Miscellaneous/Coq Extensions"
"keyword:iris"
"keyword:ltac2"
"logpath:IrisStringIdent"
]
authors: [
"Tej Chajed"
]
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment