Commits (799)
# Enable syntax highlighting.
*.v gitlab-language=coq
# Convert to native line endings on checkout.
*.ref text
# Shell scripts need Linux line endings.
*.sh eol=lf
*.vo
*.vos
*.vok
*.vio
*.v.d
.coqdeps.d
.Makefile.coq.d
*.glob
*.cache
*.aux
......@@ -14,5 +17,5 @@ Makefile.coq
Makefile.coq.conf
*.crashcoqide
html/
build-dep/
builddep/
_opam
......@@ -6,8 +6,25 @@ stages:
variables:
CPU_CORES: "10"
.only_branches: &only_branches
only:
- /^master/@iris/stdpp
- /^ci/@iris/stdpp
.only_mr: &only_mr
only:
- merge_requests
.branches_and_mr: &branches_and_mr
only:
- /^master/@iris/stdpp
- /^ci/@iris/stdpp
- merge_requests
.template: &template
<<: *only_branches
stage: build
interruptible: true
tags:
- fp
script:
......@@ -16,63 +33,55 @@ variables:
cache:
key: "$CI_JOB_NAME"
paths:
- opamroot/
only:
- master
- /^ci/
- _opam/
except:
- triggers
- schedules
- api
## Build jobs
build-coq.dev:
<<: *template
variables:
OCAML: "ocaml-base-compiler.4.07.0"
OPAM_PINS: "coq version dev"
MANGLE_NAMES: "1"
CI_COQCHK: "1"
build-coq.8.9.0:
build-coq.8.13.2:
<<: *template
interruptible: false
variables:
OPAM_PINS: "coq version 8.9.0"
OPAM_PKG: "coq-stdpp"
OPAM_PINS: "coq version 8.13.2"
MANGLE_NAMES: "1"
DENY_WARNINGS: "1"
OPAM_PKG: "1"
DOC_DIR: "coqdoc@center.mpi-sws.org:stdpp"
TIMING_CONF: "coq-8.9.0"
tags:
- fp-timing
build-coq.8.8.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.2"
build-coq.8.8.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.1"
build-coq.8.8.0:
# Separate MR job that does not run on fp-timing.
build-coq.8.13.2-mr:
<<: *template
<<: *only_mr
variables:
OPAM_PINS: "coq version 8.8.0"
TIMING_CONF: "coq-8.8.0"
tags:
- fp-timing
OPAM_PINS: "coq version 8.13.2"
MANGLE_NAMES: "1"
DENY_WARNINGS: "1"
build-coq.8.7.2:
build-coq.8.12.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.2"
OPAM_PINS: "coq version 8.12.2"
DENY_WARNINGS: "1"
build-coq.8.7.1:
build-coq.8.11.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.1"
OPAM_PINS: "coq version 8.11.2"
build-coq.8.7.0:
build-coq.8.10.2:
<<: *template
<<: *branches_and_mr
variables:
OPAM_PINS: "coq version 8.7.0"
OPAM_PINS: "coq version 8.10.2"
[submodule "ci"]
path = ci
url = https://gitlab.mpi-sws.org/FP/iris-ci.git
This diff is collapsed.
All files in this development are distributed under the terms of the BSD
license, included below.
All files in this development are distributed under the terms of the 3-clause
BSD license (https://opensource.org/licenses/BSD-3-Clause), included below.
------------------------------------------------------------------------------
Copyright: std++ developers and contributors
BSD LICENCE
------------------------------------------------------------------------------
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:
......@@ -12,18 +12,17 @@ modification, are permitted provided that the following conditions are met:
* Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.
* Neither the name of the <organization> nor the
names of its contributors may be used to endorse or promote products
derived from this software without specific prior written permission.
* Neither the name of the copyright holder nor the names of its contributors
may be used to endorse or promote products derived from this software
without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT HOLDER> BE LIABLE FOR ANY
DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
+@make -f Makefile.coq $@
# Default target
all: Makefile.coq
+@make -f Makefile.coq all
+@$(MAKE) -f Makefile.coq all
.PHONY: all
# Permit local customization
-include Makefile.local
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
@#echo "Forwarding $@"
+@$(MAKE) -f Makefile.coq $@
phony: ;
.PHONY: phony
clean: Makefile.coq
+@make -f Makefile.coq clean
find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
rm -f Makefile.coq
+@$(MAKE) -f Makefile.coq clean
@# Make sure not to enter the `_opam` folder.
find [a-z]*/ \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
rm -f Makefile.coq .lia.cache builddep/*
.PHONY: clean
# Create Coq Makefile.
Makefile.coq: _CoqProject Makefile
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
# Install build-dependencies
build-dep/opam: opam Makefile
@echo "# Creating build-dep package."
@mkdir -p build-dep
@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam
@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
build-dep: build-dep/opam phony
@# We want opam to not just instal the build-deps now, but to also keep satisfying these
OPAMFILES=$(wildcard *.opam)
BUILDDEPFILES=$(addsuffix -builddep.opam, $(addprefix builddep/,$(basename $(OPAMFILES))))
builddep/%-builddep.opam: %.opam Makefile
@echo "# Creating builddep package for $<."
@mkdir -p builddep
@sed <$< -E 's/^(build|install|remove):.*/\1: []/; s/"(.*)"(.*= *version.*)$$/"\1-builddep"\2/;' >$@
builddep-opamfiles: $(BUILDDEPFILES)
.PHONY: builddep-opamfiles
builddep: builddep-opamfiles
@# We want opam to not just install the build-deps now, but to also keep satisfying these
@# constraints. Otherwise, `opam upgrade` may well update some packages to versions
@# that are incompatible with our build requirements.
@# To achieve this, we create a fake opam package that has our build-dependencies as
@# dependencies, but does not actually install anything itself.
@echo "# Pinning build-dep package." && \
if opam --version | grep "^1\." -q; then \
BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"; \
else \
opam install $(OPAMFLAGS) build-dep/; \
fi
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
_CoqProject: ;
opam: ;
# Phony wildcard targets
phony: ;
.PHONY: phony
@echo "# Installing builddep packages."
@opam install $(OPAMFLAGS) $(BUILDDEPFILES)
.PHONY: builddep
# Backwards compatibility target
build-dep: builddep
.PHONY: build-dep
# Some files that do *not* need to be forwarded to Makefile.coq.
# ("::" lets Makefile.local overwrite this.)
Makefile Makefile.local _CoqProject $(OPAMFILES):: ;
# use NO_TEST=1 to skip the tests
NO_TEST:=
# use MAKE_REF=1 to generate new reference files
MAKE_REF:=
# Run tests interleaved with main build. They have to be in the same target for this.
real-all: $(if $(NO_TEST),,test)
real-all: style $(if $(NO_TEST),,test)
style: $(VFILES) coq-lint.sh
# Make sure everything imports the options, and some general linting.
$(SHOW)"COQLINT"
$(HIDE)for FILE in $(VFILES); do \
if ! fgrep -q 'From stdpp Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; echo; exit 1; fi ; \
./coq-lint.sh "$$FILE" || exit 1; \
done
.PHONY: style
# the test suite
TESTFILES=$(wildcard tests/*.v)
TESTFILES:=$(shell find tests -name "*.v")
NORMALIZER:=test-normalizer.sed
test: $(TESTFILES:.v=.vo)
.PHONY: test
COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
COQ_OLD=$(shell echo "$(COQ_VERSION)" | egrep "^8\.7\b" -q && echo 1)
# Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later.
COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+\b' -o)
tests/.coqdeps.d: $(TESTFILES)
......@@ -16,18 +32,24 @@ tests/.coqdeps.d: $(TESTFILES)
$(HIDE)$(COQDEP) -dyndep var $(COQMF_COQLIBS_NOML) $^ $(redir_if_ok)
-include tests/.coqdeps.d
$(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref)
$(HIDE)TEST="$$(basename -s .v $<)" && \
if test -f "tests/$$TEST.$(COQ_MINOR_VERSION).ref"; then \
REF="tests/$$TEST.$(COQ_MINOR_VERSION).ref"; \
# Main test script (comments out-of-line because macOS otherwise barfs?!?)
# - Determine reference file (`REF`).
# - Print user-visible status line.
# - Dump Coq output into a temporary file.
# - Run `sed -i` on that file in a way that works on macOS.
# - Either compare the result with the reference file, or move it over the reference file.
# - Cleanup, and mark as done for make.
$(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref) $(NORMALIZER)
$(HIDE)if test -f $*".$(COQ_MINOR_VERSION).ref"; then \
REF=$*".$(COQ_MINOR_VERSION).ref"; \
else \
REF="tests/$$TEST.ref"; \
REF=$*".ref"; \
fi && \
echo "COQTEST$(if $(COQ_OLD), [no ref],$(if $(MAKE_REF), [make ref],)) $<$(if $(COQ_OLD),, (ref: $$REF))" && \
echo "COQTEST$(if $(MAKE_REF), [make ref],) $< (ref: $$REF)" && \
TMPFILE="$$(mktemp)" && \
$(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \
$(if $(COQ_OLD),true, \
$(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff -u "$$REF" "$$TMPFILE") \
) && \
sed -f $(NORMALIZER) "$$TMPFILE" > "$$TMPFILE".new && \
mv "$$TMPFILE".new "$$TMPFILE" && \
$(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff -u "$$REF" "$$TMPFILE") && \
rm -f "$$TMPFILE" && \
touch $@
......@@ -45,11 +45,11 @@ Notably:
This version is known to compile with:
- Coq version 8.7.0 / 8.7.1 / 8.7.2 / 8.8.0 / 8.8.1 / 8.8.2 / 8.9.0
- Coq version 8.10.2 / 8.11.2 / 8.12.2 / 8.13.2
## Installing via opam
To obtain the latest stable release via opam (1.2.2 or newer), you have to add
To obtain the latest stable release via opam (2.0.0 or newer), you have to add
the Coq opam repository:
opam repo add coq-released https://coq.inria.fr/opam/released
......@@ -79,3 +79,9 @@ your account. Then you can fork the
[Coq-std++ git repository](https://gitlab.mpi-sws.org/iris/stdpp), make your
changes in your fork, and create a merge request.
## Common problems
On Windows, differences in line endings may cause tests to fail. This can be
fixed by setting Git's autocrlf option to true:
git config --global core.autocrlf true
-Q theories stdpp
# "Declare Scope" does not exist yet in 8.9
-arg -w -arg -undeclared-scope
theories/options.v
theories/base.v
theories/tactics.v
theories/option.v
......@@ -33,10 +33,12 @@ theories/numbers.v
theories/nmap.v
theories/zmap.v
theories/coPset.v
theories/coGset.v
theories/lexico.v
theories/propset.v
theories/decidable.v
theories/list.v
theories/list_numbers.v
theories/functions.v
theories/hlist.v
theories/sorting.v
......@@ -44,3 +46,4 @@ theories/infinite.v
theories/nat_cancel.v
theories/namespaces.v
theories/telescopes.v
theories/binders.v
#!/bin/bash
set -e
## A simple shell script checking for some common Coq issues.
FILE="$1"
if egrep -n '^\s*((Existing\s+|Program\s+)Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold)|(Open|Close)\s+Scope|Opaque|Transparent)\b' "$FILE"; then
echo "ERROR: $FILE contains 'Instance'/'Arguments'/'Hint' or another side-effect without locality (see above)."
echo "Please add 'Global' or 'Local' as appropriate."
echo
exit 1
fi
This project contains an extended "Standard Library" for Coq called coq-std++.
opam-version: "2.0"
maintainer: "Ralf Jung <jung@mpi-sws.org>"
authors: "The std++ team"
license: "BSD-3-Clause"
homepage: "https://gitlab.mpi-sws.org/iris/stdpp"
bug-reports: "https://gitlab.mpi-sws.org/iris/stdpp/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/iris/stdpp.git"
version: "dev"
synopsis: "An extended \"Standard Library\" for Coq"
description: """
The key features of this library are as follows:
- It provides a great number of definitions and lemmas for common data
......@@ -17,3 +27,11 @@ The key features of this library are as follows:
for proving compatibility of functions with respect to relations, and a solver
`set_solver` for goals involving set operations.
- It is entirely dependency- and axiom-free.
"""
depends: [
"coq" { (>= "8.10.2" & < "8.14~") | (= "dev") }
]
build: [make "-j%{jobs}%"]
install: [make "install"]
opam-version: "1.2"
name: "coq-stdpp"
maintainer: "Ralf Jung <jung@mpi-sws.org>"
homepage: "https://gitlab.mpi-sws.org/iris/stdpp"
authors: "Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung"
bug-reports: "https://gitlab.mpi-sws.org/iris/stdpp/issues"
license: "BSD"
dev-repo: "https://gitlab.mpi-sws.org/iris/stdpp.git"
build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/stdpp"]
depends: [
"coq" { (>= "8.7" & < "8.10~") | (= "dev") }
]
# adjust for https://github.com/coq/coq/pull/13656
s/subgoal/goal/g
"eunify_test"
: string
The command has indeed failed with message:
No matching clauses for match.
((fix add (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S p => S (add p m)
end) x y)
"eunify_test_evars"
: string
The command has indeed failed with message:
No matching clauses for match.
From stdpp Require Import tactics strings.
Unset Mangle Names.
Check "eunify_test".
Lemma eunify_test : x y, 0 < S x + y.
Proof.
intros x y.
(* Test that Ltac matching fails, otherwise this test is pointless *)
Fail
match goal with
| |- 0 < S _ => idtac
end.
(* [eunify] succeeds *)
match goal with
| |- 0 < ?x => eunify x (S _)
end.
match goal with
| |- 0 < ?x => let y := open_constr:(_) in eunify x (S y); idtac y
end.
lia.
Qed.
Check "eunify_test_evars".
Lemma eunify_test_evars : x y, 0 < S x + y.
Proof.
eexists _, _.
(* Test that Ltac matching fails, otherwise this test is pointless *)
Fail
match goal with
| |- 0 < S _ => idtac
end.
(* [eunify] succeeds even if the goal contains evars *)
match goal with
| |- 0 < ?x => eunify x (S _)
end.
(* Let's try to use [eunify] to instantiate the first evar *)
match goal with
| |- 0 < ?x => eunify x (1 + _)
end.
(* And the other evar *)
match goal with
| |- 0 < ?x => eunify x 2
end.
lia.
Qed.
\ No newline at end of file
From stdpp Require Import fin_maps.
From stdpp Require Import fin_maps fin_map_dom.
Section map_disjoint.
Context `{FinMap K M}.
......@@ -11,3 +11,14 @@ Section map_disjoint.
m2 !! i = None m1 ## {[ i := x ]} m2 m2 ## <[i:=x]> m1 m1 !! i = None.
Proof. intros. solve_map_disjoint. Qed.
End map_disjoint.
Section map_dom.
Context `{FinMapDom K M D}.
Lemma set_solver_dom_subseteq {A} (i j : K) (x y : A) :
{[i; j]} dom D (<[i:=x]> (<[j:=y]> ( : M A))).
Proof. set_solver. Qed.
Lemma set_solver_dom_disjoint {A} (X : D) : dom D ( : M A) ## X.
Proof. set_solver. Qed.
End map_dom.
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
length
: list ?A → nat
where
?A : [ |- Type]
From stdpp Require prelude strings list.
(** Check that we always get the [length] function on lists, not on strings. *)
Module test1.
Import stdpp.base.
Check length.
Import stdpp.strings.
Check length.
Import stdpp.base.
Check length.
End test1.
Module test2.
Import stdpp.prelude.
Check length.
Import stdpp.strings.
Check length.
Import stdpp.prelude.
Check length.
End test2.
Module test3.
Import stdpp.strings.
Check length.
Import stdpp.prelude.
Check length.
End test3.
Module test4.
Import stdpp.list.
Check length.
Import stdpp.strings.
Check length.
Import stdpp.list.
Check length.
End test4.
1 goal
============================
None = None
1 goal
============================
Some 10 = Some 10
1 goal
============================
Some 11 = Some 11
1 goal
l : list nat
============================
last (11 :: l) = last (11 :: l)
1 goal
l : list nat
============================
last (10 :: l) = last (10 :: l)