Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • iris/stdpp
  • johannes/stdpp
  • proux1/stdpp
  • dosualdo/stdpp
  • benoit/coq-stdpp
  • dfrumin/coq-stdpp
  • haidang/stdpp
  • amintimany/coq-stdpp
  • swasey/coq-stdpp
  • simongregersen/stdpp
  • proux/stdpp
  • janno/coq-stdpp
  • amaurremi/coq-stdpp
  • msammler/stdpp
  • tchajed/stdpp
  • YaZko/stdpp
  • maximedenes/stdpp
  • jakobbotsch/stdpp
  • Blaisorblade/stdpp
  • simonspies/stdpp
  • lepigre/stdpp
  • devilhena/stdpp
  • simonfv/stdpp
  • jihgfee/stdpp
  • snyke7/stdpp
  • Armael/stdpp
  • gmalecha/stdpp
  • olaure01/stdpp
  • sarahzrf/stdpp
  • atrieu/stdpp
  • herbelin/stdpp
  • arthuraa/stdpp
  • lgaeher/stdpp
  • mrhaandi/stdpp
  • mattam82/stdpp
  • Quarkbeast/stdpp
  • aa755/stdpp
  • gmevel/stdpp
  • lstefane/stdpp
  • jung/stdpp
  • vsiles/stdpp
  • dlesbre/stdpp
  • bergwerf/stdpp
  • marijnvanwezel/stdpp
  • ivanbakel/stdpp
  • tperami/stdpp
  • adamAndMath/stdpp
  • Villetaneuse/stdpp
  • sanjit/stdpp
  • yiyunliu/stdpp
  • thomas-lamiaux/stdpp
  • Tragicus/stdpp
  • kbedarka/stdpp
