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 (2352)
# 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
......@@ -10,4 +14,13 @@
*.bak
.coq-native/
Makefile.coq
Makefile.coq.conf
_CoqProject.*
Makefile.package.*
.Makefile.package.*
*.crashcoqide
html/
builddep/
_opam
_build/
*.install
image: ralfjung/opam-ci:latest
image: ralfjung/opam-ci:opam2
stdpp-coq8.5:
tags:
- coq
script:
# prepare
- . build/opam-ci.sh coq 8.5.3
# build
- 'time make -j8'
cache:
key: "coq8.5"
paths:
- opamroot/
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
- ci
- timing
- /^master/@iris/stdpp
- /^ci/@iris/stdpp
- merge_requests
stdpp-coq8.6:
.template: &template
<<: *only_branches
stage: build
interruptible: true
tags:
- coq
- fp
script:
# prepare
- . build/opam-ci.sh coq 8.6
# build
- 'time make -j8 TIMED=y 2>&1 | tee build-log.txt'
- 'if fgrep Axiom build-log.txt >/dev/null; then exit 1; fi'
- 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time.txt'
- 'if (( RANDOM % 10 == 0 )); then make validate; fi'
- git clone https://gitlab.mpi-sws.org/iris/ci.git ci -b opam2
- ci/buildjob
cache:
key: "coq8.6"
key: "$CI_JOB_NAME"
paths:
- opamroot/
only:
- master
- ci
- timing
- _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 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.
# 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 opam-builddep-temp "$$(pwd)#HEAD" -k git -n -y
opam install opam-builddep-temp --deps-only $(YFLAG)
opam pin remove opam-builddep-temp
# 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):: ;
# 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++
# 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:
......@@ -20,20 +20,85 @@ The key features of this library are as follows:
`set_solver` for goals involving set operations.
- 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.5pl3 / 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. Run `make install` to install the library.
git config --global core.autocrlf true
-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_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 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
#!/bin/bash
set -e
# This script installs the build dependencies for CI builds.
# Prepare OPAM configuration
export OPAMROOT="$(pwd)/opamroot"
export OPAMJOBS=16
export OPAM_EDITOR="$(which false)"
# Make sure we got a good OPAM
test -d "$OPAMROOT" || (mkdir "$OPAMROOT" && opam init --no-setup -y)
eval `opam conf env`
test -d "$OPAMROOT/repo/coq-extra-dev" || opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev -p 5
test -d "$OPAMROOT/repo/coq-core-dev" || opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev -p 5
test -d "$OPAMROOT/repo/coq-released" || opam repo add coq-released https://coq.inria.fr/opam/released -p 10
opam update
# Install fixed versions of some dependencies
echo
while (( "$#" )); do # while there are arguments left
PACKAGE="$1" ; shift
VERSION="$1" ; shift
# Check if the pin is already set
if opam pin list | fgrep "$PACKAGE.$VERSION " > /dev/null; then
echo "[opam-ci] $PACKAGE already pinned to $VERSION"
else
echo "[opam-ci] Pinning $PACKAGE to $VERSION"
opam pin add "$PACKAGE" "$VERSION" -k version -y
fi
done
# Install build-dependencies
echo
make build-dep Y=1
# done
echo
coqc -v
#!/bin/bash
set -e
## Process an opam.pins file from stdin: Add all the given pins, but don't install anything.
## Usage:
## ./opam-pins.sh < opam.pins
if ! which curl >/dev/null; then
echo "opam-pins needs curl. Please install curl and try again."
exit 1
fi
# Process stdin
while read PACKAGE URL HASH; do
if echo "$URL" | egrep '^https://gitlab\.mpi-sws\.org' > /dev/null; then
echo "[opam-pins] Recursing into $URL"
# an MPI URL -- try doing recursive pin processing
curl -f "$URL/raw/$HASH/opam.pins" 2>/dev/null | "$0"
fi
if opam pin list | fgrep "$PACKAGE.dev.$HASH " > /dev/null; then
echo "[opam-pins] $PACKAGE already at commit $HASH"
else
echo "[opam-pins] Applying pin: $PACKAGE -> $URL#$HASH"
opam pin add "$PACKAGE.dev.$HASH" "$URL#$HASH" -k git -y -n
echo
fi
done
#!/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"*