.gitattributes

+# 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

.gitignore

 *.vo
+*.vos
+*.vok
 *.vio
 *.v.d
+.coqdeps.d
+.Makefile.coq.d
 *.glob
 *.cache
 *.aux
@@ -10,4 +14,13 @@
 *.bak
 .coq-native/
 Makefile.coq
+Makefile.coq.conf
+_CoqProject.*
+Makefile.package.*
+.Makefile.package.*
 *.crashcoqide
+html/
+builddep/
+_opam
+_build/
+*.install

.gitlab-ci.yml

+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"

LICENSE

-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.
-

Makefile

-# Process flags
-ifeq ($(Y), 1)
-	YFLAG=-y
-endif
+# Default target
+all: Makefile.coq
+	+@$(MAKE) -f Makefile.coq all
+.PHONY: all
 
-# Determine Coq version
-COQ_VERSION=$(shell coqc --version | egrep -o 'version 8.[0-9]' | egrep -o '8.[0-9]')
-COQ_MAKEFILE_FLAGS ?=
+# Build with dune.
+# This exists only for CI; you should just call `dune build` directly instead.
+dune:
+	@dune build --display=short
+.PHONY: dune
 
-ifeq ($(COQ_VERSION), 8.6)
-	COQ_MAKEFILE_FLAGS += -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
-endif
+# Permit local customization
+-include Makefile.local
 
 # Forward most targets to Coq makefile (with some trick to make this phony)
 %: Makefile.coq phony
-	+@make -f Makefile.coq $@
-
-all: Makefile.coq
-	+@make -f Makefile.coq all
+	@#echo "Forwarding $@"
+	+@$(MAKE) -f Makefile.coq $@
+phony: ;
+.PHONY: phony
 
 clean: Makefile.coq
-	+@make -f Makefile.coq clean
-	find theories \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
-	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. POSIX awk can't do in-place editing, but coq_makefile wants the real filename, so we do some file gymnastics.
-Makefile.coq: _CoqProject Makefile awk.Makefile
-	coq_makefile $(COQ_MAKEFILE_FLAGS) -f _CoqProject -o Makefile.coq
-	mv Makefile.coq Makefile.coq.tmp && awk -f awk.Makefile Makefile.coq.tmp > Makefile.coq && rm Makefile.coq.tmp
+# Create Coq Makefile.
+Makefile.coq: _CoqProject Makefile
+	"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
 
 # Install build-dependencies
-build-dep:
-	build/opam-pins.sh < opam.pins
-	opam upgrade $(YFLAG) # it is not nice that we upgrade *all* packages here, but I found no nice way to upgrade only those that we pinned
-	opam pin add coq-prelude "$$(pwd)#HEAD" -k git -n -y
-	opam install coq-prelude --deps-only $(YFLAG)
-	opam pin remove coq-prelude
-
-# Some files that do *not* need to be forwarded to Makefile.coq
-Makefile: ;
-_CoqProject: ;
-awk.Makefile: ;
-
-# Phony targets (i.e. targets that should be run no matter the timestamps of the involved files)
-phony: ;
-.PHONY: all clean phony
+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):: ;

Makefile.coq.local

+# 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 $@

README.md

-# Coq-std++
+# 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:
@@ -14,26 +14,91 @@ The key features of this library are as follows:
   `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 simply breadth-first solver
+  `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 axiom free.
+- It is entirely dependency- and axiom-free.
 
-# History
+## Side-effects
 
-Coq-std++ has originally been developed by Robbert Krebbers as part of his
-formalization of the C programming language in his PhD thesis, called
-[CH2O](http://robbertkrebbers.nl/thesis.html). After that, Coq-std++ has been
-part of the [Iris project](http://iris-project.org), and has continued to be
-developed by Robbert Krebbers, Ralf Jung, and Jacques Henri-Jourdan.
+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 8.6
+ - 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
 
-## Building Instructions
+On Windows, differences in line endings may cause tests to fail. This can be
+fixed by setting Git's autocrlf option to true:
 
-Run `make` to build the full development.
+    git config --global core.autocrlf true

_CoqProject

--Q theories stdpp
-theories/option.v
-theories/fin_map_dom.v
-theories/bset.v
-theories/fin_maps.v
-theories/vector.v
-theories/pmap.v
-theories/stringmap.v
-theories/fin_collections.v
-theories/mapset.v
-theories/proof_irrel.v
-theories/hashset.v
-theories/pretty.v
-theories/countable.v
-theories/orders.v
-theories/natmap.v
-theories/strings.v
-theories/relations.v
-theories/collections.v
-theories/listset.v
-theories/streams.v
-theories/gmap.v
-theories/gmultiset.v
-theories/base.v
-theories/tactics.v
-theories/prelude.v
-theories/listset_nodup.v
-theories/finite.v
-theories/numbers.v
-theories/nmap.v
-theories/zmap.v
-theories/coPset.v
-theories/lexico.v
-theories/set.v
-theories/decidable.v
-theories/list.v
-theories/functions.v
-theories/hlist.v
-theories/sorting.v
+# 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_basics.v
+stdpp/list_relations.v
+stdpp/list_monad.v
+stdpp/list_misc.v
+stdpp/list_tactics.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

awk.Makefile

-# awk program that patches the Makefile generated by Coq.
-
-# Detect the name this project will be installed under.
-/\$\(COQLIBINSTALL\)\/.*\/\$\$i/ {
-# Wow, POSIX awk is really broken.  I mean, isn't it supposed to be a text processing language?
-# And there is not even a way to access the matched groups of a regexp...?!? Lucky enough,
-# we can just split the string at '/' here.
-	split($0, PIECES, /\//);
-	PROJECT=PIECES[2];
-}
-
-# Patch the uninstall target to work properly, and to also uninstall stale files.
-# Also see <https://coq.inria.fr/bugs/show_bug.cgi?id=4907>.
-/^uninstall:/ {
-	print "uninstall:";
-	print "\tif [ -d \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ ]; then find \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ \\( -name \"*.vo\" -o -name \"*.v\" -o -name \"*.glob\" -o \\( -type d -empty \\) \\) -print -delete; fi";
-	getline;
-	next
-}
-
-# Patch vio2vo to (a) run "make quick" with the same number of jobs, ensuring
-# that the .vio files are up-to-date, and (b) only schedule vio2vo for those
-# files where the .vo is *older* than the .vio.
-/^vio2vo:/ {
-	print "vio2vo:";
-	print "\t@make -j $(J) quick"
-	print "\t@VIOFILES=$$(for file in $(VOFILES:%.vo=%.vio); do vofile=\"$$(echo \"$$file\" | sed \"s/\\.vio/.vo/\")\"; if [ \"$$vofile\" -ot \"$$file\" -o ! -e \"$$vofile\" ]; then echo -n \"$$file \"; fi; done); \\"
-	print "\t echo \"VIO2VO: $$VIOFILES\"; \\"
-	print "\t if [ -n \"$$VIOFILES\" ]; then $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; fi"
-	getline;
-	next
-}
-
-# This forwards all unchanged lines
-1

coq-lint.sh

+#!/bin/sh
+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

coq-stdpp-bitvector.opam

+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"]

coq-stdpp-unstable.opam

+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"]

coq-stdpp.opam

+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"]

docs/dune.md

+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`.

dune

+(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)))))

dune-project

+(lang dune 3.8)
+(using coq 0.8)

make-package

+#!/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"*

stdpp/binders.v

+(** 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.