53 results
Show changes
Commits on Source (2385)
# 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
\#*\#
.\#*
*~
*.bak
.coq-native/
Makefile.coq
Makefile.coq.conf
_CoqProject.*
Makefile.package.*
.Makefile.package.*
*.crashcoqide
html/
builddep/
_opam
_build/
*.install
image: ralfjung/opam-ci:opam2
stages:
- build
variables:
CPU_CORES: "10"
OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
# Avoid needlessly increasing our TCB with native_compute
COQEXTRAFLAGS: "-native-compiler no"
.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:
- git clone https://gitlab.mpi-sws.org/iris/ci.git ci -b opam2
- ci/buildjob
cache:
key: "$CI_JOB_NAME"
paths:
- _opam/
except:
- triggers
- schedules
- api
## Build jobs
# The newest version runs with timing.
build-coq.8.20.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.20.1"
DENY_WARNINGS: "1"
MANGLE_NAMES: "1"
CI_COQCHK: "1"
OPAM_PKG: "1"
DOC_DIR: "coqdoc@center.mpi-sws.org:stdpp"
tags:
- fp-timing
interruptible: false
# The newest version also runs in MRs, without timing.
build-coq.8.20.1-mr:
<<: *template
<<: *only_mr
variables:
OPAM_PINS: "coq version 8.20.1"
DENY_WARNINGS: "1"
MANGLE_NAMES: "1"
# Also ensure Dune works.
build-coq.8.20.1-dune:
<<: *template
variables:
OPAM_PINS: "coq version 8.20.1 dune version 3.15.2"
MAKE_TARGET: "dune"
build-coq.8.19.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.19.1"
DENY_WARNINGS: "1"
# The oldest version runs in MRs, without name mangling.
build-coq.8.18.0:
<<: *template
<<: *branches_and_mr
variables:
OPAM_PINS: "coq version 8.18.0"
DENY_WARNINGS: "1"
This diff is collapsed.
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
------------------------------------------------------------------------------
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:
* Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.
* 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 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 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
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
# Default target
all: Makefile.coq
+@$(MAKE) -f Makefile.coq all
.PHONY: all
# Build with dune.
# This exists only for CI; you should just call `dune build` directly instead.
dune:
@dune build --display=short
.PHONY: dune
# 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
@# 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 $(EXTRA_COQFILES)
# Install build-dependencies
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 "# 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:=
# Only test reference output on known versions of Coq, to avoid blocking
# Coq CI when they change the printing a little.
# Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later.
COQ_REF=$(shell echo "$(COQ_VERSION)" | grep -E "^8\.(20)\." -q && echo 1)
# Run tests interleaved with main build. They have to be in the same target for this.
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 ! grep -F -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:=$(shell find tests -name "*.v")
NORMALIZER:=test-normalizer.sed
test: $(TESTFILES:.v=.vo)
.PHONY: test
COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
tests/.coqdeps.d: $(TESTFILES)
$(SHOW)'COQDEP TESTFILES'
$(HIDE)$(COQDEP) -dyndep var $(COQMF_COQLIBS_NOML) $^ $(redir_if_ok)
-include tests/.coqdeps.d
# Main test script (comments out-of-line because macOS otherwise barfs?!?)
# - Determine reference file (`REF`).
# - Print user-visible status line.
# - unset env vars that change Coq's output
# - 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)REF=$*".ref" && \
echo "COQTEST$(if $(COQ_REF),$(if $(MAKE_REF), [make ref],), [ref ignored]) $< (ref: $$REF)" && \
TMPFILE="$$(mktemp)" && \
unset OCAMLRUNPARAM && \
$(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \
sed -E -f $(NORMALIZER) "$$TMPFILE" > "$$TMPFILE".new && \
mv "$$TMPFILE".new "$$TMPFILE" && \
$(if $(COQ_REF),\
$(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff --strip-trailing-cr -u "$$REF" "$$TMPFILE"), \
true \
) && \
rm -f "$$TMPFILE" && \
touch $@
# Coq-std++ [[coqdoc]](https://plv.mpi-sws.org/coqdoc/stdpp/)
This project contains an extended "Standard Library" for Coq called coq-std++.
The key features of this library are as follows:
- It provides a great number of definitions and lemmas for common data
structures such as lists, finite maps, finite sets, and finite multisets.
- It uses type classes for common notations (like `∅`, `∪`, and Haskell-style
monad notations) so that these can be overloaded for different data structures.
- It uses type classes to keep track of common properties of types, like it
having decidable equality or being countable or finite.
- Most data structures are represented in canonical ways so that Leibniz
equality can be used as much as possible (for example, for maps we have
`m1 = m2` iff `∀ i, m1 !! i = m2 !! i`). On top of that, the library provides
setoid instances for most types and operations.
- It provides various tactics for common tasks, like an ssreflect inspired
`done` tactic for finishing trivial goals, a simple breadth-first solver
`naive_solver`, an equality simplifier `simplify_eq`, a solver `solve_proper`
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.
## Side-effects
Importing std++ has some side effects as the library sets some global options.
Notably:
* `Generalizable All Variables`: This option enables implicit generalization in
arguments of the form `` `{...}`` (i.e., anonymous arguments) and in terms of
shape `` `{}``/`` `[]``/`` `()``. See [Coq's
manual](https://coq.inria.fr/distrib/current/refman/language/extensions/implicit-arguments.html#implicit-generalization)
for further details.
* The behavior of `Program` is tweaked: `Unset Transparent Obligations`,
`Obligation Tactic := idtac`, `Add Search Blacklist "_obligation_"`. See
[`base.v`](theories/base.v) for further details.
* It blocks `simpl` on all operations involving `Z`, `N`, and `positive` (by
setting `Arguments op : simpl never`). We do this because `simpl` tends to
expose the internals of said operations (e.g. try `simpl` on `Z.of_nat (S n) + y`).
* It sets `intuition_solver` to `auto`. The default is `auto with *`, which is
very expensive.
## Prerequisites
This version is known to compile with:
- Coq version 8.18.0 / 8.19.1 / 8.20.1
Generally we always aim to support the last two stable Coq releases. Support for
older versions will be dropped when it is convenient.
## Installing via opam
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
Then you can do `opam install coq-stdpp`.
To obtain a development version, add the Iris opam repository:
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
## Building from source
Run `make -jN` in this directory to build the library, where `N` is the number
of your CPU cores. Then run `make install` to install the library.
## Unstable libraries
The `stdpp_unstable` folder contains a set of libraries that are not
deemed stable enough to be included in the main std++ library. These
libraries are available via the `coq-stdpp-unstable` opam package. For
each library, there is a corresponding "tracking issue" in the std++
issue tracker (also linked from the library itself) which tracks the
work that still needs to be done before moving the library to std++.
No stability guarantees whatsoever are made for this package.
Note that the unstable package is not released, so it only exists in the
development version of std++.
## Contributing to std++
If you want to report a bug, please use the
[issue tracker](https://gitlab.mpi-sws.org/iris/stdpp/issues). You will have to
create an account at the
[MPI-SWS GitLab](https://gitlab.mpi-sws.org/users/sign_in) (use the "Register"
tab).
To contribute code, please send your MPI-SWS GitLab username to
[Ralf Jung](https://gitlab.mpi-sws.org/jung) to enable personal projects for
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.
Please refer to [our style guide](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/style_guide.md)
for code formatting and naming policies.
## 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
# Search paths for all packages. They must all match the regex
# `-Q $PACKAGE[/ ]` so that we can filter out the right ones for each package.
-Q stdpp stdpp
-Q stdpp_bitvector stdpp.bitvector
-Q stdpp_unstable stdpp.unstable
# Custom flags (to be kept in sync with the dune file at the root of the repo).
# Fixing this one requires Coq 8.19
-arg -w -arg -argument-scope-delimiter
# Warning seems incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
-arg -w -arg -notation-incompatible-prefix
# We can't do this migration yet until we require Coq 9.0
-arg -w -arg -deprecated-from-Coq
-arg -w -arg -deprecated-dirpath-Coq
stdpp/options.v
stdpp/base.v
stdpp/tactics.v
stdpp/option.v
stdpp/fin_map_dom.v
stdpp/boolset.v
stdpp/fin_maps.v
stdpp/fin.v
stdpp/vector.v
stdpp/pmap.v
stdpp/stringmap.v
stdpp/fin_sets.v
stdpp/mapset.v
stdpp/proof_irrel.v
stdpp/hashset.v
stdpp/pretty.v
stdpp/countable.v
stdpp/orders.v
stdpp/natmap.v
stdpp/strings.v
stdpp/well_founded.v
stdpp/relations.v
stdpp/sets.v
stdpp/listset.v
stdpp/streams.v
stdpp/gmap.v
stdpp/gmultiset.v
stdpp/prelude.v
stdpp/listset_nodup.v
stdpp/finite.v
stdpp/numbers.v
stdpp/nmap.v
stdpp/zmap.v
stdpp/coPset.v
stdpp/coGset.v
stdpp/lexico.v
stdpp/propset.v
stdpp/decidable.v
stdpp/list.v
stdpp/list_numbers.v
stdpp/functions.v
stdpp/hlist.v
stdpp/sorting.v
stdpp/infinite.v
stdpp/nat_cancel.v
stdpp/namespaces.v
stdpp/telescopes.v
stdpp/binders.v
stdpp/ssreflect.v
stdpp_bitvector/definitions.v
stdpp_bitvector/tactics.v
stdpp_bitvector/bitvector.v
stdpp_unstable/bitblast.v
#!/bin/bash
set -e
## A simple shell script checking for some common Coq issues.
FILE="$1"
if grep -E -n '^\s*((Existing\s+|Program\s+|Declare\s+)?Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold|Rewrite)|(Open|Close)\s+Scope|Opaque|Transparent|Typeclasses (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
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: "A library for bitvectors based on std++"
description: """
This library provides the `bv n` type for representing n-bit bitvectors (i.e.,
fixed-size integers with n bits). It comes with definitions for the standard operations
(e.g., the operations exposed by SMT-LIB) and some basic automation for solving bitvector
goals based on the lia tactic.
"""
tags: [
"logpath:stdpp.bitvector"
]
depends: [
"coq-stdpp" {= version}
]
build: ["./make-package" "stdpp_bitvector" "-j%{jobs}%"]
install: ["./make-package" "stdpp_bitvector" "install"]
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: "Unfinished std++ libraries"
description: """
This package contains libraries that have been proposed for inclusion in std++, but more
work is needed before they are ready for this.
"""
tags: [
"logpath:stdpp.unstable"
]
depends: [
"coq-stdpp" {= version}
"coq-stdpp-bitvector" {= version}
]
build: ["./make-package" "stdpp_unstable" "-j%{jobs}%"]
install: ["./make-package" "stdpp_unstable" "install"]
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
structures such as lists, finite maps, finite sets, and finite multisets.
- It uses type classes for common notations (like `∅`, `∪`, and Haskell-style
monad notations) so that these can be overloaded for different data structures.
- It uses type classes to keep track of common properties of types, like it
having decidable equality or being countable or finite.
- Most data structures are represented in canonical ways so that Leibniz
equality can be used as much as possible (for example, for maps we have
`m1 = m2` iff `∀ i, m1 !! i = m2 !! i`). On top of that, the library provides
setoid instances for most types and operations.
- It provides various tactics for common tasks, like an ssreflect inspired
`done` tactic for finishing trivial goals, a simple breadth-first solver
`naive_solver`, an equality simplifier `simplify_eq`, a solver `solve_proper`
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.
"""
tags: [
"logpath:stdpp"
]
depends: [
"coq" { (>= "8.18" & < "9.1~") | (= "dev") }
]
build: ["./make-package" "stdpp" "-j%{jobs}%"]
install: ["./make-package" "stdpp" "install"]
Support for the dune build system
=================================
**NOTE:** in case of problem with the dune build, you can ask @lepigre or
@Blaisorblade for help.
The library can be built using dune by running `dune build`. Note that `dune`
needs to be installed separately with `opam install dune`, as it is currently
not part of the dependencies of the project.
Useful links:
- [dune documentation](https://dune.readthedocs.io)
- [coq zulip channel](https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs-.26-users)
Editor support
--------------
Good dune support in editors is lacking at the moment, but there are tricks you
can play to make it work.
One option is to configure your editor to invoke the `dune coq top` command
instead of `coqtop`, but that is not easy to configure.
Another option is to change the `_CoqProject` file to something like:
```
-Q stdpp stdpp
-Q _build/default/stdpp stdpp
-Q stdpp_bitvector stdpp.bitvector
-Q _build/default/stdpp_bitvector stdpp.bitvector
-Q stdpp_unstable stdpp.unstable
-Q _build/default/stdpp_unstable stdpp.unstable
```
Note that this includes two bindings for each logical path: a binding to a
folder in the source tree (where editors will find the `.v` files), and a
binding to the same folder under `_build/default` (where editors will find
the corresponding `.vo` files). The binding for a source folder must come
before the binding for the corresponding build folder, so that editors know
to jump to source files in the source tree (and not their read-only copy in
the build folder).
If you do this, you still need to invoke `dune` manually to make sure that the
dependencies of the file you are stepping through are up-to-date. To build a
single file, you can do, e.g., `dune build stdpp/options.vo`. To build only
the `stdpp` folder, you can do `dune build stdpp`.
(env
(_ ; Applies to all profiles (dev, release, ...).
(coq
(flags ; Configure the coqc flags.
(:standard ; Keeping the default flags.
; Add custom flags (to be kept in sync with _CoqProject).
-w -argument-scope-delimiter
-w -notation-incompatible-prefix)))))
(lang dune 3.8)
(using coq 0.8)
#!/bin/sh
set -e
# Helper script to build and/or install just one package out of this repository.
# Assumes that all the other packages it depends on have been installed already!
# Make sure we get a GNU version of make.
# This is exactly how opam determines which make executable to use.
OS=$(uname)
MAKE="make"
if [ $OS == "FreeBSD" ] || [ $OS == "OpenBSD" ] ||\
[ $OS == "NetBSD" ] || [ $OS == "DragonFly" ]; then
MAKE="gmake"
fi
PROJECT="$1"
shift
COQFILE="_CoqProject.$PROJECT"
MAKEFILE="Makefile.package.$PROJECT"
if ! grep -E -q "^$PROJECT/" _CoqProject; then
echo "No files in $PROJECT/ found in _CoqProject; this does not seem to be a valid project name."
exit 1
fi
# Generate _CoqProject file and Makefile
rm -f "$COQFILE"
# Get the right "-Q" line.
grep -E "^-Q $PROJECT[ /]" _CoqProject >> "$COQFILE"
# Get everything until the first empty line except for the "-Q" lines.
sed -n '/./!q;p' _CoqProject | grep -E -v "^-Q " >> "$COQFILE"
# Get the files.
grep -E "^$PROJECT/" _CoqProject >> "$COQFILE"
# Now we can run coq_makefile.
"${COQBIN}coq_makefile" -f "$COQFILE" -o "$MAKEFILE"
# Run build
$MAKE -f "$MAKEFILE" "$@"
# Cleanup
rm -f ".$MAKEFILE.d" "$MAKEFILE"*
This diff is collapsed.
(** This file implements a type [binder] with elements [BAnon] for the
anonymous binder, and [BNamed] for named binders. This type is isomorphic to
[option string], but we use a special type so that we can define [BNamed] as
a coercion.
This library is used in various Iris developments, like heap-lang, LambdaRust,
Iron, Fairis. *)
From stdpp Require Export strings.
From stdpp Require Import sets countable finite fin_maps.
From stdpp Require Import options.
(* Pick up extra assumptions from section parameters. *)
Set Default Proof Using "Type*".
Declare Scope binder_scope.
Delimit Scope binder_scope with binder.
Inductive binder := BAnon | BNamed :> string binder.
Bind Scope binder_scope with binder.
Notation "<>" := BAnon : binder_scope.
(** [binder_list] matches [option_list]. *)
Definition binder_list (b : binder) : list string :=
match b with
| BAnon => []
| BNamed s => [s]
end.
Global Instance binder_dec_eq : EqDecision binder.
Proof. solve_decision. Defined.
Global Instance binder_inhabited : Inhabited binder := populate BAnon.
Global Instance binder_countable : Countable binder.
Proof.
refine (inj_countable'
(λ b, match b with BAnon => None | BNamed s => Some s end)
(λ b, match b with None => BAnon | Some s => BNamed s end) _); by intros [].
Qed.
(** The functions [cons_binder b ss] and [app_binder bs ss] are typically used
to collect the free variables of an expression. Here [ss] is the current list of
free variables, and [b], respectively [bs], are the binders that are being
added. *)
Definition cons_binder (b : binder) (ss : list string) : list string :=
match b with BAnon => ss | BNamed s => s :: ss end.
Infix ":b:" := cons_binder (at level 60, right associativity).
Fixpoint app_binder (bs : list binder) (ss : list string) : list string :=
match bs with [] => ss | b :: bs => b :b: app_binder bs ss end.
Infix "+b+" := app_binder (at level 60, right associativity).
Global Instance set_unfold_cons_binder s b ss P :
SetUnfoldElemOf s ss P SetUnfoldElemOf s (b :b: ss) (BNamed s = b P).
Proof.
constructor. rewrite <-(set_unfold (s ss) P).
destruct b; simpl; rewrite ?elem_of_cons; naive_solver.
Qed.
Global Instance set_unfold_app_binder s bs ss P Q :
SetUnfoldElemOf (BNamed s) bs P SetUnfoldElemOf s ss Q
SetUnfoldElemOf s (bs +b+ ss) (P Q).
Proof.
intros HinP HinQ.
constructor. rewrite <-(set_unfold (s ss) Q), <-(set_unfold (BNamed s bs) P).
clear HinP HinQ.
induction bs; set_solver.
Qed.
Lemma app_binder_named ss1 ss2 : (BNamed <$> ss1) +b+ ss2 = ss1 ++ ss2.
Proof. induction ss1; by f_equal/=. Qed.
Lemma app_binder_snoc bs s ss : bs +b+ (s :: ss) = (bs ++ [BNamed s]) +b+ ss.
Proof. induction bs; by f_equal/=. Qed.
Global Instance cons_binder_Permutation b : Proper (() ==> ()) (cons_binder b).
Proof. intros ss1 ss2 Hss. destruct b; csimpl; by rewrite Hss. Qed.
Global Instance app_binder_Permutation : Proper (() ==> () ==> ()) app_binder.
Proof.
assert ( bs, Proper (() ==> ()) (app_binder bs)).
{ intros bs. induction bs as [|[]]; intros ss1 ss2; simpl; by intros ->. }
induction 1 as [|[]|[] []|]; intros ss1 ss2 Hss; simpl;
first [by eauto using perm_trans|by rewrite 1?perm_swap, Hss].
Qed.
Definition binder_delete `{Delete string M} (b : binder) (m : M) : M :=
match b with BAnon => m | BNamed s => delete s m end.
Definition binder_insert `{Insert string A M} (b : binder) (x : A) (m : M) : M :=
match b with BAnon => m | BNamed s => <[s:=x]> m end.
Global Instance: Params (@binder_insert) 4 := {}.
Section binder_delete_insert.
Context `{FinMap string M}.
Global Instance binder_insert_proper `{Equiv A} b :
Proper (() ==> () ==> (≡@{M A})) (binder_insert b).
Proof. destruct b; solve_proper. Qed.
Lemma binder_delete_empty {A} b : binder_delete b =@{M A} ∅.
Proof. destruct b; simpl; eauto using delete_empty. Qed.
Lemma lookup_binder_delete_None {A} (m : M A) b s :
binder_delete b m !! s = None b = BNamed s m !! s = None.
Proof. destruct b; simpl; by rewrite ?lookup_delete_None; naive_solver. Qed.
Lemma binder_insert_fmap {A B} (f : A B) (x : A) b (m : M A) :
f <$> binder_insert b x m = binder_insert b (f x) (f <$> m).
Proof. destruct b; simpl; by rewrite ?fmap_insert. Qed.
Lemma binder_delete_insert {A} b s x (m : M A) :
b BNamed s binder_delete b (<[s:=x]> m) = <[s:=x]> (binder_delete b m).
Proof. intros. destruct b; simpl; by rewrite ?delete_insert_ne by congruence. Qed.
Lemma binder_delete_delete {A} b s (m : M A) :
binder_delete b (delete s m) = delete s (binder_delete b m).
Proof. destruct b; simpl; by rewrite 1?delete_commute. Qed.
End binder_delete_insert.
(** This file implements boolsets as functions into Prop. *)
From stdpp Require Export prelude.
From stdpp Require Import options.
Record boolset (A : Type) : Type := BoolSet { boolset_car : A bool }.
Global Arguments BoolSet {_} _ : assert.
Global Arguments boolset_car {_} _ _ : assert.
Global Instance boolset_top {A} : Top (boolset A) := BoolSet (λ _, true).
Global Instance boolset_empty {A} : Empty (boolset A) := BoolSet (λ _, false).
Global Instance boolset_singleton `{EqDecision A} : Singleton A (boolset A) := λ x,
BoolSet (λ y, bool_decide (y = x)).
Global Instance boolset_elem_of {A} : ElemOf A (boolset A) := λ x X, boolset_car X x.
Global Instance boolset_union {A} : Union (boolset A) := λ X1 X2,
BoolSet (λ x, boolset_car X1 x || boolset_car X2 x).
Global Instance boolset_intersection {A} : Intersection (boolset A) := λ X1 X2,
BoolSet (λ x, boolset_car X1 x && boolset_car X2 x).
Global Instance boolset_difference {A} : Difference (boolset A) := λ X1 X2,
BoolSet (λ x, boolset_car X1 x && negb (boolset_car X2 x)).
Global Instance boolset_cprod {A B} :
CProd (boolset A) (boolset B) (boolset (A * B)) := λ X1 X2,
BoolSet (λ x, boolset_car X1 x.1 && boolset_car X2 x.2).
Global Instance boolset_top_set `{EqDecision A} : TopSet A (boolset A).
Proof.
split; [split; [split| |]|].
- by intros x ?.
- by intros x y; rewrite <-(bool_decide_spec (x = y)).
- split; [apply orb_prop_elim | apply orb_prop_intro].
- split; [apply andb_prop_elim | apply andb_prop_intro].
- intros X Y x; unfold elem_of, boolset_elem_of; simpl.
destruct (boolset_car X x), (boolset_car Y x); simpl; tauto.
- done.
Qed.
Global Instance boolset_elem_of_dec {A} : RelDecision (∈@{boolset A}).
Proof. refine (λ x X, cast_if (decide (boolset_car X x))); done. Defined.
Lemma elem_of_boolset_cprod {A B} (X1 : boolset A) (X2 : boolset B) (x : A * B) :
x cprod X1 X2 x.1 X1 x.2 X2.
Proof. apply andb_True. Qed.
Global Instance set_unfold_boolset_cprod {A B} (X1 : boolset A) (X2 : boolset B) x P Q :
SetUnfoldElemOf x.1 X1 P SetUnfoldElemOf x.2 X2 Q
SetUnfoldElemOf x (cprod X1 X2) (P Q).
Proof.
intros ??; constructor.
by rewrite elem_of_boolset_cprod, (set_unfold_elem_of x.1 X1 P),
(set_unfold_elem_of x.2 X2 Q).
Qed.
Global Typeclasses Opaque boolset_elem_of.
Global Opaque boolset_empty boolset_singleton boolset_union
boolset_intersection boolset_difference boolset_cprod.