Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Iris
stdpp
Commits
df4fbcb4
Commit
df4fbcb4
authored
Jan 13, 2020
by
Ralf Jung
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
opam 2 upgrade
parent
bcb89f76
Changes
3
Hide whitespace changes
Inline
Sidebyside
Showing
3 changed files
with
32 additions
and
34 deletions
+32
34
Makefile
Makefile
+2
8
descr
descr
+0
19
opam
opam
+30
7
No files found.
Makefile
View file @
df4fbcb4
...
...
@@ 29,14 +29,8 @@ builddep: builddep/opam phony
@
# that are incompatible with our build requirements.
@
# To achieve this, we create a fake opam package that has our builddependencies as
@
# dependencies, but does not actually install anything itself.
@
echo
"# Pinning builddep package."
&&
\
if
opam
version

grep
"^1
\.
"
q
;
then
\
BUILD_DEP_PACKAGE
=
"
$$
(egrep "
^name:
" builddep/opam  sed 's/^name: *"
\(
.
*
\)
" */
\1
/')"
&&
\
opam pin add
k
path
$(OPAMFLAGS)
"
$$
BUILD_DEP_PACKAGE"
.dev builddep
&&
\
opam reinstall
$(OPAMFLAGS)
"
$$
BUILD_DEP_PACKAGE"
;
\
else
\
opam
install
$(OPAMFLAGS)
builddep/
;
\
fi
@
echo
"# Installing builddep package."
@
opam
install
$(OPAMFLAGS)
builddep/
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile
:
;
...
...
descr
deleted
100644 → 0
View file @
bcb89f76
This project contains an extended "Standard Library" for Coq called coqstd++.
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 Haskellstyle
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 breadthfirst 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 axiomfree.
opam
View file @
df4fbcb4
opamversion: "1.2"
name: "coqstdpp"
synopsis: "This project contains an extended \"Standard Library\" for Coq called coqstd++"
maintainer: "Ralf Jung <jung@mpisws.org>"
homepage: "https://gitlab.mpisws.org/iris/stdpp"
authors: "Robbert Krebbers, JacquesHenri Jourdan, Ralf Jung"
bugreports: "https://gitlab.mpisws.org/iris/stdpp/issues"
license: "BSD"
devrepo: "https://gitlab.mpisws.org/iris/stdpp.git"
build: [make "j%{jobs}%"]
install: [make "install"]
remove: ["rm" "rf" "%{lib}%/coq/usercontrib/stdpp"]
homepage: "https://gitlab.mpisws.org/iris/stdpp"
bugreports: "https://gitlab.mpisws.org/iris/stdpp/issues"
devrepo: "git+https://gitlab.mpisws.org/iris/stdpp.git"
synopsis: "This project contains an extended \"Standard Library\" for Coq called coqstd++"
description: """
This project contains an extended "Standard Library" for Coq called coqstd++.
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 Haskellstyle
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 breadthfirst 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 axiomfree.
"""
depends: [
"coq" { (= "8.7.2")  (= "8.8.2")  (>= "8.9.1" & < "8.12~")  (= "dev") }
]
build: [make "j%{jobs}%"]
install: [make "install"]
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment