.gitignore

@@ -15,7 +15,14 @@
 .coq-native/
 Makefile.coq
 Makefile.coq.conf
+_CoqProject
+_CoqProject.*
+Makefile.package.*
+.Makefile.package.*
 *.crashcoqide
 html/
 builddep/
 _opam
+_build/
+*.install
+config/local-flags

.gitlab-ci.yml

@@ -5,6 +5,9 @@ stages:
 
 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:
@@ -24,6 +27,7 @@ variables:
 .template: &template
   <<: *only_branches
   stage: build
+  interruptible: true
   tags:
   - fp
   script:
@@ -40,46 +44,52 @@ variables:
 
 ## Build jobs
 
-build-coq.dev:
+# The newest version runs with timing.
+build-coq.9.0.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version dev"
+    OPAM_PINS: "coq version 9.0.0"
+    DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
     CI_COQCHK: "1"
-
-build-coq.8.13.2:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version 8.13.2"
-    MANGLE_NAMES: "1"
-    DENY_WARNINGS: "1"
     OPAM_PKG: "1"
     DOC_DIR: "coqdoc@center.mpi-sws.org:stdpp"
   tags:
   - fp-timing
+  interruptible: false
 
-# Separate MR job that does not run on fp-timing.
-build-coq.8.13.2-mr:
+# The newest version also runs in MRs, without timing.
+build-coq.9.0.0-mr:
   <<: *template
   <<: *only_mr
   variables:
-    OPAM_PINS: "coq version 8.13.2"
-    MANGLE_NAMES: "1"
+    OPAM_PINS: "coq version 9.0.0"
     DENY_WARNINGS: "1"
+    MANGLE_NAMES: "1"
+
+# Also ensure Dune works (broken on older Coq versions due to Stdlib split).
+build-coq.9.0.0-dune:
+  <<: *template
+  variables:
+    OPAM_PINS: "coq version 9.0.0   dune version 3.18.1"
+    MAKE_TARGET: "dune"
 
-build-coq.8.12.2:
+build-coq.8.20.1:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.12.2"
+    OPAM_PINS: "coq version 8.20.1"
     DENY_WARNINGS: "1"
 
-build-coq.8.11.2:
+build-coq.8.19.1:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.11.2"
+    OPAM_PINS: "coq version 8.19.1"
+    DENY_WARNINGS: "1"
 
-build-coq.8.10.2:
+# The oldest version runs in MRs, without name mangling.
+build-coq.8.18.0:
   <<: *template
   <<: *branches_and_mr
   variables:
-    OPAM_PINS: "coq version 8.10.2"
+    OPAM_PINS: "coq version 8.18.0"
+    DENY_WARNINGS: "1"

Makefile

@@ -3,9 +3,19 @@ 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
 
+# Generate the _CoqProject file.
+_CoqProject: gen_CoqProject.sh config/paths config/flags config/source-list $(wildcard config/local-flags)
+	@./$< > $@
+
 # Forward most targets to Coq makefile (with some trick to make this phony)
 %: Makefile.coq phony
 	@#echo "Forwarding $@"
