Merge branch 'ci/msammler/stdpp_experimental' into 'master'

Create stdpp-unstable package and add bitblast library

See merge request !402

CHANGELOG.md

@@ -32,6 +32,13 @@ Coq 8.11 is no longer supported.
 - Rename `lookup_union_l` → `lookup_union_l'` and add `lookup_union_l`
   as the dual to `lookup_union_r`.
 - Add `map_seqZ` as the `Z` analogue of `map_seq`. (by Michael Sammler)
+- Add the `coq-stdpp-unstable` package for libraries that are not
+  deemed stable enough to be included in the main std++ library,
+  following the `coq-iris-unstable` package. This library is contained
+  in the `stdpp_unstable` folder. The `theories` folder was renamed
+  to `stdpp`.
+- Add an unstable `bitblast` tactic for solving equalities between integers
+  involving bitwise operations. (by Michael Sammler)
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).

README.md

@@ -65,6 +65,16 @@ To obtain a development version, add the Iris opam repository:
 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.
+
 ## Contributing to std++
 
 If you want to report a bug, please use the

_CoqProject

--Q theories stdpp
+# 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_unstable stdpp.unstable
 # 'Global Hint Rewrite' not supported before Coq 8.14.
 -arg -w -arg -deprecated-hint-rewrite-without-locality
 # Fixing this one requires Coq 8.15.
@@ -6,51 +9,53 @@
 # Fixing this one requires Coq 8.13.
 -arg -w -arg -deprecated-syntactic-definition
 
-theories/options.v
-theories/base.v
-theories/tactics.v
-theories/option.v
-theories/fin_map_dom.v
-theories/boolset.v
-theories/fin_maps.v
-theories/fin.v
-theories/vector.v
-theories/pmap.v
-theories/stringmap.v
-theories/fin_sets.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/well_founded.v
-theories/relations.v
-theories/sets.v
-theories/listset.v
-theories/streams.v
-theories/gmap.v
-theories/gmultiset.v
-theories/prelude.v
-theories/listset_nodup.v
-theories/finite.v
-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
-theories/infinite.v
-theories/nat_cancel.v
-theories/namespaces.v
-theories/telescopes.v
-theories/binders.v
+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_unstable/bitblast.v

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}
+]
+
+build: ["./make-package" "stdpp_unstable" "-j%{jobs}%"]
+install: ["./make-package" "stdpp_unstable" "install"]

coq-stdpp.opam

@@ -36,5 +36,5 @@ depends: [
   "coq" { (>= "8.12" & < "8.16~") | (= "dev") }
 ]
 
-build: [make "-j%{jobs}%"]
-install: [make "install"]
+build: ["./make-package" "stdpp" "-j%{jobs}%"]
+install: ["./make-package" "stdpp" "install"]

make-package

+#!/bin/bash
+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!
+
+PROJECT="$1"
+shift
+
+COQFILE="_CoqProject.$PROJECT"
+MAKEFILE="Makefile.package.$PROJECT"
+
+if ! egrep -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.
+egrep "^-Q $PROJECT[ /]" _CoqProject >> "$COQFILE"
+# Get everything until the first empty line except for the "-Q" lines.
+sed -n '/./!q;p' _CoqProject | egrep -v "^-Q " >> "$COQFILE"
+# Get the files.
+egrep "^$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"*