-
Notifications
You must be signed in to change notification settings - Fork 46
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
44 changed files
with
426 additions
and
307 deletions.
There are no files selected for viewing
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,76 @@ | ||
# This file was generated from `meta.yml`, please do not edit manually. | ||
# Follow the instructions on https://github.com/coq-community/templates to regenerate. | ||
name: Docker CI | ||
|
||
on: | ||
push: | ||
branches: | ||
- master | ||
pull_request: | ||
branches: | ||
- '**' | ||
|
||
jobs: | ||
build: | ||
# the OS must be GNU/Linux to be able to use the docker-coq-action | ||
runs-on: ubuntu-latest | ||
strategy: | ||
matrix: | ||
image: | ||
- 'coqorg/coq:8.9' | ||
- 'coqorg/coq:8.11' | ||
- 'coqorg/coq:8.12' | ||
- 'coqorg/coq:8.13' | ||
- 'coqorg/coq:8.14' | ||
- 'coqorg/coq:8.15' | ||
- 'coqorg/coq:8.16' | ||
- 'coqorg/coq:8.17' | ||
- 'coqorg/coq:8.18' | ||
- 'coqorg/coq:dev' | ||
fail-fast: false | ||
steps: | ||
- uses: actions/checkout@v3 | ||
with: | ||
submodules: recursive | ||
- uses: coq-community/docker-coq-action@v1 | ||
with: | ||
opam_file: 'coq-ext-lib.opam' | ||
custom_image: ${{ matrix.image }} | ||
after_script: | | ||
startGroup "Test dependants" | ||
PINS=$(opam list -s --pinned --columns=package | xargs | tr ' ' ,) | ||
PACKAGES=`opam list -s --depends-on coq-ext-lib --coinstallable-with $PINS` | ||
for PACKAGE in $PACKAGES | ||
do DEPS_FAILED=false | ||
opam install -y --deps-only $PACKAGE || DEPS_FAILED=true | ||
[ $DEPS_FAILED == true ] || opam install -t $PACKAGE | ||
done | ||
endGroup | ||
set -o pipefail # recommended if the script uses pipes | ||
startGroup "Generate Coqdoc" | ||
make -j`nproc` coqdoc | ||
endGroup | ||
before_script: | | ||
startGroup "Install and configure Clang" | ||
opam install conf-clang | ||
endGroup | ||
startGroup "Workaround permission issue" | ||
sudo chown -R coq:coq . | ||
endGroup | ||
export: 'OPAMWITHTEST OPAMCONFIRMLEVEL' | ||
env: | ||
OPAMWITHTEST: true | ||
OPAMCONFIRMLEVEL: unsafe-yes | ||
- name: Revert permissions | ||
# to avoid a warning at cleanup time | ||
if: ${{ always() }} | ||
run: sudo chown -R 1001:116 . | ||
- uses: actions/upload-artifact@v3 | ||
with: | ||
name: coqdoc | ||
path: html | ||
|
||
# See also: | ||
# https://github.com/coq-community/docker-coq-action#readme | ||
# https://github.com/erikmd/docker-coq-github-action-demo |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,16 @@ | ||
name: 'Close stale issues and PRs' | ||
on: | ||
schedule: | ||
- cron: '30 1 * * 1-5' | ||
|
||
permissions: | ||
issues: write | ||
pull-requests: write | ||
|
||
jobs: | ||
stale: | ||
runs-on: ubuntu-latest | ||
steps: | ||
- uses: actions/stale@v8 | ||
with: | ||
days-before-close: -1 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -19,6 +19,7 @@ deps.pdf | |
.DS_Store | ||
html | ||
index.md | ||
index.html | ||
*.coq.d | ||
*.vok | ||
*.vos | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,3 +1,6 @@ | ||
[submodule "coqdocjs"] | ||
path = coqdocjs | ||
url = https://github.com/coq-community/coqdocjs.git | ||
[submodule "templates"] | ||
path = templates | ||
url = https://github.com/coq-community/templates.git |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,29 +1,29 @@ | ||
# This file was generated from `meta.yml`, please do not edit manually. | ||
# Follow the instructions on https://github.com/coq-community/templates to regenerate. | ||
|
||
opam-version: "2.0" | ||
maintainer: "[email protected]" | ||
version: "dev" | ||
|
||
homepage: "https://github.com/coq-community/coq-ext-lib" | ||
dev-repo: "git+https://github.com/coq-community/coq-ext-lib.git" | ||
bug-reports: "https://github.com/coq-community/coq-ext-lib/issues" | ||
authors: ["Gregory Malecha"] | ||
license: "BSD" | ||
build: [ | ||
[make "-j%{jobs}%" "theories"] | ||
] | ||
run-test: [ | ||
[make "-j%{jobs}%" "examples"] | ||
] | ||
install: [ | ||
[make "install"] | ||
] | ||
depends: [ | ||
"ocaml" | ||
"coq" {>= "8.8"} | ||
] | ||
license: "BSD-2-Clause" | ||
|
||
synopsis: "A library of Coq definitions, theorems, and tactics" | ||
description: """ | ||
A collection of theories and plugins that may be useful in other Coq developments.""" | ||
|
||
build: [make "-j%{jobs}%" "theories"] | ||
run-test: [make "-j%{jobs}%" "examples"] | ||
install: [make "install"] | ||
depends: [ | ||
"coq" { >= "8.9" < "8.10" | >= "8.11" } | ||
] | ||
|
||
tags: [ | ||
"logpath:ExtLib" | ||
] | ||
url { | ||
src: "git+https://github.com/coq-community/coq-ext-lib" | ||
} | ||
authors: [ | ||
"Gregory Malecha" | ||
] |
Submodule coqdocjs
updated
6 files
+7 −7 | Makefile.doc | |
+3 −3 | README.md | |
+10 −3 | example/Makefile | |
+1 −0 | example/Makefile.coq.local | |
+1 −1 | example/README.md | |
+1 −1 | extra/resources/coqdocjs.js |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,30 +1,30 @@ | ||
Require Import Coq.Bool.Bool. | ||
Require NPeano. | ||
Import NPeano.Nat. | ||
Require Import Arith.PeanoNat. | ||
Require Import ExtLib.Tactics.Consider. | ||
Require Import ExtLib.Data.Nat. | ||
|
||
Require Import Coq.ZArith.ZArith. | ||
Require Import Coq.micromega.Lia. | ||
|
||
Set Implicit Arguments. | ||
Set Strict Implicit. | ||
|
||
(** Some tests *) | ||
Section test. | ||
Goal forall x y z, (ltb x y && ltb y z) = true -> | ||
ltb x z = true. | ||
Goal forall x y z, (Nat.ltb x y && Nat.ltb y z) = true -> | ||
Nat.ltb x z = true. | ||
intros x y z. | ||
consider (ltb x y && ltb y z). | ||
consider (ltb x z); auto. intros. exfalso. omega. | ||
consider (Nat.ltb x y && Nat.ltb y z). | ||
consider (Nat.ltb x z); auto. intros. exfalso. lia. | ||
Qed. | ||
|
||
Goal forall x y z, | ||
ltb x y = true -> | ||
ltb y z = true -> | ||
ltb x z = true. | ||
Nat.ltb x y = true -> | ||
Nat.ltb y z = true -> | ||
Nat.ltb x z = true. | ||
Proof. | ||
intros. consider (ltb x y); consider (ltb y z); consider (ltb x z); intros; auto. | ||
exfalso; omega. | ||
intros. consider (Nat.ltb x y); consider (Nat.ltb y z); consider (Nat.ltb x z); intros; auto. | ||
exfalso; lia. | ||
Qed. | ||
|
||
End test. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,15 @@ | ||
From ExtLib Require Import | ||
Monad | ||
OptionMonad | ||
StateMonad. | ||
|
||
(** [Monad_stateT] is not in context, so this definition fails *) | ||
Fail Definition foo : stateT unit option unit := | ||
ret tt. | ||
|
||
(** Use [Existing Instance] to bring the Local [Monad_stateT] instance into context *) | ||
#[global] Existing Instance Monad_stateT. | ||
|
||
(** Now the definition succeeds *) | ||
Definition foo : stateT unit option unit := | ||
ret tt. |
Oops, something went wrong.