@@ -17,7 +27,7 @@ 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/*
+	rm -f Makefile.coq .lia.cache builddep/* _CoqProject
 .PHONY: clean
 
 # Create Coq Makefile.
@@ -52,4 +62,4 @@ build-dep: builddep
 
 # Some files that do *not* need to be forwarded to Makefile.coq.
 # ("::" lets Makefile.local overwrite this.)
-Makefile Makefile.local _CoqProject $(OPAMFILES):: ;
+Makefile Makefile.local config/paths config/flags config/source-list config/local-flags $(OPAMFILES):: ;

Makefile.coq.local

@@ -4,14 +4,19 @@ 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)"Performing some style checks..."
+	$(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 ; \
+	  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
@@ -24,8 +29,6 @@ test: $(TESTFILES:.v=.vo)
 .PHONY: test
 
 COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
-# 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)
 	$(SHOW)'COQDEP TESTFILES'
@@ -35,21 +38,22 @@ tests/.coqdeps.d: $(TESTFILES)
 # 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)if test -f $*".$(COQ_MINOR_VERSION).ref"; then \
-	    REF=$*".$(COQ_MINOR_VERSION).ref"; \
-	  else \
-	    REF=$*".ref"; \
-	  fi && \
-	  echo "COQTEST$(if $(MAKE_REF), [make ref],) $< (ref: $$REF)" && \
+	$(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 -f $(NORMALIZER) "$$TMPFILE" > "$$TMPFILE".new && \
+	  sed -E -f $(NORMALIZER) "$$TMPFILE" > "$$TMPFILE".new && \
 	  mv "$$TMPFILE".new "$$TMPFILE" && \
-	  $(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff -u "$$REF" "$$TMPFILE") && \
+	  $(if $(COQ_REF),\
+	    $(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff --strip-trailing-cr -u "$$REF" "$$TMPFILE"), \
+	    true \
+	  ) && \
 	  rm -f "$$TMPFILE" && \
 	  touch $@

README.md

@@ -26,26 +26,27 @@ 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).  Unfortunately, it
-  also enables implicit generalization in `Instance`.  We think that the fact
-  that both behaviors are coupled together is a
-  [bug in Coq](https://github.com/coq/coq/issues/6030).
+  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 integers `Z` (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`).
-  As a consequence of blocking `simpl`, due to
-  [Coq bug #5039](https://github.com/coq/coq/issues/5039) the `omega` tactic
-  becomes unreliable. We do not consider this an issue since we use `lia` (for
-  which the aforementioned Coq bug was fixed) instead of `omega` everywhere.
+* 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.10.2 / 8.11.2 / 8.12.2 / 8.13.2
+ - Coq version 8.18.0 / 8.19.1 / 8.20.1 / 9.0.0
+
+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
 
@@ -65,6 +66,19 @@ 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.
+
+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
@@ -79,9 +93,12 @@ 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 
+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

_CoqProject

--Q theories stdpp
-
-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/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

config/flags

+# Specification for custom Rocq compilation flags.
+# Syntax:
+# - One flag per line with no leading/trailing blanks.
+# - Empty lines and lines starting with '#' are ignored.
+
+# Fixing this one requires Coq 8.19
+-w
+-argument-scope-delimiter
+
+# Warning seems incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
+-w
+-notation-incompatible-prefix
+
+# We can't do this migration yet until we require Coq 9.0
+-w
+-deprecated-from-Coq
+-w
+-deprecated-dirpath-Coq

config/paths

+# Search paths for all packages.
+# Each line should be of the form "<PACKAGE> <LOGICAL_PATH>",
+# where <PACKAGE> is the name of a directory that matches the
+# corresponding package name.
+stdpp stdpp
+stdpp_bitvector stdpp.bitvector
+stdpp_unstable stdpp.unstable

config/source-list

+# List of source files included in the libraries.
+
+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

coq-lint.sh

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

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

@@ -28,10 +28,13 @@ The key features of this library are as follows:
   `set_solver` for goals involving set operations.
 - It is entirely dependency- and axiom-free.
 """
+tags: [
+  "logpath:stdpp"
+]
 
 depends: [
-  "coq" { (>= "8.10.2" & < "8.14~") | (= "dev") }
+  "coq" { (>= "8.18" & < "9.1~") | (= "dev") }
 ]
 
-build: [make "-j%{jobs}%"]
-install: [make "install"]
+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
+--------------
+
+Editors relying on `_CoqProject` files for their configuration are supported.
+A suitable `_CoqProject` file is generated by `dune build`. Note that you must
+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 use, e.g.,
+`dune build stdpp/options.vo`. To build only the `stdpp` folder, you can do
+`dune build stdpp`.
+
+Alternatively, you can configure your editor to invoke `dune coq top` instead
+of `coqtop`, but that is non-trivial for most editors.
+
+### Extra `_CoqProject` flags
+
+If file `config/local-flags` exists, then its contents is added at the end of
+the generated `_CoqProject` file. This can be useful when the library is built
+together with its dependencies (e.g., the Rocq standard library) as part of a
+dune workspace build. Note that the file can be generated with a dune rule.

dune

+(env
+ (_ ; Applies to all profiles (dev, release, ...).
+  (coq
+   ; Configure coqc flags.
+   (flags (:standard %{read-lines:flags.dune})))))
+
+(rule
+ (action
+  (with-stdout-to flags.dune
+   (pipe-stdout
+    (cat config/flags)
+    (bash "grep '^[^#]\\+'")))))
+
+(rule
+ (deps
+  (glob_files config/*))
+ (mode promote)
+ (action
+  (with-stdout-to _CoqProject
+   (run ./gen_CoqProject.sh))))

dune-project

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

gen_CoqProject.sh

+#!/bin/sh
+set -e
+# Script generating the contents of [_CoqProject] based on files [config/*].
+# We use standard dune variable DUNE_SOURCEROOT to determine if the build
+# system is dune. In a dune build, the [_CoqProject] is solely used for editor
+# support.
+
+echo "# Generated file, edit [config/*] instead."
+
+echo
+echo "# Search paths"
+# Adding "-Q " prefix to all non-empty, non-comment lines of [config/paths].
+cat config/paths | grep "^[^#]\+" | sed "s/^/-Q /"
+# When building with dune, we also add the corresponding paths under dune's
+# [_build] directory. This is done by adding the prefix "-Q $PWD/" to all
+# non-empty, non-comment lines of [config/paths]. So for instance, this will
+# complement an entry of the form "-Q dir coqdir" produced above, with an
+# entry "-Q $PWD/dir coqdir". This relies on the fact that dune runs (a copy
+# of) the current script in the corresponding path under [_build]. This is
+# where ".vo" files actually end up in a dune build. Note that paths without
+# the "$PWD/" prefix are given first, so that editors find the original ".v"
+# sources (e.g., for "jump to definition") instead of their copy under the
+# [_build] directory.
+if [ -n "$DUNE_SOURCEROOT" ]; then
+  cat config/paths | grep "^[^#]\+" | sed "s,^,-Q $PWD/,"
+fi
+
+echo
+echo "# Flags"
+# Adding "-arg " prefix to all non-empty, non-comment lines of [config/flags].
+cat config/flags | grep "^[^#]\+" | sed "s/^/-arg /"
+
+# Potential extra flags.
+if [ -f config/local-flags ]; then
+  echo
+  # We take the whole file; no need to strip comments.
+  cat config/local-flags
+fi
+
+# The list of source files is only needed for [coq_makefile] builds.
+if [ -z "$DUNE_SOURCEROOT" ]; then
+  echo
+  echo "# Sources"
+  # Take only non-empty, non-comment lines of [config/source-list].
+  cat config/source-list | grep "^[^#]\+"
+fi

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"
+
+# Ensure we have an up-to-date _CoqProject file.
+$MAKE _CoqProject
+
+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"*